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