[proofplan] Transport the translated hypotheses back to the original hypotheses. From each assumption $G\in\Gamma$, the derivation $G\vdash G^N$ gives the corresponding member of $\Gamma^N$. By weakening and cut, any derivation from $\Gamma^N$ may therefore be used under assumptions $\Gamma$. Apply this to the assumed derivation $\Gamma^N\vdash\neg\neg N$, then cut with the stability derivation $\vdash\neg\neg N\to N$. [/proofplan] [step:Derive each translated hypothesis from the original context] Let $G \in \Gamma$. By hypothesis, there is an intuitionistic derivation \begin{align*} G \vdash G^N. \end{align*} Weakening this derivation by the other assumptions in $\Gamma$ gives \begin{align*} \Gamma \vdash G^N. \end{align*} Thus every formula in the translated context $\Gamma^N$ is derivable from the original context $\Gamma$. [guided] For each $G \in \Gamma$, the theorem supplies a derivation $G \vdash G^N$. The structural rule of weakening lets the same derivation run with all assumptions in $\Gamma$ available, so $\Gamma \vdash G^N$. Therefore each member $G^N$ of $\Gamma^N=\{G^N:G\in\Gamma\}$ can be derived from $\Gamma$. [/guided] [/step] [step:Transport the translated proof to the original context] The hypothesis $\Gamma^N \vdash \neg\neg N$ is a derivation whose open assumptions are formulas of the form $G^N$ with $G \in \Gamma$. For each such open assumption, substitute the derivation $\Gamma \vdash G^N$ constructed in the previous step. Repeated applications of cut eliminate the translated assumptions and produce \begin{align*} \Gamma \vdash \neg\neg N. \end{align*} [guided] Start with the derivation $\Gamma^N \vdash \neg\neg N$. Whenever it uses an assumption $G^N \in \Gamma^N$, replace that assumption by the already constructed derivation $\Gamma \vdash G^N$. The cut rule performs this replacement inside intuitionistic logic. After all translated assumptions are replaced, the resulting derivation has only assumptions from $\Gamma$ and concludes $\neg\neg N$, so $\Gamma \vdash \neg\neg N$. [/guided] [/step] [step:Use stability of the negative conclusion] By stability of $N$, we have a derivation \begin{align*} \vdash \neg\neg N \to N. \end{align*} Cutting this derivation with the derivation $\Gamma \vdash \neg\neg N$ from the previous step gives \begin{align*} \Gamma \vdash N. \end{align*} [guided] The previous step gives $\Gamma \vdash \neg\neg N$. The stability hypothesis gives the derivation $\vdash \neg\neg N \to N$. Using implication elimination under the assumptions $\Gamma$, or equivalently applying one more cut to these two derivations, converts the derived double negation into the target conclusion and yields $\Gamma \vdash N$. [/guided] [/step] [step:Conclude the reformulation principle] We have derived $N$ from the original assumptions $\Gamma$ using only the derivability of each translated hypothesis from its original form, the translated proof of $\neg\neg N$, and stability of $N$. Therefore $\Gamma\vdash N$, as required. [/step]