proposition: Lemma powerset_size X : size (powerset X) = 2 ^ (size X).
proof: Proof. rewrite /powerset size_of_uniq. - by rewrite size_map -cardE card_tuple card_bool. - rewrite map_inj_uniq ?enum_uniq //. move: (elements X) (funiq X) => {X} s uniq_s m1 m2 => H. have {H} E : mask m1 s =i mask m2 s. move => x. by rewrite -set_ofE H set_ofE. apply/eqP. apply: mask_inj E; by rewrite // size_tuple. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)