Function axiom_slice_get_range 

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

ensures

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

    },

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