pub proof fn encode_utf8_first_scalar(chars: Seq<char>)Expand description
requires
chars.len() > 0,decode_first_scalar(encode_utf8(chars)) == chars[0] as u32,length_of_first_scalar(encode_utf8(chars)) == encode_scalar(chars[0] as u32).len(),valid_first_scalar(encode_utf8(chars)),Properties of the first scalar from the result of encode_utf8.