∀ {pat s : String.Slice} {stackPos needlePos : String.Pos.Raw} {k : ℕ}
  {hki : needlePos.byteIdx - 1 < pat.copy.toByteArray.size} (p : s.Pos),
  stackPos.byteIdx - p.offset.byteIdx ≤ needlePos.byteIdx - 1 →
    ¬pat.copy.toByteArray.size - (p.offset.byteIdx + pat.copy.toByteArray.size - stackPos.byteIdx) ≤
          needlePos.byteIdx - 1 →
      False