Function vstd::array::lemma_array_index

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