proposition: Lemma iter_step_complete2 : forall p, problem_wf p -> (forall s, ~is_sol s p) -> exists k, iter_step k p = None.
proof: Proof. intros. destruct (wf_iter_step p) as [k]. exists k. case_eq (iter_step k p). 2: refl. intros p0 H2. rewrite H2 in H1. destruct p0. destruct e. ded (iter_step_Some H H2). ded (H0 (subst_of_solved_eqns s)). contr. discr. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)