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