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