subst heq
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'
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this : ¬c :: r' = []
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1