proposition: Lemma all_subP (U : {fset T}) (P : pred _) : reflect (forall X, X `<=` U -> P X) (all P (powerset U)).
proof: Proof. apply: (iffP allP) => [H X /subP sub| H X]. apply H; exact/powersetP. move/powersetP => /subP. exact: H. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)