fact: Definition powerset X : {fset {fset T}} := let e := elements X in let mT := ((size e).-tuple bool) in set_of (map (fun m : mT => set_of (mask m e)) (enum {: mT})).
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)