proposition: Lemma vars_subs_elim : forall s x (v : term), mem x (vars (sub s v)) = true -> exists y, mem y (vars v) = true /\ mem x (vars (s y)) = true.
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)) = true -> exists y, mem y (vars_vec ts) = true /\ mem x (vars (s y)) = true); clear v. simpl. intros. exists x0. mem. tauto. intros f ts IH. rewrite sub_fun, !vars_fun. intro. destruct (IH H). exists x0. hyp. simpl. mem. discr. simpl. intros u n us IH1 IH2. mem. intro. destruct (orb_true_elim H). destruct (IH1 e). exists x0. mem. intuition. destruct (IH2 e). exists x0. mem. intuition. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)