pub broadcast proof fn is_ascii_chars_nat_bound(chars: Seq<char>)Expand description
ensures
#[trigger] is_ascii_chars(chars)
==> forall |i: int| 0 <= i < chars.len() ==> (chars.index(i) as nat) < 128,Ensures that all characters in an ASCII character sequence have a numerical representation that falls in the range 0 (inclusive) to 128 (exclusive).