simp [v.stopPos, v.str]
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
⊢ s.stopPos < s.str.endPos
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
⊢ String.utf8Len l + String.utf8Len m < String.utf8Len l + (String.utf8Len m + (String.utf8Len r + String.csize c))