[proofplan]
Apply the Goedel-Gentzen negative translation theorem to the given classical derivation. This gives an intuitionistic derivation of the translated conclusion from the translated assumptions. Then use the assumed equivalences between each formula and its negative translation to replace the translated assumptions and translated conclusion by the original formulas.
[/proofplan]
[step:Translate the classical derivation]
Assume $\Gamma\vdash_{\mathrm{CL}} N$. By the Goedel-Gentzen negative translation theorem, there is an intuitionistic derivation
\begin{align*}
\Gamma^N\vdash_{\mathrm{IL}} N^N,
\end{align*}
where $\Gamma^N=\{B^N:B\in\Gamma\}$. This is the only use of classical soundness under negative translation.
[/step]
[step:Derive translated assumptions from the original assumptions]
Work now in intuitionistic logic with assumptions $\Gamma$. For each $B\in\Gamma$, the hypothesis gives an intuitionistic proof of $B\to B^N$. Since $B$ is available as an assumption, modus ponens gives $B^N$. Therefore every translated assumption needed by the derivation of $N^N$ is derivable from the original assumptions $\Gamma$.
[/step]
[step:Obtain the translated conclusion]
Substitute the derivations of the translated assumptions from the previous step into the translated derivation
\begin{align*}
\Gamma^N\vdash_{\mathrm{IL}} N^N.
\end{align*}
Cut elimination is not needed; ordinary composition of natural-deduction derivations gives
\begin{align*}
\Gamma\vdash_{\mathrm{IL}} N^N.
\end{align*}
Thus the original assumptions intuitionistically imply the negative translation of the conclusion.
[/step]
[step:Return from the translated conclusion to the original conclusion]
The invariance hypothesis applied to $N$ gives an intuitionistic proof of
\begin{align*}
N^N\to N.
\end{align*}
Composing this implication with the derivation of $N^N$ from $\Gamma$ yields
\begin{align*}
\Gamma\vdash_{\mathrm{IL}} N.
\end{align*}
This is the desired conservativity conclusion.
[/step]
[step:Summarize the conservativity argument]
The proof first translates the classical derivation, then replaces translated assumptions by original assumptions using the invariance hypotheses, and finally replaces the translated conclusion by the original conclusion using the same invariance hypothesis.
[guided]
Assume $\Gamma\vdash_{\mathrm{CL}}N$. The Goedel-Gentzen theorem gives an intuitionistic derivation
\begin{align*}
\Gamma^N\vdash_{\mathrm{IL}}N^N.
\end{align*}
For each assumption $B\in\Gamma$, the invariance hypothesis contains an intuitionistic proof of $B\to B^N$. Therefore, working from the original assumptions $\Gamma$, we can derive every translated assumption $B^N$ needed in the translated derivation.
Composing those derivations with the translated derivation gives
\begin{align*}
\Gamma\vdash_{\mathrm{IL}}N^N.
\end{align*}
The same invariance hypothesis applied to the conclusion gives an intuitionistic proof of $N^N\to N$. A final composition therefore yields
\begin{align*}
\Gamma\vdash_{\mathrm{IL}}N.
\end{align*}
This proves the desired conservativity statement.
[/guided]
[/step]
