[proofplan] We prove the statement by unpacking the constructive meaning of implication. A construction of $\bot \to P$ is a method which turns any construction of $\bot$ into a construction of $P$. Since $\bot$ has no constructions, there are no input cases to handle; formally, the required method is exactly the eliminator for absurdity, specialized to the target proposition $P$. [/proofplan] [step:Fix the proposition and interpret the implication as a transformation of constructions] Let $P$ be an arbitrary proposition. Under the constructive interpretation of implication, to construct $\bot \to P$ is to give a rule which, for every hypothetical construction $b$ of $\bot$, produces a construction of $P$. Thus it is enough to define a map \begin{align*} \operatorname{exfalso}_P : \bot \to P. \end{align*} [guided] We first isolate what must be constructed. The proposition $P$ is arbitrary, so the construction cannot use any special feature of $P$. A construction of an implication $A \to B$ is not a truth-table argument; it is a procedure which accepts a construction of $A$ and returns a construction of $B$. Here the antecedent is $A = \bot$ and the consequent is $B = P$. Therefore a construction of $\bot \to P$ is precisely a rule of the following form: \begin{align*} \operatorname{exfalso}_P : \bot \to P. \end{align*} This means: if a construction $b : \bot$ were supplied, the rule would have to output a construction of $P$. The key point is that $\bot$ is the absurdity proposition, so there are no genuine constructions $b : \bot$. The next step turns this absence of input cases into a formally valid construction. [/guided] [/step] [step:Define the construction by eliminating the hypothetical absurdity] Let $b : \bot$ be a hypothetical construction of absurdity. By bottom elimination, specialized to the proposition $P$, the hypothesis $b : \bot$ determines a construction \begin{align*} \bot\operatorname{-elim}_P(b) : P. \end{align*} Define \begin{align*} \operatorname{exfalso}_P : \bot &\to P \end{align*} \begin{align*} b &\mapsto \bot\operatorname{-elim}_P(b). \end{align*} This is a construction of $\bot \to P$. [guided] We now define the required transformation. Suppose, hypothetically, that we are given a construction $b : \bot$. The proposition $\bot$ is absurdity: it has no constructors, and its elimination principle says that from a construction of $\bot$ one may construct an object of any proposition. Applying this elimination principle with target proposition $P$ gives \begin{align*} \bot\operatorname{-elim}_P(b) : P. \end{align*} This is not an extra assumption about $P$. The target $P$ is arbitrary because the eliminator for $\bot$ has no cases to analyze: there is no constructor of $\bot$ whose behavior must be specified. Hence the rule \begin{align*} \operatorname{exfalso}_P : \bot &\to P \end{align*} \begin{align*} b &\mapsto \bot\operatorname{-elim}_P(b) \end{align*} is a well-defined construction of the implication $\bot \to P$. [/guided] [/step] [step:Conclude the construction exists for every proposition] Since $P$ was arbitrary, the assignment \begin{align*} P \mapsto \operatorname{exfalso}_P \end{align*} gives, for every proposition $P$, a construction \begin{align*} \operatorname{exfalso}_P : \bot \to P. \end{align*} Therefore every proposition follows constructively from absurdity. [/step]