-(* Piu' semplice e non lascia l'ipotesi inutile Hcut *)
-alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
-theorem test_inversion2: \forall n. le n O \to n=O.
- intros.
- (* inversion begins *)
- generalize in match (refl_equal nat O).
- apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H);
- [ intro. rewrite < H1.
- | simplify. intros. discriminate H3.
- ]
- reflexivity.
+theorem t1: \forall x,y. sum x y O \to x = y.
+intros.
+
+(*
+cut y=y \to O=O \to x = y.
+apply Hcut.reflexivity. reflexivity.
+apply (sum_ind ? (\lambda a,b,K. y=a \to O=b \to x=a) ? ? ? s).*)
+
+(*apply (sum_ind ? (\lambda a,b,K. y = a \to O = b \to x = a) ? ? ? s).*)
+inversion s.
+intros.simplify.
+intros.
+rewrite > H. rewrite < H2. auto.