How to prove double negation elimination without using $\bot$? $\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$
I am trying to derive some rules without the use of the $\bot$ symbol.
First I want to describe how I am defining certain inference rules:
Negation Introduction: $\{(a\to b), (a \to \lnot b) \} \vdash \lnot a$:
$$\fitch{}
    {\fitch{a}
    {\vdots
    \\b}
    \\a\to b\\
    {\fitch{a}
    {\vdots
    \\\lnot b}}
\\ a \to \lnot b \\ \lnot a}$$
Now presume that we take the law of excluded middle $a \lor \lnot a$ as an axiom and use it (with negation introduction and disjunction elimination) to prove the double-negation rule:
$$\fitch{\lnot \lnot a}{
    a \lor \lnot a
    \\ \fitch{a}{
        a
    }
    \\ a \to a
    \\ \fitch{\lnot a}{
        \vdots
        \\ a
    }
    \\ \lnot a \to a
    \\ a \text{ (by or-elim using LEM and the two implications)}
}$$
I can't quite figure out how to fill in the dotted section. Normally we'd just restate $\lnot \lnot a$ and note the contradiction with $\lnot a$, state the contradiction $\bot$, and then use ex falso $\bot \to a$ to invoke $a$ and finish the proof.
But without the $\bot$ symbol, is this impossible to do? I don't know how to prove ex falso in the first place without using $\bot$ or double negation elimination which is the very thing I am trying to prove.

This prover is helpful to reply to this question. See example 3
