Function vstd::std_specs::vecdeque::axiom_vec_dequeue_index_decreases

source · 
pub broadcast proof fn axiom_vec_dequeue_index_decreases<A>(v: VecDeque<A>, i: int)
Expand description
requires
0 <= i < v.len(),
ensures
#[trigger] (decreases_to!(v => v[i])),