+inductive And (A,B:Type) : Type ≝
+ | Conj : A → B → And A B.
+
+interpretation "constructive and" 'and x y =
+ (cic:/matita/constructive_connectives/And.ind#xpointer(1/1) x y).
+
+inductive exT (A:Type) (P:A→Type) : Type ≝
+ ex_introT: ∀w:A. P w → exT A P.
+
+inductive ex (A:Type) (P:A→Prop) : Type ≝