proposition: Lemma emptyPn X : reflect (exists x , x \in X) (X != fset0).
proof: Proof. apply: introP => [|/negPn/eqP-> [x]]; last by rewrite in_fset0. case (fset0Vmem X) => [ -> | [ x inX ] ]; by [rewrite eqxx |exists x]. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)