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