proposition: Lemma wf_iter_step : forall p, exists k, solved (iter_step k p) = true.
proof: Proof. intro. ded (wf_Lt' p). elim H; clear H p; intros. destruct x. 2: exists 0; refl. destruct p. destruct e. exists 0; refl. set (p := Some (s, e::e0)). case_eq (solved (step p)); intro H1. exists 1. unfold iter_step. hyp. destruct (H0 (step p) (Lt_step (solved_inv H1))). exists (S x). simpl. rewrite <- iter_step_commut. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)