 Given the simplicity of von Plato and Siders’s technique, it is somewhat surprising that it took so long to discover a method of normalizing natural deduction. Perhaps the barrier was psychological: the intuitively obvious part of the Gentzen/Prawitz normalization of intuitionistic logic is in the immediate reductions, the permutative reductions in contrast being perceived as annoying technical details needed for a few rules. So perhaps logicians didn’t find it natural to use permutative-style reductions more generally. In this connection, it is perhaps significant that von Plato (2001) had worked with systems having what are called general elimination rules. Here the other elimination rules are replaced by rules more in the spirit of \(\lor\)-E: the conclusion, which need not be an immediate subformula of the (major) premise, is derived in a subproof having hypotheses sufficient for obtaining that premise by the corresponding Introduction rule, and is taken to be established in the main proof by the existence of the subproof. This was of course not a logically necessary prerequisite—normalization holds both for classical natural deduction with general rules and, as we have seen, for a more standard formulation of classical natural deduction—but psychologically it may have made it easy to see how the problem could be solved.