Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
ひろしま学生IT勉強会で発表した資料です
Theorem p : forall (A : Type)
(b : bool)
(x : A),
(if b then x else x) = x.
Proof.
intros A b x.
destruct b.
- reflexivity.
- reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.