pub broadcast proof fn encode_utf8_decode_utf8(chars: Seq<char>)Expand description
ensures
#[trigger] decode_utf8(encode_utf8(chars)) == chars,Ensures that performing encode_utf8 followed by decode_utf8 results in the original char sequence.