proposition: Lemma card_unionE : #|union_finType| = \sum_(i : TPI) #|TPi i|.
proof: Proof. Proof using. rewrite cardE -(size_map val) /= enum_unionE. rewrite /enum_union size_flatten /shape -map_comp. rewrite (eq_map (g := fun i => #|TPi i|)); first last. by move=> i; rewrite /= size_map cardE. by rewrite sumn_mapE big_enum. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools