unfold expand
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ ValidFor l (m ++ [c]) r s.expand
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ ValidFor l (m ++ [c]) r
    (if s.stopPos < s.str.endPos then { str := s.str, startPos := s.startPos, stopPos := s.str.next s.stopPos } else s)