proposition: Lemma iter_step_complete : forall p, problem_wf p -> (exists s, is_sol s p) -> exists k, successfull (iter_step k p) = true.
proof: Proof. intros. destruct H0 as [s]. destruct (wf_iter_step p) as [k]. exists k. rewrite (iter_step_correct s p k) in H0. destruct (iter_step k p). destruct p0. destruct e. refl. discr. contr. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)