1 inductive nat : Set \def
5 inductive le (n:nat) : nat \to Prop \def
7 | leS : \forall m. le n m \to le n (S m).
9 alias symbol "eq" (instance 0) = "leibnitz's equality".
11 theorem test_inversion: \forall n. le n O \to n=O.
17 generalize Hcut. (* non attaccata. Dovrebbe dare 0=0 -> n=0 *)
18 apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).