Function vstd::set_lib::lemma_set_disjoint_lens
source · pub proof fn lemma_set_disjoint_lens<A>(a: Set<A>, b: Set<A>)Expand description
requires
a.finite(),b.finite(),a.disjoint(b) ==> (a + b).len() == a.len() + b.len(),If sets a and b are disjoint, meaning they share no elements in common, then the length
of the union a + b is equal to the sum of the lengths of a and b.