pub proof fn lemma_flatten_cardinality_under_disjointness<A>(parts: Set<Set<A>>)Expand description
requires
parts.finite(),pairwise_disjoint(parts),forall |p: Set<A>| #[trigger] parts.contains(p) ==> p.finite(),parts.flatten().len() == parts.fold(0nat, |acc: nat, p: Set<A>| acc + p.len()),parts.flatten().finite(),If parts is a finite set of finite, pairwise-disjoint sets,
then the cardinality of the union is the sum of cardinalities.