Function spec_range_inclusive_end_bound 

pub open spec fn spec_range_inclusive_end_bound<T>(r: &RangeInclusive<T>) -> Bound<&T>

{ if r@.exhausted { Bound::Excluded(&r@.end) } else { Bound::Included(&r@.end) } }