$\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$