Function spec_range_inclusive_is_empty 

pub open spec fn spec_range_inclusive_is_empty<Idx>(r: &RangeInclusive<Idx>) -> bool

{ r@.exhausted || spec_range_inclusive_out_of_order(r) }