12/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.