proposition: Lemma proper_sym_arrow_iffT : forall `(Symmetric A R)`(Proper _ (R==>arrow) f), Proper (R==>iffT) f.
proof: Proof. intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Classes.CRelationClasses