Ssreflect Tutorial最初のコード
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.
Author And Source
この問題について(Ssreflect Tutorial最初のコード), 我々は、より多くの情報をここで見つけました https://qiita.com/yoshihiro503/items/6a1f0c6933daafd4754b著者帰属：元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。
Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .