 We use upper case Greek letters \(\Gamma,\Delta,\Lambda,\Theta,\Xi\ldots\) to range over finite lists of formulae. \(\Gamma\subseteq \Delta\) means that every formula of \(\Gamma\) is also a formula of \(\Delta\). A sequent is an expression \(\Gamma\Rightarrow \Delta\) where \(\Gamma\) and \(\Delta\) are finite sequences of formulae \(A_1,\ldots,A_n\) and \(B_1,\ldots, B_m\), respectively. We also allow for the possibility that \(\Gamma\) or \(\Delta\) (or both) are empty. The empty sequence will be denoted by \(\emptyset\). \(\Sigma \Rightarrow \Delta\) is read, informally, as \(\Gamma\) yields \(\Delta\) or, rather, the conjunction of the \(A_i\) yields the disjunction of the \(B_j\).