Function lemma_array_index_decreases 

pub broadcast proof fn lemma_array_index_decreases<T, const N: usize>(a: &[T; N], i: int)

requires

0 <= i < a@.len(),

ensures

#[trigger] (decreases_to!(a => a @ [i])),

An array can decrease to any of its elements, obtained by indexing.