proposition: Lemma sig2_eqW (vT : eqType) (P : pred T) (lhs rhs : T -> vT) : (exists2 x, P x & lhs x = rhs x) -> {x | P x & lhs x = rhs x}.
proof: Proof. move=> exP; suffices [x Px /eqP Ex]: {x | P x & lhs x == rhs x} by exists x. by apply: sig2W; have [x Px /eqP Ex] := exP; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)