Function vstd::seq_lib::lemma_seq_properties

forall |s: Seq<A>, x: A| {
    s.contains(x) <==> exists |i: int| 0 <= i < s.len() && #[trigger] s[i] == x
},

forall |x: A| !(#[trigger] Seq::<A>::empty().contains(x)),

forall |s: Seq<A>| #[trigger] s.len() == 0 ==> s =~= Seq::<A>::empty(),

forall |x: Seq<A>, y: Seq<A>, elt: A| {
    #[trigger] (x + y).contains(elt) <==> x.contains(elt) || y.contains(elt)
},

forall |s: Seq<A>, v: A, x: A| {
    (#[trigger] s.push(v).contains(x) <==> v == x || s.contains(x)) && #[trigger]
        s.push(v).contains(v)
},

forall |s: Seq<A>, start: int, stop: int, x: A| {
    (0 <= start <= stop <= s.len() && #[trigger] s.subrange(start, stop).contains(x))
        <==> (exists |i: int| 0 <= start <= i < stop <= s.len() && #[trigger] s[i] == x)
},

forall |s: Seq<A>, n: int| 0 <= n <= s.len() ==> #[trigger] s.take(n).len() == n,

forall |s: Seq<A>, n: int, x: A| {
    (#[trigger] s.take(n).contains(x) && 0 <= n <= s.len())
        <==> (exists |i: int| 0 <= i < n <= s.len() && #[trigger] s[i] == x)
},

forall |s: Seq<A>, n: int, j: int| {
    0 <= j < n <= s.len() ==> #[trigger] s.take(n)[j] == s[j]
},

forall |s: Seq<A>, n: int| {
    0 <= n <= s.len() ==> #[trigger] s.skip(n).len() == s.len() - n
},

forall |s: Seq<A>, n: int, x: A| {
    (#[trigger] s.skip(n).contains(x) && 0 <= n <= s.len())
        <==> (exists |i: int| 0 <= n <= i < s.len() && #[trigger] s[i] == x)
},

forall |s: Seq<A>, n: int, j: int| {
    0 <= n && 0 <= j < (s.len() - n) ==> #[trigger] s.skip(n)[j] == s[j + n]
},

forall |a: Seq<A>, b: Seq<A>, n: int| {
    n == a.len() ==> ((a + b).take(n) =~= a && (a + b).skip(n) =~= b)
},

forall |s: Seq<A>, i: int, v: A, n: int| {
    0 <= i < n <= s.len() ==> #[trigger] s.update(i, v).take(n) == s.take(n).update(i, v)
},

forall |s: Seq<A>, i: int, v: A, n: int| {
    0 <= n <= i < s.len() ==> #[trigger] s.update(i, v).take(n) == s.take(n)
},

forall |s: Seq<A>, i: int, v: A, n: int| {
    0 <= n <= i < s.len()
        ==> #[trigger] s.update(i, v).skip(n) == s.skip(n).update(i - n, v)
},

forall |s: Seq<A>, i: int, v: A, n: int| {
    0 <= i < n <= s.len() ==> #[trigger] s.update(i, v).skip(n) == s.skip(n)
},

forall |s: Seq<A>, v: A, n: int| {
    0 <= n <= s.len() ==> #[trigger] s.push(v).skip(n) == s.skip(n).push(v)
},

forall |s: Seq<A>, n: int| n == 0 ==> #[trigger] s.skip(n) == s,

forall |s: Seq<A>, n: int| n == 0 ==> #[trigger] s.take(n) == Seq::<A>::empty(),

forall |s: Seq<A>, m: int, n: int| {
    (0 <= m && 0 <= n && m + n <= s.len()) ==> s.skip(m).skip(n) == s.skip(m + n)
},

forall |s: Seq<A>, a: A| {
    #[trigger] (s.push(a).to_multiset()) =~= s.to_multiset().insert(a)
},

forall |s: Seq<A>| s.len() == #[trigger] s.to_multiset().len(),

forall |s: Seq<A>, a: A| s.contains(a) <==> #[trigger] s.to_multiset().count(a) > 0,