fact: Definition relation_disjunction (R : relation A) (R' : relation A) : relation A := @predicate_union (A::A::Tnil) R R'.
imports: Coq.Classes.Init Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions