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