Function axiom_slice_get_range_to 

pub broadcast proof fn axiom_slice_get_range_to<T>(v: &[T], i: RangeTo<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)

    },

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