proposition: Lemma context_closed_red (R : rules) : context_closed (red R).
proof: Proof. intros t u c h. redtac. subst. rewrite !fill_fill. ex l r (comp c c0) s. intuition. Qed.
imports: CoLoR(ATrs ListUtil RelUtil ARelation LogicUtil SetUtil) Coq(Morphisms)