$ \def\imp{\Rightarrow} \def\celse{\ |\ } \def\prov{\vdash} \def\dns{{\downarrow}} \def\preq{\dashv\vdash} \def\sh{\#} $
Source Language
The source language is the small focused first-order logic FF described in Focus-preserving Embeddings of Substructural Logics in Intuitionistic Logic. Its syntax goes like this:
Negative $N$$::=$$P \imp N \celse N \land N \celse \top \celse \forall x . N(x) \celse a^-(t)$
Positive $P$$::=$$\dns N \celse a^+(t)$
Terms $t$$::=$$x \celse \cdots$
It has negative connectives, and both polarities of atoms. First-order terms can be built from variables and whatever term constructors you like.
Target Language
The target language is just ordinary unpolarized first-order intuitionistic logic, with one nonstandard connective, a U-quantifier:
Propositions $A,B,C$$::=$$A \imp A \celse A \land A \celse A \lor A \celse \top \celse \bot \celse \forall x . A(x) \celse \exists x . A(x)\celse Ux.A(x)\celse a(t)$
The rules for $U$ feature a distinguished atomic proposition $\sh$ that takes one term argument. $${ \Gamma, A(x) \prov \sh(x) \over \Gamma \prov Ux.A(x) }{\small(x\not\in\Gamma)}\qquad { \Gamma\prov A(t) \over \Gamma, Ux.A(x) \prov \sh(t) }$$ Naturally, it is easy to show that $Ux.A(x) \preq \forall x . A(x) \imp \sh(x)$, but the presentation of $U$ as a 'jumbo' connective is important for the isomorphism proof.
Abbrevs and Translation
We mutually recursively make the abbreviation $$N^\ast = Ux.N^x$$ and define $P^\ast$, $P^\circ$, $N^t$, $N^\circ$ by
$N$$N^ t$$N^\circ$
$P \imp N$ $P^\ast \land N^t$ $P^\circ \imp N^\circ$
$N_1 \land N_2$ $N_1^t \lor N_2^t$ $N_1^\circ \land N_2^\circ$
$\top$ $\bot$ $\top$
$\forall x . N(x)$ $\exists x . N^t(x)$ $\forall x . N^\circ(x)$
$a^-$ $a^-(t)$ $(a^-)^\ast$
$P$$P^\ast$$P^\circ$
$\dns N$ $N^\circ$ $N^\ast$
$a^+$ $a^+$ $a^+$
We're abusing notation a little by acting like that the $a^-$ and $a^+$ in the source language don't have arguments. What's really going on in the translation of $a^-$ is we're adding one more argument to the list, and with $a^+$ preserving the set of arguments.
Translation of sequents
$N_1\ldots, N_n\prov a^-$$N_1^\ast, \ldots, N_n^\ast, a^-(x) \prov \sh(x)$
$N_1\ldots, N_n[N]\prov a^-$$N^\ast_1, \ldots, N^\ast_n, a^-(x) \prov N^x$
$N_1\ldots, N_n\prov N$$N^\ast_1, \ldots, N^\ast_n\prov N^\circ$
$N_1\ldots, N_n\prov [P]$$N^\ast_1, \ldots, N^\ast_n\prov P^\ast$
Theorems
Proving these establishes cut and identity for FF, and are super easy to prove by induction:
$P^\ast \preq P^\circ$
$N^\ast \preq N^\circ$