Function vstd::set_lib::lemma_set_propertiesCopy item path

forall |a: Set<A>, b: Set<A>| #[trigger] a.union(b).union(b) == a.union(b),

forall |a: Set<A>, b: Set<A>| #[trigger] a.union(b).union(a) == a.union(b),

forall |a: Set<A>, b: Set<A>| #[trigger] (a.intersect(b)).intersect(b) == a.intersect(b),

forall |a: Set<A>, b: Set<A>| #[trigger] (a.intersect(b)).intersect(a) == a.intersect(b),

forall |s1: Set<A>, s2: Set<A>, a: A| s2.contains(a) ==> !s1.difference(s2).contains(a),

forall |a: Set<A>, b: Set<A>| {
    a.disjoint(b)
        ==> ((#[trigger] (a + b)).difference(a) == b && (a + b).difference(b) == a)
},

forall |s: Set<A>| #[trigger] s.len() != 0 && s.finite() ==> exists |a: A| s.contains(a),

forall |a: Set<A>, b: Set<A>| {
    (a.finite() && b.finite() && a.disjoint(b))
        ==> #[trigger] (a + b).len() == a.len() + b.len()
},

forall |a: Set<A>, b: Set<A>| {
    (a.finite() && b.finite())
        ==> #[trigger] (a + b).len() + #[trigger] a.intersect(b).len()
            == a.len() + b.len()
},

forall |a: Set<A>, b: Set<A>| {
    (a.finite() && b.finite())
        ==> ((#[trigger] a.difference(b).len() + b.difference(a).len()
            + a.intersect(b).len() == (a + b).len())
            && (a.difference(b).len() == a.len() - a.intersect(b).len()))
},