inductive ex (A:Type) (P:A \to Prop) : Prop \def
ex_intro: \forall x:A. P x \to ex A P.
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "exists" 'exists x y = (cic:/matita/logic/connectives/ex.ind#xpointer(1/1) x y).
+
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.