proposition: Lemma flip_pointwise_relation A (R : relation A) : relation_equivalence (pointwise_relation A (flip R)) (flip (pointwise_relation A R)).
proof: Proof. intros. split; firstorder. Qed.
imports: Relation_Definitions Coq.Classes.Morphisms Coq.Program.Program