Function vstd::set_lib::lemma_set_disjoint
source · pub broadcast 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.