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.
13 (* inversion begins *)
19 apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
20 (* first goal (left open) *)
21 intro. rewrite right H1.
23 (* second goal (closed) *)
31 (* Piu' semplice e non lascia l'ipotesi inutile Hcut *)
32 alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
33 theorem test_inversion2: \forall n. le n O \to n=O.
35 (* inversion begins *)
36 generalize (refl_equal nat O).
37 apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
38 (* first goal (left open) *)
39 intro. rewrite right H1.
40 (* second goal (closed) *)