proposition: Lemma incl_vars_sub l r : incl (vars r) (vars l) -> incl (vars (sub s r)) (vars (sub s l)).
proof: Proof. intros. rewrite !vars_sub. apply incl_svars. hyp. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)