Sequent
= Sequent
{title2=$\Gamma\vdash A$}
A <sequent> $\Gamma\vdash A$ records that the formula $A$ is derivable with undischarged assumptions drawn from $\Gamma$. In <natural deduction>, a <temporary assumption> contributes to $\Gamma$ only until an appropriate discharge rule closes its scope.