proposition: Lemma card_fpowerset (A : {fset K}) : #|` fpowerset A| = 2 ^ #|` A|.
proof: Proof. rewrite !card_imfset; first by rewrite -cardE card_powerset cardsE cardfE. by move=> X Y /fsetP eqXY; apply/setP => x; have := eqXY (val x); rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)