[proofplan] The reduction removes the immediate detour created by introducing $A \to B$ and then eliminating it with a proof of $A$. The only role of the discharged assumptions in $\Pi$ is that they supply occurrences of $A$; since $\Delta$ is already a derivation of $A$, each such occurrence can be replaced by a fresh copy of $\Delta$. A structural induction on the derivation tree $\Pi$ verifies that the replacement preserves every inference rule above those leaves and changes the open assumptions exactly by replacing the discharged $A$-occurrences with the open assumptions of $\Delta$. [/proofplan] [step:Define the substitution of $\Delta$ for the discharged $A$-occurrences] Let $\mathcal{U}$ denote the distinguished finite family of open assumption occurrences of formula $A$ in $\Pi$ that are discharged by the application of $\to$-introduction. Define $\Pi[\Delta/\mathcal{U}]$ to be the derivation tree obtained from $\Pi$ as follows. For each assumption leaf occurrence $u \in \mathcal{U}$, delete that leaf and insert a fresh copy of the full derivation tree $\Delta$ in its place. The root formula of each inserted copy is $A$, so the formula supplied to the inference rule immediately above the deleted leaf is unchanged. Every assumption leaf of $\Pi$ not belonging to $\mathcal{U}$ is left unchanged, and every inference rule occurrence in $\Pi$ is left unchanged. [guided] The operation $\Pi[\Delta/\mathcal{U}]$ is a syntactic substitution operation on derivation trees. The family $\mathcal{U}$ is not a set of formulas; it is a family of particular leaf occurrences in the tree $\Pi$. This distinction matters because the same formula $A$ may occur several times as an open assumption, and only the occurrences marked for discharge by $\to$-introduction are replaced. For each marked leaf $u \in \mathcal{U}$, the formula at that leaf is $A$. The derivation $\Delta$ also concludes with formula $A$. Therefore replacing the leaf $u$ by a fresh copy of $\Delta$ preserves the formula that is passed upward to the next inference rule in $\Pi$. The word "fresh" means that if there are several marked occurrences, we insert independent copies of the tree $\Delta$, so that each replacement is a valid derivation of its own occurrence of $A$. All other parts of $\Pi$ are kept fixed: unmarked assumption leaves remain assumption leaves, and every rule occurrence above the leaves is copied exactly. Thus the substitution changes only the sources of the marked assumptions and does not alter the shape of the proof above them. [/guided] [/step] [step:Verify by structural induction that the substituted tree is a derivation of the same conclusion] We prove by induction on subderivations $\Theta$ of $\Pi$ that $\Theta[\Delta/\mathcal{U}]$ is a well-formed derivation with the same conclusion formula as $\Theta$. If $\Theta$ is an assumption occurrence in $\mathcal{U}$, then its conclusion is $A$, and $\Theta[\Delta/\mathcal{U}]$ is a fresh copy of $\Delta$, whose conclusion is $A$. If $\Theta$ is an assumption occurrence not in $\mathcal{U}$, then $\Theta[\Delta/\mathcal{U}] = \Theta$, so it remains a well-formed derivation with the same conclusion. For the inductive step, suppose the last rule of $\Theta$ has immediate subderivations $\Theta_1,\dots,\Theta_m$. By the induction hypothesis, each $\Theta_i[\Delta/\mathcal{U}]$ is a well-formed derivation with the same conclusion as $\Theta_i$. Since the last rule of $\Theta$ is left unchanged and its premise formulas are unchanged, the same rule may be applied to the substituted premises. Hence $\Theta[\Delta/\mathcal{U}]$ is a well-formed derivation with the same conclusion as $\Theta$. Applying this to $\Theta = \Pi$, the tree $\Pi[\Delta/\mathcal{U}]$ is a well-formed derivation of $B$. [guided] The point of the induction is to check that substitution does not merely give a tree-shaped object, but gives a genuine derivation. First consider a subderivation $\Theta$ that consists of a single assumption leaf. There are two cases. If that leaf belongs to $\mathcal{U}$, then its formula is $A$ by definition of $\mathcal{U}$, and after substitution it is replaced by $\Delta$. Since $\Delta$ is a derivation of $A$, the resulting subderivation still concludes with $A$. If the assumption leaf is not in $\mathcal{U}$, it is not changed at all, so it remains a valid one-line derivation of the same formula. Now suppose $\Theta$ ends with an inference rule whose immediate premise derivations are $\Theta_1,\dots,\Theta_m$. The substitution operation acts inside the premise derivations and leaves the final rule occurrence itself unchanged. By the induction hypothesis, each substituted premise $\Theta_i[\Delta/\mathcal{U}]$ is a derivation of exactly the same formula as $\Theta_i$. Therefore the final inference rule has exactly the same premise formulas after substitution as it had before substitution. Since it was a legitimate rule application before, it is still a legitimate rule application after substitution. Taking $\Theta$ to be the entire derivation $\Pi$, we obtain that $\Pi[\Delta/\mathcal{U}]$ is a well-formed derivation. Its conclusion is the same as the conclusion of $\Pi$, namely $B$. [/guided] [/step] [step:Compute the open assumptions of the substituted derivation] The open assumptions of $\Pi$ consist only of assumptions from $\Gamma$ together with the marked occurrences in $\mathcal{U}$. In $\Pi[\Delta/\mathcal{U}]$, every occurrence in $\mathcal{U}$ has been removed. Each removed occurrence is replaced by a copy of $\Delta$, whose open assumptions are contained in $\Sigma$. The unmarked open assumptions from $\Pi$ are unchanged and are contained in $\Gamma$. Therefore the open assumptions of $\Pi[\Delta/\mathcal{U}]$ are contained in $\Gamma \cup \Sigma$. [guided] We now track exactly what happens to open assumptions. The original derivation $\Pi$ may have open assumptions from $\Gamma$, and it also has the marked occurrences $\mathcal{U}$ of formula $A$. When $\to$-introduction is applied to $\Pi$, precisely the occurrences in $\mathcal{U}$ are discharged. The reduction replaces those same occurrences directly by proofs of $A$. After substitution, no occurrence from $\mathcal{U}$ remains as an open assumption, because each such leaf has been deleted. In its place sits a copy of $\Delta$. The only open assumptions introduced by that copy are the open assumptions of $\Delta$, and these are contained in $\Sigma$ by hypothesis. All other open assumptions of $\Pi$ were unmarked, so the substitution does not affect them; they remain among $\Gamma$. Thus every open assumption in the substituted derivation is either an unchanged open assumption from $\Gamma$ or an open assumption coming from one of the inserted copies of $\Delta$, hence from $\Sigma$. Consequently the open assumptions are contained in $\Gamma \cup \Sigma$. [/guided] [/step] [step:Identify the detour reduction with the substituted derivation] The displayed derivation first abstracts the marked $A$-assumptions in $\Pi$ to obtain $A \to B$, and then immediately applies that implication to a derivation $\Delta$ of $A$. The defining reduction for an immediate $\to I$ followed by $\to E$ removes this detour by substituting the argument derivation $\Delta$ for precisely the discharged assumption occurrences. By the construction and verification above, the reduct is exactly $\Pi[\Delta/\mathcal{U}]$, a derivation of $B$ from open assumptions contained in $\Gamma \cup \Sigma$. This proves the theorem. [/step]