(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/elim".
-include "../legacy/coq.ma".
+
+include "coq.ma".
inductive stupidtype: Set \def
| Base : stupidtype
simplify. intros.
generalize in match H1.
rewrite < H2; rewrite < H3.intro.
- rewrite > H4.auto new library.
+ rewrite > H4.autobatch library.
qed.