  Ketonen's proof of invertibility of the logical rules of his sequent  calculus used the structural rule of cut. Later Kurt Schütte  (1950) and Haskell Curry (1963) gave direct proofs of invertibility,  the latter with the explicit result that the inversions are height preserving: if a given sequent is derivable in at most n steps, the premisses in a rule that can conclude that sequent also  have a derivation in at most n steps.