proposition: Lemma iter_step_most_general : forall p l k, problem_wf p -> iter_step k p = Some (l, nil) -> forall s, is_sol s p -> forall x, s x = sub (theta l s) (subst_of_solved_eqns l x).
proof: Proof. intros. apply subst_of_solved_eqns_most_general. eapply iter_step_solved_eqn_wf; ehyp. cut (is_sol s (Some (l, nil))). simpl. tauto. rewrite <- H0, <- iter_step_correct. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)