Function axiom_slice_get_range_from 

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

ensures

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

    },

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