proposition: Lemma red_mod_union : red_mod E (R ++ R') << red_mod E R U red_mod E R'.
proof: Proof. unfold inclusion. intros. do 2 destruct H. redtac. subst x0. subst y. destruct (in_app_or lr). left. exists (fill c (sub s l)); split. hyp. apply red_rule. hyp. right. exists (fill c (sub s l)); split. hyp. apply red_rule. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)