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.