Function spec_range_inclusive_unspecified_bounds 

pub uninterp spec fn spec_range_inclusive_unspecified_bounds<T>(
    r: &RangeInclusive<T>,
) -> (Bound<&T>, Bound<&T>)