Function vstd::seq_lib::lemma_seq_take_len
source · pub proof fn lemma_seq_take_len<A>(s: Seq<A>, n: int)Expand description
ensures
0 <= n <= s.len() ==> s.take(n).len() == n,Taking the first n elements of a sequence results in a sequence of length n,
as long as n is within the bounds of the original sequence.