  Thus, cut is the only rule that makes a formula  “disappear” in a derivation. Gentzen showed that  instances of the rule of cut can be eliminated from derivations by  permuting them upward until they reach points at which the derivation starts. In ND, the starting points are assumptions, in SC they are  “initial sequents” of the form  A → A in which the assumption  formula A is at the same time the conclusion. A cut with  such a sequent as one premiss has the other premiss equal to the  conclusion and can therefore be deleted.