Function vstd::std_specs::vec::axiom_vec_index_decreases
source · pub broadcast proof fn axiom_vec_index_decreases<A>(v: Vec<A>, i: int)Expand description
requires
0 <= i < v.len(),#[trigger] (decreases_to!(v => v[i])),