- cut O=O.
- (* goal 2: 0 = 0 *)
- goal 7. reflexivity.
- (* goal 1 *)
- generalize Hcut. (* non attaccata. Dovrebbe dare 0=0 -> n=0 *)
- apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
- intro. reflexivity.
- simplify. intros.
- discriminate H3.
-qed.
\ No newline at end of file
+ inversion H.
+
+ (*
+ cut (y = y \to O = O \to match H with [ (k a b p) \Rightarrow a] = x).
+ apply Hcut; reflexivity.
+ apply
+ (sum_ind ?
+ (\lambda a,b,K. y=a \to O=b \to
+ match K with [ (k a b p) \Rightarrow a ] = x)
+ ? ? ? H).
+ goal 16.*)
+ simplify. intros.
+ generalize in match H1.
+ rewrite < H2; rewrite < H3.intro.
+ rewrite > H4.auto.
+qed.
+
+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.
+qed.