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. コマンド Section HilbertSaxiom は、あとで閉じられるCoqのセクションを始めます。 コマンド Variable A B C : Prop は命題変数A,B,C(型はProp)を仮定します。 これらの変数は今のセクション HilbertSaxiomの中で使えます。 上の補題は HilbertS と呼ばれます。 (A -> B -> C) -> (A -> B) -> A -> CにおけるA -> B -> CはA