no goals
s : String
⊢ (toSubstring s).str.data = [] ++ s.data ++ []
simp [toSubstring]
no goals
s : String
⊢ (toSubstring s).stopPos.byteIdx = utf8Len [] + utf8Len s.data
simp [toSubstring, endPos, utf8ByteSize]