proposition: Lemma proper_sym_flip_2 : forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f), Proper (R1==>R2==>flip R3) f.
proof: Proof. intros A R1 Sym1 B R2 Sym2 C R3 f Hf. intros x x' Hxx' y y' Hyy'. apply Hf; auto. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses