Function spec_range_inclusive_start_bound 

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

{
    if spec_range_inclusive_is_empty(r) {
        spec_range_inclusive_unspecified_bounds(r).0
    } else {
        Bound::Included(&r@.start)
    }
}