interpretation "exists1" 'exists x = (Ex1 ? x).
interpretation "exists" 'exists x = (Ex ? x).
+ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝
+ sig_intro : ∀x:A.P x → sigma A P.
+
+interpretation "sigma" 'sigma \eta.p = (sigma ? p).
+
nrecord iff (A,B: CProp[0]) : CProp[0] ≝
{ if: A → B;
fi: B → A