[proofplan]
We prove the implication by taking evidence $d$ of the decidability statement $P \vee \neg P$ and evidence $h$ of $\neg\neg P$. The proof then performs [disjunction elimination](/theorems/4625) on $d$. In the left branch, evidence of $P$ is already available; in the right branch, the refutation of $P$ contradicts $h$, and falsity elimination gives evidence of $P$.
[/proofplan]
[step:Assume decidability and double negation evidence]
Let $P$ be a proposition. Assume $d$ is evidence of $P \vee \neg P$. To construct evidence of $\neg\neg P \to P$, assume $h$ is evidence of $\neg\neg P$. Since $\neg P$ means $P \to \bot$, the term $h$ is a function that sends any evidence of $\neg P$ to evidence of $\bot$.
[/step]
[step:Eliminate the decision of $P$ by cases]
We eliminate the disjunction $d : P \vee \neg P$.
If $d$ is given by the left injection, then there is evidence $p$ of $P$. In this branch we return $p$.
If $d$ is given by the right injection, then there is evidence $k$ of $\neg P$, that is, $k : P \to \bot$. Since $h : \neg\neg P$, applying $h$ to $k$ gives evidence $h(k)$ of $\bot$. By the intuitionistic elimination rule for falsity, evidence of $\bot$ yields evidence of any proposition, in particular evidence of $P$. Thus this branch also produces evidence of $P$.
[guided]
We now use the only available information about $P$: the decision evidence $d : P \vee \neg P$. Since $d$ is evidence of a disjunction, intuitionistic disjunction elimination permits us to prove $P$ by proving $P$ separately from each possible form of $d$.
First suppose $d$ is evidence of the left side of the disjunction. Then $d$ supplies a term $p : P$. No further argument is needed in this branch: the required output is evidence of $P$, and $p$ is exactly such evidence.
Second suppose $d$ is evidence of the right side of the disjunction. Then $d$ supplies a term $k : \neg P$. By the definition of negation, this means $k : P \to \bot$. The hypothesis $h : \neg\neg P$ means $h : \neg P \to \bot$, again by the definition of negation. Therefore $h$ can be applied to $k$, producing a contradiction:
\begin{align*}
h(k) : \bot.
\end{align*}
At this point we use the intuitionistic elimination rule for falsity: from evidence of $\bot$, one may construct evidence of any proposition. Applying that rule to the proposition $P$ and the contradiction $h(k) : \bot$, we obtain evidence of $P$.
Both branches of the case analysis therefore produce evidence of $P$. Hence disjunction elimination applied to $d : P \vee \neg P$ produces evidence of $P$ under the assumption $h : \neg\neg P$.
[/guided]
[/step]
[step:Discharge the assumptions to obtain stability]
Starting from arbitrary evidence $h : \neg\neg P$, the case analysis above constructs evidence of $P$. Therefore we have constructed evidence of $\neg\neg P \to P$. Since this construction used only the assumed evidence $d : P \vee \neg P$, we have constructed evidence of
\begin{align*}
(P \vee \neg P) \to (\neg\neg P \to P).
\end{align*}
This proves that every decidable proposition is stable.
[/step]
