pub broadcast proof fn lemma_array_index<T, const N: usize>(a: [T; N], i: int)
0 <= i < N,
a[i] == array_view(a)[i],