 The Cut rule differs from the other rules in an important respect. With the rules for introducing connectives, one sees that every formula that occurs above the line occurs below the line either directly, or as a subformula of a formula below the line. That is also true for the structural rules. (Here \(A(t)\) is counted as a subformula, in a slightly extended sense, of both \(\exists xA(x)\) and \(\forall xA(x)\).) But in the case of the Cut rule, the cut formula A vanishes. Gentzen showed that such “vanishing rules” can be eliminated.