proposition: Lemma context_closed_red_mod : context_closed (red_mod E R).
proof: Proof. intros t u c h. apply red_mod_fill. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)