[proofplan] We pass from a closed natural-deduction derivation to the single-succedent LJ sequent calculus, where closed derivability of a formula $C$ corresponds to derivability of the sequent $\Rightarrow C$. Cut elimination then permits us to replace the LJ derivation of $\Rightarrow A \lor B$ by a cut-free one. In a cut-free derivation whose antecedent is empty and whose succedent is a disjunction, inspection of the last inference forces the final rule to be one of the two right-introduction rules for $\lor$. The premise of that last rule is therefore either $\Rightarrow A$ or $\Rightarrow B$, and translating back to natural deduction gives a closed proof of the corresponding disjunct. [/proofplan] [step:Translate the closed intuitionistic proof into a single-succedent LJ derivation] Let $\mathcal{L}_{\mathrm{IPC}}$ denote the propositional language generated from propositional variables by $\land$, $\lor$, $\to$, and $\bot$. Let $A, B \in \mathcal{L}_{\mathrm{IPC}}$ be formulas, and assume $\vdash_{\mathrm{IPC}} A \lor B$. Fix the standard single-succedent LJ sequent calculus for intuitionistic propositional logic. A sequent has the form $\Gamma \Rightarrow C$, where $\Gamma$ is a finite list, multiset, or set of formulas and $C$ is either empty or a single formula, according to the chosen standard presentation. We use only the single-succedent case with succedent formula present. By the equivalence between natural deduction and LJ for intuitionistic propositional logic (citing a result not yet in the wiki: Equivalence of Natural Deduction and LJ for Intuitionistic Propositional Logic), the closed natural-deduction derivation of $A \lor B$ yields an LJ derivation $\mathcal{D}$ of the sequent $\Rightarrow A \lor B$. [/step] [step:Remove cuts from the LJ derivation] By cut elimination for LJ (citing a result not yet in the wiki: Cut Elimination for LJ), applied to the LJ derivation $\mathcal{D}$ of $\Rightarrow A \lor B$, there exists a cut-free LJ derivation $\mathcal{D}_0$ with the same end-sequent $\Rightarrow A \lor B$. The hypotheses of cut elimination are met because $\mathcal{D}$ is an LJ derivation in the fixed single-succedent intuitionistic sequent calculus. Thus $\mathcal{D}_0$ is a cut-free derivation of exactly the sequent $\Rightarrow A \lor B$. [/step] [step:Inspect the final inference of the cut-free derivation] We claim that the final inference of $\mathcal{D}_0$ must be one of the two right-introduction rules for disjunction. Since the end-sequent is $\Rightarrow A \lor B$, its antecedent is empty and its succedent formula is the disjunction $A \lor B$. The final inference cannot be a cut, because $\mathcal{D}_0$ is cut-free. It cannot be an initial axiom, since an initial axiom in LJ has a formula occurring in the antecedent, for example $C \Rightarrow C$, while the end-sequent has empty antecedent. It cannot be a left-introduction rule, because every left-introduction rule has as its principal formula a formula in the antecedent of the conclusion, and the conclusion here has no antecedent formula. It cannot be a structural rule on the antecedent producing this conclusion: exchange and contraction do not change the set of antecedent formulas, and weakening adds formulas to the antecedent rather than removing all of them. Therefore the last inference is a right-introduction rule whose principal formula is the succedent formula $A \lor B$. In the standard LJ calculus, the only right-introduction rules with principal succedent formula a disjunction are $\lor R_1$ and $\lor R_2$. Hence the last inference is either \begin{align*} \frac{\Rightarrow A}{\Rightarrow A \lor B}\ \lor R_1 \end{align*} or \begin{align*} \frac{\Rightarrow B}{\Rightarrow A \lor B}\ \lor R_2. \end{align*} [guided] The purpose of passing to a cut-free LJ derivation is that cut-free proofs have a strong last-rule discipline: the final connective of the succedent cannot appear by a hidden detour through a cut. Here the end-sequent of $\mathcal{D}_0$ is $\Rightarrow A \lor B$, so the formula displayed on the right is built by the outer connective $\lor$. We now check all possible forms of the final inference. It is not a cut, because $\mathcal{D}_0$ was chosen cut-free. It is not an initial axiom: an LJ initial axiom has a formula available on the left, such as $C \Rightarrow C$, but the sequent $\Rightarrow A \lor B$ has empty antecedent. It is not a left-introduction rule, because a left-introduction rule introduces or analyzes a principal formula in the antecedent of its conclusion, and there is no antecedent formula in $\Rightarrow A \lor B$. It is not an antecedent structural rule. Exchange and contraction cannot change an empty antecedent into a nonempty one or conversely, and weakening on the left only adds formulas to the antecedent, so it cannot have $\Rightarrow A \lor B$ as its conclusion unless the premise already has the same empty antecedent; in the usual formulation, weakening has nonempty conclusion antecedent when it acts nontrivially. Thus the last inference must introduce the succedent formula. Since the succedent formula is $A \lor B$, the only LJ rules that can introduce it on the right are the two disjunction-right rules. The first has premise $\Rightarrow A$ and conclusion $\Rightarrow A \lor B$; the second has premise $\Rightarrow B$ and conclusion $\Rightarrow A \lor B$. Consequently the cut-free derivation $\mathcal{D}_0$ contains, immediately above its last inference, either a derivation of $\Rightarrow A$ or a derivation of $\Rightarrow B$. [/guided] [/step] [step:Extract a closed derivation of one disjunct] If the final inference of $\mathcal{D}_0$ is $\lor R_1$, then its premise is an LJ derivation of $\Rightarrow A$. By the LJ-to-natural-deduction direction of the same equivalence theorem (citing a result not yet in the wiki: Equivalence of Natural Deduction and LJ for Intuitionistic Propositional Logic), this yields a closed intuitionistic natural-deduction derivation of $A$, so $\vdash_{\mathrm{IPC}} A$. If the final inference of $\mathcal{D}_0$ is $\lor R_2$, then its premise is an LJ derivation of $\Rightarrow B$. Translating this derivation back to natural deduction yields a closed intuitionistic derivation of $B$, so $\vdash_{\mathrm{IPC}} B$. These are the only two possible final inferences, so from $\vdash_{\mathrm{IPC}} A \lor B$ we obtain $\vdash_{\mathrm{IPC}} A$ or $\vdash_{\mathrm{IPC}} B$. This proves the disjunction property. [/step]