proposition: Lemma app_same_relation: forall {A: Type} (R1 R2: relation A) (a1 a2: A), same_relation A R1 R2 -> (R1 a1 a2 <-> R2 a1 a2).
proof: Proof. intros. rewrite same_relation_spec in H. specialize (H a1 a2). tauto. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Coq.Classes.Equivalence