no goals
cs cs' : List Char
⊢ prev { data := cs ++ cs' } { byteIdx := utf8Len cs } = { byteIdx := utf8Len (List.dropLast cs) }
match cs, cs.eq_nil_or_concat with
| _, .inl rfl => rfl
| _, .inr ⟨cs, c, rfl⟩ => simp [prev_of_valid]
no goals
cs cs' : List Char
⊢ prev { data := [] ++ cs' } { byteIdx := utf8Len [] } = { byteIdx := utf8Len (List.dropLast []) }
rfl
no goals
cs✝ cs' cs : List Char
c : Char
⊢ prev { data := cs ++ [c] ++ cs' } { byteIdx := utf8Len (cs ++ [c]) } =
    { byteIdx := utf8Len (List.dropLast (cs ++ [c])) }
simp [prev_of_valid]