[proofplan] The forward implication is exactly the operation licensed by implication introduction: starting from a derivation of $B$ in which some open leaves are temporary assumptions labelled $A$, discharge precisely those leaves and conclude $A \to B$. The reverse implication uses implication elimination: from a derivation of $A \to B$ from $\Gamma$, adjoin one fresh open assumption occurrence labelled $A$ and apply modus ponens to obtain $B$. The only bookkeeping issue is that natural deduction tracks assumption occurrences, not merely formulas, so we explicitly record which occurrences are discharged and which remain open. [/proofplan] [step:Discharge the selected temporary occurrences of $A$ to derive $A \to B$] Assume first that $\Pi$ is a natural deduction derivation with conclusion $B$. Let $\mathcal{O}(\Pi)$ denote the finite set of open assumption occurrences of $\Pi$. By hypothesis, there is a selected subset $S \subseteq \mathcal{O}(\Pi)$ such that every occurrence in $S$ is labelled by the formula $A$, and every occurrence in $\mathcal{O}(\Pi) \setminus S$ is labelled by a formula belonging to $\Gamma$. Apply the implication introduction rule $(\to I)$ to the derivation $\Pi$, discharging exactly the assumption occurrences in $S$. The resulting derivation, call it $\Pi'$, has conclusion $A \to B$. Its open assumption occurrences are exactly the occurrences in $\mathcal{O}(\Pi) \setminus S$, because $(\to I)$ removes from the open assumptions precisely the discharged occurrences and leaves all other open assumptions unchanged. Hence every open assumption occurrence of $\Pi'$ is labelled by a formula in $\Gamma$. Therefore there is a derivation of $A \to B$ whose open assumptions are contained in $\Gamma$. [guided] Assume that we have a derivation $\Pi$ of $B$ in which the only open assumptions are assumptions from $\Gamma$ together with some temporary assumptions labelled $A$. Natural deduction does not discharge formulas abstractly; it discharges particular leaves of a derivation tree. Therefore let $\mathcal{O}(\Pi)$ be the finite set of open assumption occurrences of $\Pi$, and let $S \subseteq \mathcal{O}(\Pi)$ be the selected family of temporary open leaves labelled by $A$. The hypothesis says two things about these open leaves. First, every occurrence in $S$ has label $A$. Second, every open occurrence not in $S$, namely every element of $\mathcal{O}(\Pi) \setminus S$, has label belonging to $\Gamma$. Thus the derivation has exactly the right form for implication introduction: it derives $B$ under temporary assumptions $A$, and those are precisely the assumptions we intend to discharge. Apply the rule $(\to I)$ to $\Pi$, discharging exactly the occurrences in $S$. This produces a new derivation $\Pi'$ whose conclusion is $A \to B$. The open assumptions of $\Pi'$ are the open assumptions of $\Pi$ except for the discharged occurrences in $S$. Hence the open assumptions of $\Pi'$ are precisely the occurrences in $\mathcal{O}(\Pi) \setminus S$, all of which are labelled by formulas in $\Gamma$. Therefore $\Pi'$ is a derivation of $A \to B$ from open assumptions contained in $\Gamma$. [/guided] [/step] [step:Add a fresh assumption $A$ and apply implication elimination to derive $B$] Conversely, assume that $\Pi'$ is a natural deduction derivation with conclusion $A \to B$ whose open assumption occurrences are contained in $\Gamma$. Let $a$ be a new assumption occurrence labelled by $A$, not occurring in $\Pi'$. Form the one-line derivation $\Pi_A$ whose only open assumption occurrence is $a$ and whose conclusion is $A$. Apply implication elimination $(\to E)$ to the derivations $\Pi'$ and $\Pi_A$. The resulting derivation $\Pi$ has conclusion $B$. Its open assumption occurrences are the open assumption occurrences of $\Pi'$ together with the fresh occurrence $a$. Since the open assumptions of $\Pi'$ are contained in $\Gamma$ and $a$ is labelled by $A$, the derivation $\Pi$ has open assumptions contained in $\Gamma$ together with one selected temporary occurrence of $A$. Hence there is a derivation of $B$ from $\Gamma$ together with selected temporary occurrences of $A$. [guided] Now assume that we have a derivation $\Pi'$ of $A \to B$ and that every open assumption occurrence of $\Pi'$ is labelled by a formula in $\Gamma$. To recover a derivation of $B$, we must supply the antecedent $A$ as an open assumption and then use implication elimination. Choose a fresh assumption occurrence $a$ labelled by $A$. Fresh means that $a$ is a new leaf and is not already an occurrence in the derivation tree $\Pi'$. Let $\Pi_A$ be the derivation consisting only of this assumption occurrence; its conclusion is $A$, and its only open assumption occurrence is $a$. The implication elimination rule $(\to E)$ takes one derivation with conclusion $A \to B$ and another derivation with conclusion $A$, and produces a derivation with conclusion $B$. Applying $(\to E)$ to $\Pi'$ and $\Pi_A$ gives a derivation $\Pi$ of $B$. The open assumptions of $\Pi$ are exactly the open assumptions inherited from $\Pi'$ together with the fresh assumption occurrence $a$. The inherited open assumptions are labelled by formulas in $\Gamma$, and the new open assumption occurrence is labelled by $A$. Thus $\Pi$ is a derivation of $B$ whose open assumptions are contained in $\Gamma$ together with a selected temporary occurrence of $A$. [/guided] [/step] [step:Combine the two constructions to obtain the equivalence] The first construction proves that any derivation of $B$ from $\Gamma$ together with selected temporary occurrences of $A$ yields a derivation of $A \to B$ from $\Gamma$. The second construction proves that any derivation of $A \to B$ from $\Gamma$ yields a derivation of $B$ from $\Gamma$ together with a fresh selected temporary occurrence of $A$. Therefore the two derivability conditions are equivalent. [/step]