proposition: Lemma lforall_notin_solved_eqn_2 : forall n t, mem n (vars t) = false -> forall x l, lforall (notin_solved_eqn n) l -> lforall (notin_solved_eqn n) (map (solved_eqn_sub (single x t)) l).
proof: Proof. induction l; simpl. auto. destruct a. intuition. unfold notin_solved_eqn in H1. simpl in H1. unfold notin_solved_eqn. simpl. split_all. apply mem_vars_sub_single; hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)