pub broadcast proof fn range_set_properties<A: FiniteRange>(lo: A, hi: A)Expand description
ensures
(#[trigger] A::range_set(lo, hi)).finite(),A::range_set(lo, hi).len() == A::range_len(lo, hi),