(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/inversion_sum/".
-include "legacy/coq.ma".
+
+include "coq.ma".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
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.