proposition: Lemma relation_disjunction_inclusion_right: forall {A} (R R': relation A), inclusion _ R' (relation_disjunction R R').
proof: Proof. intros. intros ? ? ?. rewrite relation_disjunction_iff. tauto. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Coq.Classes.Equivalence