Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/SsreflectSample.v

Created April 26, 2014 00:33
Show Gist options
  • Save yoshihiro503/11308205 to your computer and use it in GitHub Desktop.
Save yoshihiro503/11308205 to your computer and use it in GitHub Desktop.
Download ZIP
Ssreflect Tutorial最初のコード ref: http://qiita.com/yoshihiro503/items/6a1f0c6933daafd4754b
Raw
SsreflectSample.v
Require Import ssreflect ssrbool eqtype ssrnat.
Section HilbertSaxiom.
Variables A B C : Prop.
Lemma HilbertS : (A -> B -> C) -> (A -> B) -> A -> C.
Proof.
move=> hAiBiC hAiB hA.
move: hAiBiC.
apply.
by [].
by apply: hAiB.
Qed.
End HilbertSaxiom.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment