no goals
l m r : List Char
⊢ Substring.toString
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
        stopPos := { byteIdx := utf8Len l + utf8Len m } } =
    { data := m }
simpa [Substring.toString] using extract_of_valid l m r