proposition: Lemma compond_assoc: forall {A: Type} (R1 R2 R3: relation A), same_relation _ (compond_relation (compond_relation R1 R2) R3) (compond_relation R1 (compond_relation R2 R3)).
proof: Proof. intros. split; hnf; intros; do 2 match goal with | H : compond_relation _ _ _ _ |- _ => inversion H; subst; clear H end; do 2 (econstructor; eauto). Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Coq.Classes.Equivalence