proposition: Lemma proper_sym_impl_iff_2 : forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>impl) f), Proper (R==>R'==>iff) f.
proof: Proof. intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'. repeat red in Hf. split; eauto. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses