∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Finite α m] {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)}
  {it it' : Std.IterM m β},
  it'.IsPlausibleSuccessorOf it →
    InvImage WellFoundedRelation.rel
      (Std.IterM.finitelyManySteps ∘ Std.Iterators.Types.TakeWhile.inner ∘ Std.IterM.internalState) it' it