proposition: Lemma subst_of_solved_eqns_correct_problem : forall p l k, problem_wf p -> iter_step k p = Some (l, nil) -> is_sol (subst_of_solved_eqns l) p.
proof: Proof. intros. set (s := subst_of_solved_eqns l). rewrite (@iter_step_correct s p k), H0. simpl. split_all. apply subst_of_solved_eqns_correct. assert (problem_wf (Some (l, nil))). rewrite <- H0. apply iter_step_wf. hyp. simpl in H1. tauto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)