∀ {m : Type → Type u_1} {s : String.Slice} [inst : Pure m] {it it' : Std.IterM m { p // p ≠ s.endPos }},
  it'.IsPlausibleSuccessorOf it →
    InvImage WellFoundedRelation.rel (fun it => s.utf8ByteSize - it.internalState.currPos.offset.byteIdx) it' it