proposition: Lemma iffE (b1 b2 : bool) : b1 = b2 <-> (b1 <-> b2).
proof: Proof. by split=>[->|] //; move/iffPb/eqP. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)