proposition: Lemma relation_conjunction_inclusion: forall {A} (R1 R2 R3 R4: relation A), inclusion _ R1 R2 -> inclusion _ R3 R4 -> inclusion _ (relation_conjunction R1 R3) (relation_conjunction R2 R4).
proof: Proof. intros. hnf; intros. inversion H1; subst. split; auto. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Coq.Classes.Equivalence