+inductive exT22 (A:Type2) (P:A→CProp2) : CProp2 ≝
+ ex_introT22: ∀w:A. P w → exT22 A P.
+
+interpretation "CProp2 exists" 'exists \eta.x = (exT22 _ x).
+
+definition pi1exT22 ≝ λA,P.λx:exT22 A P.match x with [ex_introT22 x _ ⇒ x].
+definition pi2exT22 ≝
+ λA,P.λx:exT22 A P.match x return λx.P (pi1exT22 ?? x) with [ex_introT22 _ p ⇒ p].
+
+interpretation "exT22 \fst" 'pi1 = (pi1exT22 _ _).
+interpretation "exT22 \snd" 'pi2 = (pi2exT22 _ _).
+interpretation "exT22 \fst a" 'pi1a x = (pi1exT22 _ _ x).
+interpretation "exT22 \snd a" 'pi2a x = (pi2exT22 _ _ x).
+interpretation "exT22 \fst b" 'pi1b x y = (pi1exT22 _ _ x y).
+interpretation "exT22 \snd b" 'pi2b x y = (pi2exT22 _ _ x y).
+