Function vstd::seq_lib::lemma_seq_take_index

source ·

pub proof fn lemma_seq_take_index<A>(s: Seq<A>, n: int, j: int)

Expand description

ensures

0 <= j < n <= s.len() ==> s.take(n)[j] == s[j],

If j is a valid index less than n, then the jth element of the sequence s is the same as jth element of the sequence after taking the first n elements of s.