Function vstd::seq_lib::lemma_seq_take_contains
source · pub proof fn lemma_seq_take_contains<A>(s: Seq<A>, n: int, x: A)Expand description
requires
0 <= n <= s.len(),s.take(n).contains(x) <==> (exists |i: int| 0 <= i < n <= s.len() && s[i] == x),The resulting sequence after taking the first n elements from sequence s contains
element x if and only if x is contained in the first n elements of s.