Function axiom_slice_get_range_full 

pub broadcast proof fn axiom_slice_get_range_full<T>(v: &[T], i: RangeFull)

ensures

(#[trigger] spec_slice_get(v, i)).is_some(),

spec_slice_get(v, i).unwrap()@ == v@,