Inductive myprod (X Y : Type) : Type := mypair : X -> Y -> myprod X Y. Check myprod. (* <- 型を生む関数 *) Check myprod nat nat. (* <- (型関数 myprod が型引数 nat natを取って出来た)型 *) Check mypair nat bool 1 false. (* 構成子 mypairによ…

4章まで出て来たタクティーク一覧 intros: 仮定や変数をゴールからコンテキストに移す reflexivity: 証明を完了させる（ゴールがe = eという形になっている場合） apply... （in H）: 仮定、補助定理、コンストラクタを使ってゴールを証明する apply... with…