pub open spec fn is_ascii_chars(chars: Seq<char>) -> bool
{ forall |i| 0 <= i < chars.len() ==> '\0' <= #[trigger] chars[i] <= '\u{7f}' }
True when the given character sequence only contains ASCII characters.