Function axiom_slice_get_range_to_inclusive 

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

ensures

i.end < v@.len()
    ==> {
        &&& (#[trigger] spec_slice_get(v, i)).is_some()
        &&& spec_slice_get(v, i).unwrap()@ == v@.subrange(0, i.end as int + 1)

    },

!(i.end < v@.len()) ==> spec_slice_get(v, i).is_none(),