ninductive Not (A:Prop): Prop ≝
nmk: (A → False) → Not A.
-ncheck Not_ind.
-
interpretation "logical not" 'not x = (Not x).
ntheorem absurd : ∀ A:Prop. A → ¬A → False.
ndefinition iff :=
λ A,B. (A → B) ∧ (B → A).
+
+interpretation "iff" 'iff a b = (iff a b).