proposition: Lemma successfull_elim : forall k p, successfull (iter_step k p) = true -> exists l, iter_step k p = Some (l, nil).
proof: Proof. intros. destruct (iter_step k p). destruct p0. destruct e. exists s. refl. discr. discr. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)