Function lemma_encode_decode_universal_string 

pub proof fn lemma_encode_decode_universal_string(bytes: Seq<u8>)

requires

is_valid_universal_string(bytes),

ensures

encode_universal_string(decode_universal_string(bytes)) == bytes,