proposition: Lemma flip_respectful (R : relation A) (R' : relation B) : relation_equivalence (flip (R ==> R')) (flip R ==> flip R').
proof: Proof. intros. unfold flip, respectful. split ; intros ; intuition. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses