Function vstd::set_lib::lemma_set_disjoint
source · pub proof fn lemma_set_disjoint<A>(a: Set<A>, b: Set<A>)Expand description
ensures
a.disjoint(b) ==> ((a + b).difference(a) =~= b && (a + b).difference(b) =~= a),If sets a and b are disjoint, meaning they have no elements in common, then the set difference
of a + b and b is equal to a and the set difference of a + b and a is equal to b.