pub open spec fn is_valid_bmp_chars(chars: Seq<char>) -> bool
{ forall |i: int| 0 <= i < chars.len() ==> is_bmp_char(#[trigger] chars[i]) }