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