 There are two variant forms of the complication. (1) A formula is obtained by an introduction rule and then reiterated into the subproof, and then used as the major premiss of an elimination rule there: the needed immediate reduction for this introduction-elimination detour isn’t possible because the material (premiss, premises, subproof) needed isn’t available in the subproof of the \(\lor\)-E or \(\exists\)-E. (Note that this problem can’t arise if we have a Gentzen-style presentation of natural deduction: where a Fitch-style derivation uses reiteration to get a second copy of a formula, the Gentzen-style derivation just repeats the whole argumentation leading to the formula above each of its occurrences.) The fix for this is conceptually simple (though in some cases it can lead to an increase in total derivation size, since it can involve installing multiple copies of many formulas): instead of reiterating the formula into the subproof, reiterate whatever was needed to derive it, derive it by the introduction rule within the subproof, and proceed to the immediate reduction. (2) The conclusion of the \(\lor\)-E or \(\exists\)-E inference, which is also the last line of the subproof(s), is obtained by an introduction rule inside the subproof, and is then used as the (major) premiss of an elimination rule in the main derivation. Again, an immediate reduction of the detour is not possible: the conclusion is in the main derivation, but the materials needed for its direct derivation are available only in the subproof(s). It is perhaps a little less obvious that the fix for this works, but it is again conceptually simple: do the second elimination inference inside the subproof(s), so its conclusion is the last line of the subproof(s), and then take its conclusion in place of the original as the conclusion of the main \(\lor\)-E or \(\exists\)-E inference. Call modifications of this sort to a derivation permutative reductions. Then the less rough statement of Gentzen’s theorem is that any derivation (in the natural deduction system for intuitionistic logic) can be converted, by a sequence of immediate and permutative reductions, into the normal form, in which no occurrence of a formula is both the conclusion of an introduction rule and the major premiss of an elimination rule. Derivations in normal form have interesting and useful properties. Perhaps the most noteworthy is the subformula property: every formula in a normal derivation is a subformula of (that is, either identical to or a part of) either an undischarged hypothesis or the final conclusion.