Skip to content

Instantly share code, notes, and snippets.

@mheiber

mheiber/sum_equiv_visitor.v

Last active August 8, 2024 22:00
Show Gist options
  • Save mheiber/872eddb8fdec21a8cb63b6a4d2710892 to your computer and use it in GitHub Desktop.
Save mheiber/872eddb8fdec21a8cb63b6a4d2710892 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
sum_equiv_visitor.v
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