 Prawitz (1965) proved a normalization theorem for a system of classical natural deduction with a reduced set of logical operators. (The operators, \(\lor\) and \(\exists\), that he omitted can be defined, in classical logic, in terms of the others, so Prawitz’s result is strong enough for some applications.) Several later writers proved normalization results for classical logic with all the usual operators, but under various restrictions. It thus came as a surprise to the logical community when von Plato and Siders (2012) were able to give a very simple proof of a fully general normalization theorem for a system of classical logic including all the usual operators.