pub proof fn lemma_flatten_cardinality_under_disjointness_same_length<A>(
parts: Set<Set<A>>,
c: nat,
)Expand description
requires
parts.finite(),pairwise_disjoint(parts),parts.all(|p: Set<A>| p.finite() && p.len() == c),parts.flatten().len() == parts.len() * c,parts.flatten().finite(),If parts is a finite set of finite, pairwise-disjoint sets, and each set has the same length c,
then the cardinality of the union is the product of the number of sets and c.