1 set "baseuri" "cic:/matita/tests/".
3 inductive nat : Set \def
7 inductive le (n:nat) : nat \to Prop \def
9 | leS : \forall m. le n m \to le n (S m).
11 alias symbol "eq" (instance 0) = "leibnitz's equality".
13 theorem test_inversion: \forall n. le n O \to n=O.
19 generalize Hcut. (* non attaccata. Dovrebbe dare 0=0 -> n=0 *)
20 apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).