+ 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.