proposition: Lemma lforall_notin_solved_eqn_1' : forall n t, mem n (vars t) = false -> forall l' l, lforall (notin ((Var n, t) :: l')) l -> lforall (notin_solved_eqn n) (map (solved_eqn_sub (single n t)) l).
proof: Proof. induction l; simpl. auto. destruct a. simpl. unfold notin_eqn. simpl. mem. intros. unfold notin_solved_eqn. simpl. split_all. subst n0. rewrite (beq_refl beq_nat_ok) in H0. discr. apply mem_vars_sub_single'; hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)