proposition: Lemma cardfE : size (enum_fset A) = #|fset_sub_type|.
proof: Proof. by rewrite cardE enum_fsetE size_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)