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