c : Char
it : Iterator
h✝ : Valid it
l r : List Char
h : ValidFor l r it
⊢ Valid (Iterator.setCurr it c)
c : Char
it : Iterator
h : Valid it
⊢ Valid (Iterator.setCurr it c)
let ⟨l, r, h⟩ := h.validFor
no goals
c : Char
it : Iterator
h✝ : Valid it
l r : List Char
h : ValidFor l r it
⊢ Valid (Iterator.setCurr it c)
exact h.setCurr'.valid