proposition: Lemma is_sol_solved_eqns_map : forall s n u, s n = sub s u -> forall l, is_sol_solved_eqns s (map (solved_eqn_sub (single n u)) l) <-> is_sol_solved_eqns s l.
proof: Proof. induction l; simpl. tauto. destruct a. unfold is_sol_solved_eqn. simpl. split_all; try tauto. rewrite H0, sub_sub. apply sub_eq. intros. unfold sub_comp, single. case_beq_nat n x; auto. rewrite H0, sub_sub. apply sub_eq. intros. unfold sub_comp, single. case_beq_nat n x; auto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)