have : 0 < String.csize c := String.csize_pos c
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))
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : 0 < String.csize c
⊢ String.utf8Len l + String.utf8Len m < String.utf8Len l + (String.utf8Len m + (String.utf8Len r + String.csize c))