[proofplan] We prove the double negation directly: assume a refuter $h : \neg(P \vee \neg P)$ and derive absurdity. Under this assumption, we first construct a refuter of $P$ by showing that any $p : P$ would give the left injection into $P \vee \neg P$, contradicting $h$. Then this constructed $\neg P$ gives the right injection into $P \vee \neg P$, again contradicting $h$. [/proofplan] [step:Assume a refuter of excluded middle] Let $P$ be a proposition. By the definition of negation, to construct $\neg\neg(P \vee \neg P)$ it suffices to construct a map $((P \vee \neg P) \to \bot) \to \bot$. Thus let $h : (P \vee \neg P) \to \bot$ be arbitrary. We must construct an element of $\bot$. [/step] [step:Construct $\neg P$ from the assumed refuter] Define a construction $n_P : P \to \bot$ as follows. Given an arbitrary proof $p : P$, the left introduction rule for disjunction gives $\operatorname{inl}(p) : P \vee \neg P$. Applying $h$ to this disjunction proof gives $h(\operatorname{inl}(p)) : \bot$. Therefore $n_P(p) := h(\operatorname{inl}(p))$ defines a proof of $\neg P$. [guided] The temporary assumption $h$ says that every attempted proof of $P \vee \neg P$ produces absurdity. To build $\neg P$, we must build a map from $P$ to $\bot$. So assume, temporarily, that $p : P$ is given. From $p$, the left injection rule for disjunction constructs $\operatorname{inl}(p) : P \vee \neg P$. But $h$ is precisely a function whose input is a proof of $P \vee \neg P$ and whose output is absurdity. Applying it to $\operatorname{inl}(p)$ gives $h(\operatorname{inl}(p)) : \bot$. Since an arbitrary proof $p : P$ has been transformed into an element of $\bot$, the assignment $p \mapsto h(\operatorname{inl}(p))$ is a construction of $P \to \bot$. By the definition of negation, this is a construction of $\neg P$. [/guided] [/step] [step:Contradict the refuter using the right injection] Since $n_P : \neg P$, the right introduction rule for disjunction gives $\operatorname{inr}(n_P) : P \vee \neg P$. Applying $h$ once more yields $h(\operatorname{inr}(n_P)) : \bot$. Thus every assumed $h : \neg(P \vee \neg P)$ produces absurdity, so we have constructed $\neg\neg(P \vee \neg P)$. This construction does not produce a proof of $P \vee \neg P$ itself; it only shows that refuting $P \vee \neg P$ is impossible. [/step]