 It is clear from Gentzen (1934) that he was aware of the normalization theorem, but he did not publish a proof, or even a precise formulation, of it. The reason would seem to be that he despaired of proving an analogous result for the system of natural deduction for classical logic, and so developed his sequent calculus systems. For these he was able to prove a result for both the classical and intuitionistic variants (his Hauptsatz) which is analogous to the normalization theorem, and useful for some of the same applications. A proof of the normalization theorem was finally published by Prawitz (1965), but it turns out that Gentzen himself had written out a detailed proof in 1933, which is very similar to that given by Prawitz. Jan von Plato discovered Gentzen’s manuscript and published it (von Plato 2008). (Gentzen’s presentation of the proof is very clear, and evidences a strong visual imagination: it is a pleasure to read.)