∀ {l m r : List Char} (s : Substring.Raw),
  s.str.toList = l ++ m ++ r →
    s.startPos.byteIdx = String.utf8Len l →
      s.stopPos.byteIdx = String.utf8Len l + String.utf8Len m → Substring.Raw.ValidFor l m r s