proposition: Lemma notin_map x t : mem x (vars t) = false -> forall l, notin (map (eqn_sub (single x t)) l) (x, t).
proof: Proof. induction l; simpl. trivial. destruct a. unfold notin_eqn. simpl. split_all. trans (mem x (if mem x (vars t0) then union (vars t) (remove x (vars t0)) else vars t0)). apply mem_m. refl. apply vars_single. case_eq (mem x (vars t0)); intro H0. mem. rewrite H, H0. refl. hyp. trans (mem x (if mem x (vars t1) then union (vars t) (remove x (vars t1)) else vars t1)). apply mem_m. refl. apply vars_single. case_eq (mem x (vars t1)); intro H0. mem. rewrite H, H0. refl. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)