Equivalence between $\neg\neg\bot$ and $\bot$ in intuitionistic logic. As the title says, why are those two equivalent? I can find a simple derivation (using natural deduction) of $\bot$ from $\neg\neg\bot$, but i fail at proving the other implication.
 A: (a) One of the rules of inference in standard natural deduction systems for intuitionistic logic is ex falso quodlibet, i.e.

From $\bot$ infer $\varphi$ for any $\varphi$.

So, as a particular application, we have a one-step derivation of, in particular,  $\neg\neg\bot$ from $\bot$.
(b) As you say the other direction is also intuitionistically provable. Thus $\bot$ trivially entails $\bot$ so (by the intuitionistically acceptable version of reductio that if you can infer $\bot$ from $\psi$, then that gives you $\neg\psi$), $\neg\bot$ is a theorem. But then $\neg\neg\bot$ as an assumption, combined with this theorem (so a pair of the form $\neg\psi$, $\psi$) gives you $\bot$ (by the introduction rule for $\bot$).
A: The $\bot \to \neg\neg\bot$ implication is a special case of $\forall \alpha.\ \forall \beta.\ \alpha \to (\beta \to \alpha)$.
Below there are both derivations using Curry-Howard isomorphism. 
Formula 
$$((\bot \to \bot) \to \bot) \to \bot$$ 
is a special case of 
$$\forall \beta.\ \forall \alpha.\ ((\alpha \to \alpha) \to \beta) \to \beta $$
which can be proved by $\lambda$-term
$$\lambda f.\ f\ (\lambda x.\ x)$$
The other implication
$$\bot \to ((\bot \to \bot) \to \bot)$$
is a special case of
$$\forall \beta.\ \forall \alpha.\ \beta \to (\alpha \to \beta)$$
which can be proved by $\lambda$-term
$$\lambda x. \lambda f.\ x$$
I hope this helps $\ddot\smile$
