proposition: Lemma fin_choices (T : finType) (P : T -> Prop) (Pdec : forall x, P x \/ ~ P x) : exists A : {set T}, forall x, x \in A <-> P x.
proof: Proof. pose R x (b :bool) := b <-> P x. have/fin_choice [f Hf]: forall x, exists b, R x b. move => x. case (Pdec x); [by exists true|by exists false]. exists (finset f) => x. rewrite inE. exact: Hf. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)