simp [v.stopPos, v.str, String.next]
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 { str := s.str, startPos := s.startPos, stopPos := s.str.next s.stopPos }
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
    { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
      stopPos :=
        { byteIdx := String.utf8Len l + String.utf8Len m } +
          { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } }