Function spec_range_inclusive_unspecified_contains 

pub uninterp spec fn spec_range_inclusive_unspecified_contains<Idx, U: ?Sized>(
    r: &RangeInclusive<Idx>,
    item: &U,
) -> bool