definition Iff : Prop \to Prop \to Prop \def
\lambda A,B. (A \to B) \land (B \to A).
(*CSC: the URI must disappear: there is a bug now *)
interpretation "logical iff" 'iff x y = (cic:/matita/logic/iff/Iff.con x y).
definition Iff : Prop \to Prop \to Prop \def
\lambda A,B. (A \to B) \land (B \to A).
(*CSC: the URI must disappear: there is a bug now *)
interpretation "logical iff" 'iff x y = (cic:/matita/logic/iff/Iff.con x y).