proposition: Lemma context_closed_red_mod (E R : rules) : context_closed (red_mod E R).
proof: Proof. apply context_closed_comp. apply context_closed_rtc. apply context_closed_red. apply context_closed_red. Qed.
imports: CoLoR(ATrs ListUtil RelUtil ARelation LogicUtil SetUtil) Coq(Morphisms)