Guest User

Untitled

a guest
Jun 20th, 2018
84
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 0.19 KB | None | 0 0
  1. Lemma exercise2 : forall A B C D:Prop, (A->B)/\(C->D)/\A/\C -> B/\D.
  2. Proof.
  3. intros A B C D H.
  4. destruct H as [H1 [H2 [H3 H4]]].
  5. split.
  6. apply H1.
  7. exact H3.
  8. apply H2.
  9. exact H4.
  10. Qed.
Add Comment
Please, Sign In to add comment