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