proposition: Lemma rt_red_mod_union (E R : rules) : red_mod E R # << red (union E R) #.
proof: Proof. intros. incl_trans (red(union E R)##). rewrite red_mod_union. refl. rewrite rtc_invol. refl. Qed.
imports: CoLoR(ATrs ListUtil RelUtil ARelation LogicUtil SetUtil) Coq(Morphisms)