proposition: Lemma iter_step_wf : forall p k, problem_wf p -> problem_wf (iter_step k p).
proof: Proof. induction k; simpl; intuition. apply step_wf. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)