1 set "baseuri" "cic:/matita/tests/match_inference/".
3 inductive pos: Set \def
11 definition pos2nat : pos \to nat \def
12 \lambda x:pos . match x with
14 | (next z) \Rightarrow O].
16 inductive empty (x:nat) : nat \to Set \def .
18 definition empty2nat : (empty O O) \to nat \def
19 \lambda x : (empty O O). S (match x in empty with []).
21 inductive le (n:nat) : nat \to Prop \def
23 | le_S : \forall m:nat. le n m \to le n (S m).
25 inductive True : Prop \def
28 definition r : True \def
31 | (le_S y p') \Rightarrow I ].