Function partial_valid_utf8_extend 

pub broadcast proof fn partial_valid_utf8_extend(bytes: Seq<u8>, i: int)

requires

#[trigger] partial_valid_utf8(bytes, i),

#[trigger] valid_first_scalar(bytes[i..]),

ensures

#[trigger] partial_valid_utf8(bytes, i + length_of_first_scalar(bytes[i..])),

Ensures that if the prefix of a byte sequence is valid UTF-8, and remainder of the sequence begins with a valid UTF-8 encoding of a single scalar, then the prefix extended by that scalar encoding is also valid UTF-8.