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