proposition: Lemma compond_relation_spec: forall {A} (R1 R2: relation A) x z, compond_relation R1 R2 x z -> exists y, R1 x y /\ R2 y z.
proof: Proof. intros. inversion H; subst. eauto. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Coq.Classes.Equivalence