proposition: Lemma card_tagged : #|{: {i : I & T_ i}}| = sumn (map (fun i => #|T_ i|) (enum I)).
proof: Proof. rewrite cardE !enumT [in LHS]unlock size_flatten /shape -map_comp. by congr (sumn _); apply: eq_map => i; rewrite /= size_map -enumT -cardE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)