pub broadcast proof fn axiom_spec_slice_update<T>(slice: &[T], i: int, t: T)Expand description
ensures
0 <= i < spec_slice_len(slice)
==> (#[trigger] spec_slice_update(slice, i, t)@) == slice@.update(i, t),