Function vstd::seq::axiom_seq_subrange_decreases

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