(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/elim".
-include "legacy/coq.ma".
+
+include "coq.ma".
inductive stupidtype: Set \def
| Base : stupidtype
(\lambda a,b,K. y=a \to O=b \to
match K with [ (k a b p) \Rightarrow a ] = x)
? ? ? H).
- goal 16.
simplify. intros.
generalize in match H1.
rewrite < H2; rewrite < H3.intro.
- rewrite > H4.auto new library.
+ rewrite > H4.autobatch library.
qed.