 The secret to Gentzen’s Hauptsatz is the symmetry of left and right rules for all the logical connectives including negation. The proof of the cut elimination theorem is rather intricate as the process of removing cuts interferes with the structural rules. It is contraction that accounts for the high cost of eliminating cuts. Let \(\lvert \cD\rvert\) be the height of the deduction \(\cD\) and let \(rank(\cD)\) be the supremum of the lengths of cut formulae occurring in \(\cD\). Turning \(\cD\) into a cut-free deduction of the same end sequent results, in the worst case, in a deduction of height \(\cH(rank(\cD),\lvert \cD\rvert)\) where \(\cH(0,n)=n\) and \(\cH(k+1,n)=4^{\cH(k,n)}\), yielding hyper-exponential growth.