Function vstd::seq_lib::lemma_seq_take_contains
source · pub broadcast proof fn lemma_seq_take_contains<A>(s: Seq<A>, n: int, x: A)Expand description
requires
0 <= n <= s.len(),#[trigger] s.take(n).contains(x)
<==> (exists |i: int| 0 <= i < n <= s.len() && #[trigger] 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.