[proofplan] We build a derivation of $C$ from $\Gamma$ by applying the natural deduction elimination rule for disjunction. The derivation of $A \lor B$ supplies the major premise, while the two derivations of $C$ from $\Gamma \cup \{A\}$ and from $\Gamma \cup \{B\}$ supply the two case branches. The rule discharges the temporary assumptions $A$ and $B$, so every undischarged assumption in the resulting derivation belongs to $\Gamma$. [/proofplan] [step:Choose derivations witnessing the three hypotheses] By the definition of derivability, the hypothesis $\Gamma \vdash A \lor B$ gives a derivation $\mathcal{D}_0$ whose conclusion is $A \lor B$ and whose undischarged assumptions are all elements of $\Gamma$. Similarly, $\Gamma \cup \{A\} \vdash C$ gives a derivation $\mathcal{D}_1$ whose conclusion is $C$ and whose undischarged assumptions are all elements of $\Gamma \cup \{A\}$. Mark every undischarged occurrence of the formula $A$ in $\mathcal{D}_1$ that is not being treated as an assumption from $\Gamma$ as the left temporary case assumption. Finally, $\Gamma \cup \{B\} \vdash C$ gives a derivation $\mathcal{D}_2$ whose conclusion is $C$ and whose undischarged assumptions are all elements of $\Gamma \cup \{B\}$. Mark every undischarged occurrence of the formula $B$ in $\mathcal{D}_2$ that is not being treated as an assumption from $\Gamma$ as the right temporary case assumption. [/step] [step:Apply disjunction elimination to the three derivations] The disjunction elimination rule has the following form: from a derivation of $A \lor B$, a derivation of $C$ from a temporary assumption $A$, and a derivation of $C$ from a temporary assumption $B$, infer $C$, discharging the two temporary assumptions. Apply this rule with $\mathcal{D}_0$ as the derivation of the major premise $A \lor B$, with $\mathcal{D}_1$ as the left case derivation of $C$ from $A$, and with $\mathcal{D}_2$ as the right case derivation of $C$ from $B$. This produces a derivation $\mathcal{D}$ whose final conclusion is $C$. [/step] [step:Check that the resulting derivation has only assumptions from $\Gamma$] The rule application discharges exactly the marked temporary assumptions $A$ in the left branch and $B$ in the right branch. The derivation $\mathcal{D}_0$ had only undischarged assumptions from $\Gamma$. After the discharge, every remaining undischarged assumption in $\mathcal{D}_1$ is an element of $\Gamma$, and every remaining undischarged assumption in $\mathcal{D}_2$ is an element of $\Gamma$. Therefore every undischarged assumption of the combined derivation $\mathcal{D}$ belongs to $\Gamma$. Since $\mathcal{D}$ concludes $C$, the definition of derivability gives $\Gamma \vdash C$. [/step]