proposition: Lemma iter_step_None : forall p k, iter_step k p = None -> forall s, ~is_sol s p.
proof: Proof. intros. intro. rewrite (iter_step_correct s p k), H in H0. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)