proposition: Lemma sig2W P Q : (exists2 x, P x & Q x) -> {x | P x & Q x}.
proof: Proof. move=> exPQ; have [|x /andP[]] := @sigW (predI P Q); last by exists x. by have [x Px Qx] := exPQ; exists x; apply/andP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)