have ⟨c, r', heq⟩ := List.exists_cons_of_ne_nil this
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : ¬r = []
⊢ ∃ r', r = it.curr :: r'
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : ¬r = []
c : Char
r' : List Char
heq : r = c :: r'
⊢ ∃ r', r = it.curr :: r'