 The sequent calculus we have been discussing allows the proof of classically, but not intuitionistically correct formulae, for example, the law of excluded middle. An intuitionist version of the sequent calculus can be obtained by a very simple structural restriction: there can be at most one formula on the right hand side of the sequent symbol \(\Rightarrow\). The cut elimination theorem is also provable for this intuitionist variant. In either case, the Hauptsatz has an important corollary that parallels that of the Normalization theorem (for intuitionist logic) and expresses the subformula property.