proposition: Lemma vars_sub : forall t, vars (sub s t) = svars (vars t).
proof: Proof. apply term_ind with (Q := fun n (v : terms n) => vars_vec (Vmap (sub s) v) = svars (vars_vec v)). simpl. intro. rewrite <- app_nil_end. refl. intros. simpl sub. rewrite !vars_fun. hyp. refl. intros. simpl. rewrite H, svars_app. f_equal. hyp. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)