Function spec_range_inclusive_unspecified_ref_bounds 

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