Skip to content

Instantly share code, notes, and snippets.

@takoeight0821

takoeight0821/Demo.v

Created January 6, 2018 05:53
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save takoeight0821/3814235f3229caa14952b2804e94265a to your computer and use it in GitHub Desktop.
Save takoeight0821/3814235f3229caa14952b2804e94265a to your computer and use it in GitHub Desktop.
Download ZIP
ひろしま学生IT勉強会で発表した資料です
Raw
Demo.v
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