pub broadcast proof fn encode_utf8_push(chars: Seq<char>, c: char)Expand description
ensures
#[trigger] encode_utf8(chars.push(c)) == encode_utf8(chars) + encode_scalar(c as u32),Specialization of encode_utf8_concat for appending one char.