= Solution
A common-context <sequent> version of the <disjunction elimination rule> is
$$
\boxed{\frac{\Gamma\vdash\phi\lor\psi\qquad\Gamma,\phi\vdash\kappa\qquad\Gamma,\psi\vdash\kappa}{\Gamma\vdash\kappa}.}
$$
The second and third premises record exactly the two boxed <subproofs> of the <natural deduction> presentation. Their additional case assumptions do not occur in the conclusion: that is <assumption discharge>. The surrounding context $\Gamma$ remains throughout. A formulation with different surrounding contexts is equivalent after retaining their union by <weakening>.
Back to article page
