1 inductive pos: Set \def
9 definition pos2nat : pos \to nat \def
10 \lambda x:pos . match x with
12 | (next z) \Rightarrow O].
14 inductive empty (x:nat) : nat \to Set \def .
16 definition empty2nat : (empty O O) \to nat \def
17 \lambda x : (empty O O). S (match x in empty with []).
19 inductive le (n:nat) : nat \to Prop \def
21 | le_S : \forall m:nat. le n m \to le n (S m).
23 inductive True : Prop \def
26 definition r : True \def
29 | (le_S y p') \Rightarrow I ].