∀ {s : String.Slice} {p q : s.Pos} {h : p ≠ s.endPos},
  q.offset.byteIdx - p.offset.byteIdx < (p.get h).utf8Size →
    ¬q.offset.byteIdx - p.offset.byteIdx <
          s.startInclusive.offset.byteIdx + p.offset.byteIdx + (p.get h).utf8Size -
            (s.startInclusive.offset.byteIdx + p.offset.byteIdx) →
      False