Function vstd::seq_lib::lemma_seq_skip_contains

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