cs cs' : List Char
⊢ { byteIdx := utf8Len cs } + List.headD cs' default = { byteIdx := utf8Len cs + csize (List.headD cs' default) }
cs cs' : List Char
⊢ next { data := cs ++ cs' } { byteIdx := utf8Len cs } = { byteIdx := utf8Len cs + csize (List.headD cs' default) }
simp only [next, get_of_valid]
no goals
cs cs' : List Char
⊢ { byteIdx := utf8Len cs } + List.headD cs' default = { byteIdx := utf8Len cs + csize (List.headD cs' default) }
rfl