pub broadcast proof fn axiom_vec_index_decreases<A>(v: Vec<A>, i: int)
0 <= i < v.len(),
#[trigger] (decreases_to!(v => v[i])),