proposition: Lemma same_relation_Transitive {A}: Transitive (same_relation A).
proof: Proof. hnf; intros. rewrite same_relation_spec in *. unfold pointwise_relation in *. intros a b. specialize (H a b). specialize (H0 a b). firstorder. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Coq.Classes.Equivalence