have : s.stopPos < s.str.endPos := by
  simp [v.stopPos, v.str]
  have : 0 < String.csize c := String.csize_pos c
  omega
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
⊢ 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 s.expand