proposition: Lemma mem_vars_sub_single' : forall n (u v : term), mem n (vars v) = false -> mem n (vars (sub (single n v) u)) = false.
proof: Proof. intros. trans (mem n (if mem n (vars u) then union (vars v) (remove n (vars u)) else vars u)). apply mem_m. refl. apply vars_single. case_eq (mem n (vars u)); intro H0. mem. rewrite H0, H. refl. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)