proposition: Lemma is_sol_eqns_map : forall s x u, s x = sub s u -> forall l, is_sol_eqns s (map (eqn_sub (single x u)) l) <-> is_sol_eqns s l.
proof: Proof. induction l; simpl. tauto. destruct a as [t0 t1]. unfold is_sol_eqn. simpl. split_all; try tauto. rewrite !sub_sub in H0. trans (sub (sub_comp s (single x u)) t0). sym. apply sub_comp_single. hyp. rewrite H0. apply sub_comp_single. hyp. rewrite !sub_sub. trans (sub s t0). apply sub_comp_single. hyp. rewrite H0. sym. apply sub_comp_single. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)