case refl
l r : List Char
h : ValidFor l r { s := { data := List.reverseAux l r }, i := { byteIdx := utf8Len l } }
⊢ Iterator.remainingToString { s := { data := List.reverseAux l r }, i := { byteIdx := utf8Len l } } = { data := r }
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ Iterator.remainingToString it = { data := r }
cases h.out
no goals
case refl
l r : List Char
h : ValidFor l r { s := { data := List.reverseAux l r }, i := { byteIdx := utf8Len l } }
⊢ Iterator.remainingToString { s := { data := List.reverseAux l r }, i := { byteIdx := utf8Len l } } = { data := r }
simpa [Iterator.remainingToString, List.reverseAux_eq] using extract_of_valid l.reverse r []