Function lemma_encode_bmp_string_valid 

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

requires

is_valid_bmp_chars(chars),

ensures

is_valid_bmp_string(encode_bmp_string(chars)),