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