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.