Function vstd::seq_lib::lemma_seq_skip_index

source · 
pub proof fn lemma_seq_skip_index<A>(s: Seq<A>, n: int, j: int)
Expand description
ensures
0 <= n && 0 <= j < (s.len() - n) ==> s.skip(n)[j] == s[j + n],

If j is a valid index less than s.len() - n, then the jth element of the sequence s.skip(n) is the same as the j+nth element of the sequence s.