fact: CoInductive fpick_spec : option T -> Type := | fPick x : p x -> x \in X -> fpick_spec (Some x) | fNopick : (forall x, x \in X -> ~~ p x) -> fpick_spec None.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)