no goals
l r : List Char
⊢ { s := { data := List.reverseAux l r }, i := { byteIdx := utf8Len l } } =
    { s := { data := List.reverse l ++ r }, i := { byteIdx := utf8Len (List.reverse l) } }
simp [List.reverseAux_eq]