pub broadcast proof fn axiom_spec_array_update<T, const N: usize>(array: [T; N], i: int, t: T)Expand description
ensures
0 <= i < N ==> (#[trigger] spec_array_update(array, i, t)@) == array@.update(i, t),