proposition: Lemma red_union_inv : red R U red R' << red (R ++ R').
proof: Proof. intros x y RR'xy. destruct RR'xy as [Rxy | Rxy]; destruct Rxy as [rl [rr [c [s [Rr [dx dy]]]]]]; subst x; subst y; ex rl rr c s; intuition. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)