Function valid_utf8_split 

pub broadcast proof fn valid_utf8_split(bytes: Seq<u8>, index: int)

requires

valid_utf8(bytes),

is_char_boundary(bytes, index),

ensures

valid_utf8(bytes[..index]),

valid_utf8(bytes[index..]),

Ensures that the two subsequences formed by splitting a valid UTF-8 byte sequence at a character boundary are also valid UTF-8 byte sequences.