--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/tests/elim".
+
+inductive stupidtype: Set \def
+ | Base : stupidtype
+ | Next : stupidtype \to stupidtype
+ | Pair : stupidtype \to stupidtype \to stupidtype.
+
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "exists" (instance 0) = "exists".
+alias symbol "or" (instance 0) = "logical or".
+
+theorem serious:
+ \forall a:stupidtype.
+ a = Base
+ \lor
+ (\exists b:stupidtype.a = Next b)
+ \lor
+ (\exists c,d:stupidtype.a = Pair c d).
+intros.
+elim a.
+clear a.left.left.
+ reflexivity.
+clear H.clear H1.clear a.right.
+ exists.exact e2.exists.exact e1.reflexivity.
+clear H.clear a.left.right.
+ exists.exact e3.reflexivity.
+qed.
\ No newline at end of file