proposition: Lemma relation_disjunction_iff: forall {A} (R R': relation A) x y, relation_disjunction R R' x y <-> R x y \/ R' x y.
proof: Proof. intros. reflexivity. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Coq.Classes.Equivalence