proposition: Lemma compond_eq_right: forall {A: Type} (R: relation A), same_relation _(compond_relation R eq) R.
proof: Proof. intros. split; hnf; intros. + inversion H; subst. auto. + econstructor; eauto. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Coq.Classes.Equivalence