no goals
l m r : List Char
⊢ l ++ (m ++ r) =
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
            stopPos := { byteIdx := utf8Len l + utf8Len m } }.str.data ∧
    { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
            stopPos := { byteIdx := utf8Len l + utf8Len m } }.startPos.byteIdx =
      utf8Len l
simp
no goals
l m r : List Char
⊢ l ++ m ++ r =
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
            stopPos := { byteIdx := utf8Len l + utf8Len m } }.str.data ∧
    { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
            stopPos := { byteIdx := utf8Len l + utf8Len m } }.stopPos.byteIdx =
      utf8Len (l ++ m)
simp