Function lemma_encode_universal_string_valid 

pub proof fn lemma_encode_universal_string_valid(chars: Seq<char>)

ensures

is_valid_universal_string(encode_universal_string(chars)),