pub broadcast proof fn encode_utf8_concat(a: Seq<char>, b: Seq<char>)Expand description
ensures
#[trigger] encode_utf8(a + b) == encode_utf8(a) + encode_utf8(b),encode_utf8 distributes over sequence concatenation.