Function spec_range_inclusive_end_bound 

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

{
    if spec_range_inclusive_is_empty(r) {
        spec_range_inclusive_unspecified_bounds(r).1
    } else {
        Bound::Included(&r@.end)
    }
}