Here, $\psi$ is some arbitrary formula.
The proof I've come up with is as follows.
Assume $\lnot \lnot (\psi \lor \lnot \psi)$ is not a theorem of IPL, which means there exists some Kripke model where
$$\exists w: w \not\models \lnot \lnot (\psi \lor \lnot \psi),$$
which, by definition of negation being truthful in Kripke models, is equivalent to
$$\exists w: \exists u \geq w: u \models \lnot (\psi \lor \lnot \psi).$$
This, again by definition of negation truthfulness, implies for this $u$ that
$$\forall v \geq u : v \not \models \psi \lor \lnot \psi.$$
By definition of truthfulness of $\lor$ in Kripke models, this, in turn, implies
$$\forall v \geq u : v \not \models \psi, v \not \models \lnot \psi.$$
But if $\forall v \geq u : v \not \models \psi$, then $u \models \lnot\psi$, which contradicts $\forall v \geq u : v \not \models \lnot \psi$.
Hence, the original assumption is false, and $\lnot \lnot (\psi \lor \lnot \psi)$ is a theorem of IPL.
Is this reasoning correct?
To prove $\lnot \lnot (P \lor \lnot P)$, assume $\lnot (P \lor \lnot P)$ and show that it leads to a contradiction.
Under that assumption, you can show both $\lnot P$ holds by contradiction as well as $\lnot \lnot P$ holds, which is the desired contradiction. In long form:
$$ \begin{array} {rl} % Markup \begin{array} {r} \begin{array} {r|} \text{Assumption } \\ \hline \begin{array} {r|} \text{Assumption } \\ \hline \text{Or Intro } \\ \text{Contradiction } \\ \end{array} \\ \text{Negation Intro } \\ \begin{array} {r|} \text{Assumption } \\ \hline \text{Or Intro } \\ \text{Contradiction } \\ \end{array} \\ \text{Negation Intro } \\ \text{Contradiction } \\ \end{array} \\ \text{Negation Intro } \end{array} & % Proof \begin{array} {l} \begin{array} {|l} \lnot (P \lor \lnot P) \\ \hline \begin{array} {|l} P \\ \hline P \lor \lnot P \\ \bot \\ \end{array} \\ \lnot P \\ \begin{array} {|l} \lnot P \\ \hline P \lor \lnot P \\ \bot \\ \end{array} \\ \lnot \lnot P \\ \bot \\ \end{array} \\ \lnot \lnot (P \lor \lnot P) \end{array} % End Proof \end{array}$$