proposition: Lemma red_preserve_vars : preserve_vars (red R).
proof: Proof. unfold preserve_vars. intros. redtac. subst t. subst u. trans (cvars c ++ vars (sub s r)). apply vars_fill_elim. trans (cvars c ++ vars (sub s l)). apply appl_incl. apply incl_vars_sub. apply hyp. hyp. apply vars_fill_intro. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)