It is my first approach to the proof theory of intuitionistic logic and I am considering a single-conclusioned Gentzen-style sequent calculus for it, namely $\bf G3i$ (Negri, Von Plato, Structural Proof Theory, p. 28).
By applying root-first the rules of $\bf G3i$, it turns out that the formula $A\lor (A\to B)$ is not derivable.
I understand the motivation behind the rejection of other laws such as ($A\lor \neg A$) or ($\neg\neg A\to A$), but I am struggling to see the point with $A\lor (A\to B)$.
Why is this the case? Are there some specific discussions in the literature fixing this?
Thank you!!
Assume that it is derivable and replace $B$ with $\bot$.
What you get is $A \lor (A \to \bot)$ contradicting the underivability of LEM.