I am interested in equivalently transforming $\Sigma^1_{n+1}$ formulas $\exists Y\;\psi(X,Y)$ (with $\psi$ being $\Pi^1_n$) in the form $\exists Y\;\psi'(X,Y)$, where $\psi'$ is $\Pi^1_n$ and $\psi'(X,Y)\land \psi'(X,Y')\to Y=Y'$.
If we have (effective enough) lightface $\Pi^1_n$ uniformatization then there is a straightforward way to put each $\Sigma^1_{n+1}$ formula in this unique witness form (for a given formula $\exists Y\;\psi(X,Y)$ we take the uniformization of $\psi(X,Y)$ as $\psi'(X,Y)$). But of course generally $\psi'(X,Y)$ is not necessary a uniformization of $\psi(X,Y)$.
My question is whether there is essentially different way of putting $\Sigma^1_{n+1}$ formulas in unique witness form? And whether there are interesting examples of theories where for some $n$ it is possible to equivalently transform $\Sigma^1_{n+1}$ formulas in unique witness form but not possible to prove uniformization? More specifically is it possible to put $\Sigma^1_3$ formulas in unique witness form over $\mathsf{ZFC}$?