proposition: Lemma powersetE X Y : (X \in powerset Y) = (X `<=` Y).
proof: Proof. case: Y => ys ax_ys. rewrite /powerset !set_ofE /=. apply/mapP/subP => [ [ t t1 ->] x | H ] /=. - rewrite set_ofE. exact: mem_mask. - exists [tuple of map (mem X) (in_tuple ys)]; first by rewrite !mem_enum. apply: fset_ext => x. rewrite set_ofE /= -filter_mask mem_filter /=. case: (boolP (x \in X)) => // inX. by rewrite H. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)