proposition: Lemma successfull_is_sol : forall k p, problem_wf p -> successfull (iter_step k p) = true -> exists s, is_sol s p.
proof: Proof. intros. destruct (successfull_elim H0). exists (subst_of_solved_eqns x). eapply subst_of_solved_eqns_correct_problem. hyp. apply H1. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)