 Cut elimination works smoothly for \(\bRA^*\), however, the prize one has to pay can only be measured in terms of Veblen’s \(\varphi\) function. The optimal result is the so-called second cut elimination theorem.