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