Proving $\lnot\lnot(A\lor\lnot A)$ in intuitionistic sequent calculus with cut seems to be easy: We use cut to prove $\lnot(A\lor\lnot A)\vdash \bot$ from $\lnot(A\lor\lnot A)\vdash \lnot A \land\lnot\lnot A$ and $\lnot A \land\lnot\lnot A\vdash \bot$.
But how can one ever prove $\lnot(A\lor\lnot A)\vdash \bot$ without using cut? Without cut, the only way to prove it seems to be to derive it from $\vdash A\lor\lnot A$. But that sequent is not valid. I guess there must be some other way to prove it without cut that I just fail to see. (My reasoning is that I am pretty certain that $\lnot\lnot(A\lor\lnot A)$ and $\lnot(A\lor\lnot A)\vdash \bot$ are valid in intuitionistic logic, even if my proof with cut should be incorrect.)
I initially suspected that I am missing some rule(s) related to $\bot$, but the proof with cut still seems to go through unchanged if $\bot$ is replaced by $C$ and $\lnot X$ by $X\to C$. (Both $B\land(B\to C)\vdash C$ and $(A\lor B)\to C \vdash (A\to C) \land (B\to C)$ are easy to prove, and replacing $B$ by $(A\to C)$ and using cut like before still gives $(A\lor(A\to C))\to C\vdash C$.)
