Function vstd::seq::axiom_seq_subrange_index

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