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