proposition: Lemma iter_step_Some : 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. rewrite (iter_step_correct (subst_of_solved_eqns l) p k), H0. simpl. split_all. apply subst_of_solved_eqns_correct. eapply iter_step_solved_eqn_wf; ehyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)