Function axiom_slice_get_range_inclusive 

pub broadcast proof fn axiom_slice_get_range_inclusive<T>(v: &[T], i: RangeInclusive<usize>)

ensures

slice_range_valid(&i, v@.len())
    ==> {
        &&& (#[trigger] spec_slice_get(v, i)).is_some()
        &&& spec_slice_get(v, i).unwrap()@
            == v@.subrange(slice_range_start(&i), slice_range_end(&i, v@.len()))

    },

!slice_range_valid(&i, v@.len()) ==> spec_slice_get(v, i).is_none(),