Skip to content

Instantly share code, notes, and snippets.

@mheiber

mheiber/sum_equiv_visitor.v Secret

Last active Apr 17, 2021
Embed
What would you like to do?
Theorem sum_equiv_visitor(A B C: Prop): A \/ B -> C <-> (A -> C) /\ (B -> C).
Proof.
split.
- auto.
- destruct H; intro H0; destruct H0; auto.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment