pub broadcast proof fn axiom_spec_slice_index<T>(slice: &[T], i: int)Expand description
ensures
0 <= i < spec_slice_len(slice) ==> (#[trigger] spec_slice_index(slice, i)) == slice@[i],