  Gentzen called the analogue of normalization by the unimaginative  name of Hauptsatz, “main theorem”. The standard  terminology today is “cut elimination theorem” All of the logical rules of SC have the subformula property in a very immediate  sense: each formula in a premiss is a formula or subformula in the  conclusion. The rule for combining derivations, analogous to the one  explained above for the case of detour conversions in ND, is called  “cut”. In it, a formula A appears as a case in a first premiss and as an assumption in a second premiss. In the  conclusion, this formula has disappeared and the assumptions of the  two premisses collected together: