Function lemma_slice_index_decreases 

pub broadcast proof fn lemma_slice_index_decreases<T>(s: &[T], i: int)

requires

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

ensures

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

A slice can decrease to any of its elements, obtained by indexing.