[proofplan] We construct the term directly by function introduction. Starting from an arbitrary proof $p:P$, we must build a proof of $\neg\neg P$, namely a function from $\neg P$ to $\varnothing$. Given such a function $h:\neg P$, unfolding the definition of negation gives $h:P\to\varnothing$, so applying $h$ to $p$ produces an element of $\varnothing$. Abstracting first over $h$ and then over $p$ gives the required term of type $P\to\neg\neg P$. [/proofplan] [step:Unfold double negation as a function type] Let $P$ be an arbitrary proposition, regarded as a type. By definition of negation, \begin{align*} \neg P := P \to \varnothing. \end{align*} Therefore \begin{align*} \neg\neg P = \neg(\neg P) = (P \to \varnothing) \to \varnothing. \end{align*} Thus it is enough to construct a term of type \begin{align*} P \to ((P \to \varnothing) \to \varnothing). \end{align*} [/step] [step:Construct a contradiction from $p:P$ and $h:\neg P$] Assume $p:P$. To construct a term of $\neg\neg P$, assume $h:\neg P$. Since $\neg P := P \to \varnothing$, the term $h$ is a function \begin{align*} h:P \to \varnothing. \end{align*} By function application, applying $h$ to $p$ gives \begin{align*} h(p):\varnothing. \end{align*} Hence, under the assumption $p:P$, the assignment \begin{align*} h \mapsto h(p) \end{align*} defines a term of type \begin{align*} (P \to \varnothing) \to \varnothing. \end{align*} [guided] We need to prove $\neg\neg P$ from an assumed proof of $P$. Since negation is defined as implication into the empty type, the expression $\neg P$ means $P\to\varnothing$. Therefore $\neg\neg P$ means \begin{align*} (P \to \varnothing) \to \varnothing. \end{align*} So, after assuming $p:P$, the task is to construct a function whose input is a term of type $P\to\varnothing$ and whose output is a term of type $\varnothing$. Let \begin{align*} h:P \to \varnothing \end{align*} be such an input. Since $p:P$ and $h$ is a function with domain $P$, function application gives a term \begin{align*} h(p):\varnothing. \end{align*} This is exactly the required output for the assumed input $h$. Therefore the rule of function introduction gives the function \begin{align*} \lambda h.\,h(p):(P \to \varnothing) \to \varnothing. \end{align*} Since $(P\to\varnothing)\to\varnothing$ is $\neg\neg P$, this constructs a term of $\neg\neg P$ from the original assumption $p:P$. [/guided] [/step] [step:Abstract over the proof of $P$] The previous step constructs, from an arbitrary $p:P$, the term \begin{align*} \lambda h.\,h(p):(P \to \varnothing) \to \varnothing. \end{align*} By function introduction over $p$, define \begin{align*} d_P:P \to ((P \to \varnothing) \to \varnothing) \end{align*} by \begin{align*} d_P := \lambda p.\,\lambda h.\,h(p). \end{align*} Using $\neg P := P\to\varnothing$, this is a term \begin{align*} d_P:P \to \neg\neg P. \end{align*} Since $P$ was arbitrary, this proves double negation introduction for every proposition $P$. [/step]