simplify. intros.
generalize in match H1.
rewrite < H2; rewrite < H3.intro.
- rewrite > H4.auto.
+ rewrite > H4.auto new.
qed.
theorem t1: \forall x,y. sum x y O \to x = y.
inversion s.
intros.simplify.
intros.
-rewrite > H. rewrite < H2. auto.
+rewrite > H. rewrite < H2. auto new.
qed.