r : List Char
it : Iterator
h : ValidFor [] r it
⊢ ValidFor [] r { s := { data := r }, i := 0 }
r : List Char
it : Iterator
h : ValidFor [] r it
⊢ ValidFor [] r (Iterator.prev it)
simp [Iterator.prev, h.toString, h.pos]
no goals
r : List Char
it : Iterator
h : ValidFor [] r it
⊢ ValidFor [] r { s := { data := r }, i := 0 }
constructor