proposition: Lemma fpickP : fpick_spec (fpick).
proof: Proof. rewrite /fpick; case (fset0Vmem _) => [H|[x Hx]]. - constructor => x Hx. apply: contraT. rewrite negbK => px. suff: x \in fset0 by rewrite inE. rewrite -H !inE; bcase. - rewrite inE in Hx; constructor; bcase. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)