[proofplan]
Assume an arbitrary proposition $A$ and an inhabitant $h : A \vee \neg A$. We prove $\neg A \vee \neg\neg A$ by [disjunction elimination](/theorems/4625) on $h$. If $h$ gives $\neg A$, we inject it into the left side of the target disjunction. If $h$ gives $A$, we construct $\neg\neg A$ by sending any proof of $\neg A$ to a contradiction, and then inject this double negation into the right side.
[/proofplan]
[step:Assume an excluded-middle instance for an arbitrary proposition]
Let $A$ be an arbitrary proposition. By definition, $\neg A$ denotes the proposition $A \to \bot$, and $\neg\neg A$ denotes $(A \to \bot) \to \bot$.
Assume
\begin{align*}
h : A \vee \neg A.
\end{align*}
It remains to construct an inhabitant of $\neg A \vee \neg\neg A$.
[/step]
[step:Eliminate the disjunction into the target weak excluded-middle disjunction]
We argue by disjunction elimination on $h : A \vee \neg A$.
First suppose $h = \operatorname{inr}(n_A)$, where $n_A : \neg A$. Define
\begin{align*}
w := \operatorname{inl}(n_A) : \neg A \vee \neg\neg A.
\end{align*}
Second suppose $h = \operatorname{inl}(a)$, where $a : A$. Define
\begin{align*}
d_A : \neg\neg A
\end{align*}
by the rule
\begin{align*}
d_A(k) := k(a)
\end{align*}
for every $k : \neg A$. This is well-defined because $k : \neg A$ means $k : A \to \bot$, and therefore $k(a) : \bot$. Hence
\begin{align*}
w := \operatorname{inr}(d_A) : \neg A \vee \neg\neg A.
\end{align*}
By disjunction elimination applied to $h$, these two constructions determine an inhabitant of $\neg A \vee \neg\neg A$.
[guided]
We need to transform a proof of $A \vee \neg A$ into a proof of $\neg A \vee \neg\neg A$. The only information contained in
\begin{align*}
h : A \vee \neg A
\end{align*}
is that one of the two disjuncts has been supplied, so the correct intuitionistic rule to use is disjunction elimination: prove the desired conclusion from each possible disjunct.
In the first case, suppose $h$ supplies the right disjunct of $A \vee \neg A$. Thus
\begin{align*}
h = \operatorname{inr}(n_A)
\end{align*}
for some $n_A : \neg A$. Since the target proposition is $\neg A \vee \neg\neg A$, a proof of its left disjunct is already enough. Therefore the left injection gives
\begin{align*}
\operatorname{inl}(n_A) : \neg A \vee \neg\neg A.
\end{align*}
In the second case, suppose $h$ supplies the left disjunct of $A \vee \neg A$. Thus
\begin{align*}
h = \operatorname{inl}(a)
\end{align*}
for some $a : A$. We do not necessarily have $\neg A$, so we prove the right disjunct $\neg\neg A$. By definition,
\begin{align*}
\neg\neg A = (A \to \bot) \to \bot.
\end{align*}
Thus we must construct a map from $\neg A$ to $\bot$. Let $k : \neg A$ be arbitrary. Since $\neg A$ means $A \to \bot$, the term $k$ is a function that takes any proof of $A$ to a contradiction. Applying $k$ to the available proof $a : A$ gives
\begin{align*}
k(a) : \bot.
\end{align*}
Therefore the assignment $k \mapsto k(a)$ defines a proof
\begin{align*}
d_A : \neg\neg A.
\end{align*}
Using the right injection into the target disjunction, we obtain
\begin{align*}
\operatorname{inr}(d_A) : \neg A \vee \neg\neg A.
\end{align*}
Both cases produce an inhabitant of $\neg A \vee \neg\neg A$. Hence disjunction elimination applied to $h : A \vee \neg A$ yields the desired conclusion.
[/guided]
[/step]
[step:Discharge the assumption to obtain the implication]
Since the construction above starts with an arbitrary proof $h : A \vee \neg A$ and returns a proof of $\neg A \vee \neg\neg A$, it defines a proof of
\begin{align*}
(A \vee \neg A) \to (\neg A \vee \neg\neg A).
\end{align*}
Because $A$ was arbitrary, the theorem holds for every proposition $A$.
[/step]
