proposition: Lemma red_mod_union (E R : rules) : red_mod E R << red (union E R) #.
proof: Proof. intros t u [h [h1 h2]]. revert h1 h2. induction 1; intro. apply rt_trans with y. apply rt_step. apply red_incl with E. apply subset_union_l. hyp. apply rt_step. apply red_incl with R. apply subset_union_r. hyp. apply rt_step. apply red_incl with R. apply subset_union_r. hyp. apply rt_trans with y. eapply incl_elim. eapply rtc_incl. eapply red_incl. apply subset_union_l. hyp. auto. Qed.
imports: CoLoR(ATrs ListUtil RelUtil ARelation LogicUtil SetUtil) Coq(Morphisms)