proposition: Lemma iter_step_solved_eqn_wf : forall p l k, problem_wf p -> iter_step k p = Some (l, nil) -> solved_eqns_wf l.
proof: Proof. intros. ded (iter_step_wf p k H). rewrite H0 in H1. simpl in H1. tauto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)