Function axiom_range_inclusive_empty_contains 

pub broadcast proof fn axiom_range_inclusive_empty_contains<Idx: Ord>(
    r: &RangeInclusive<Idx>,
    item: &Idx,
)

requires

obeys_cmp::<Idx>(),

spec_range_inclusive_is_empty(r),

ensures

!#[trigger] r.contains_spec(item),

An empty range contains nothing when Idx is totally ordered.