- 135 名前：デフォルトの名無しさん mailto:sage [2012/03/09(金) 10:57:54.37 ]
- >>134
証明を引数として取るコンストラクタを使うとか
Require Import Arith.
Inductive my (n:nat) : Set :=
| myO : my n
| myS a : a <= n -> my n.
Section my1.
Let my1 := my 1.
Definition my1_0 : my1 := myO 1.
Program Definition my1_1 : my1 := myS _ 1 _.
End my1.
