proposition: Lemma vars_subs_intro : forall s x y, mem x (vars (s y)) = true -> forall v : term, mem y (vars v) = true -> mem x (vars (sub s v)) = true.
proof: Proof. intros s x y H v. pattern v; apply term_ind with (Q := fun n (ts : terms n) => mem y (vars_vec ts) = true -> mem x (vars_vec (Vmap (sub s) ts)) = true); clear v. intro. simpl. mem. intro. subst. hyp. intros f ts IH. rewrite sub_fun, !vars_fun. hyp. simpl. auto. simpl. intros u n us IH1 IH2. mem. intro. destruct (orb_true_elim H0). rewrite (IH1 e). refl. rewrite (IH2 e). bool. refl. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)