Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- lemma assumes "P ∧ C" "Z" shows "C"
- proof - from assms show ?thesis apply(erule conjunct2) oops
- lemma "P ∧ C ⟹ Z ⟹ C"
- apply(erule conjunct2) done
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement