proposition: Lemma cupP (T T' : choiceType) (X : {fset T}) (P : pred T) (F : T -> {fset T'}) y : reflect (exists x, [&& x \in X , P x & y \in F x]) (y \in \bigcup_(x in X | P x) F x).
proof: Proof. apply: (iffP idP) => [|[x] /and3P [X1 X2 X3]]. - pose Y := [fset x in X | P x && (y \in F x)]. case (fset0Vmem Y) => [Y0|[x]]; last by rewrite inE; exists x. rewrite (bigID (fun z => y \in F z)) -big_sep /= -/Y Y0 fset0Es big_nil fset0U. move => H. exfalso. move: H. apply/negP. apply big_ind => [|? ?|? /andP[//]]; rewrite !inE ?negb_or; bcase. - by rewrite (big_rem x) //= X2 inE X3. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)