no goals
l m r : List Char
⊢ Substring.next
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
        stopPos := { byteIdx := utf8Len l + utf8Len m } }
      { byteIdx := utf8Len m } =
    { byteIdx := utf8Len m }
simp [Substring.next, Pos.add_eq]