Function vstd::seq::axiom_seq_index_decreases

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