proposition: Lemma same_relation_Symmetric {A}: Symmetric (same_relation A).
proof: Proof. hnf; intros. rewrite same_relation_spec in *. unfold pointwise_relation in *. firstorder. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Coq.Classes.Equivalence