inductive ex (A:Type) (P:A \to Prop) : Prop \def
ex_intro: \forall x:A. P x \to ex A P.
-interpretation "exists" 'exists x = (ex _ x).
+interpretation "exists" 'exists x = (ex ? x).
inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def
ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q.