I : True.
ninductive False: CProp ≝.
-(* elimination principle *)
-ndefinition False_rect ≝ λP: False → Type.λp: False.
- match p in False return λp. P p with [].
ndefinition Not: CProp → CProp ≝
λA. A → False.
ninductive Ex (A:Type) (P:A → CProp) : CProp ≝
ex_intro: ∀x:A. P x → Ex A P.
+
+ninductive Ex1 (A:Type[1]) (P:A → CProp) : CProp[1] ≝
+ ex_intro1: ∀x:A. P x → Ex1 A P.
+
+interpretation "exists1" 'exists x = (Ex1 ? x).
interpretation "exists" 'exists x = (Ex ? x).
+
+nrecord iff (A,B: CProp) : CProp ≝
+ { if: A → B;
+ fi: B → A
+ }.
+
+notation > "hvbox(a break \liff b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+interpretation "logical iff" 'iff x y = (iff x y).