proposition: Lemma red_union : red (R ++ R') << red R U red R'.
proof: Proof. unfold inclusion. intros. redtac. subst x. subst y. destruct (in_app_or lr). left. apply red_rule. hyp. right. apply red_rule. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)