[proofplan] Start with a derivation of $B$ whose undischarged assumptions lie in $\Gamma \cup \{A\}$. Introduce a temporary assumption occurrence labelled $A$ if necessary, and place the given derivation under that assumption. Then apply the implication introduction rule, discharging every open occurrence of the temporary assumption $A$ used for the derivation of $B$. The resulting derivation concludes $A \to B$, and its only remaining undischarged assumptions are those already belonging to $\Gamma$. [/proofplan] [step:Choose a derivation of $B$ from assumptions in $\Gamma \cup \{A\}$] Assume $\Gamma \cup \{A\} \vdash_{\mathsf{ND}_{\to}} B$. By the definition of derivability in $\mathsf{ND}_{\to}$, there exists a finite natural deduction derivation $\Pi$ with conclusion $B$ such that every undischarged assumption occurrence of $\Pi$ is an occurrence of a formula belonging to $\Gamma \cup \{A\}$. Let $\mathcal{O}(\Pi)$ denote the set of undischarged assumption occurrences in $\Pi$. Partition $\mathcal{O}(\Pi)$ into two classes: \begin{align*} \mathcal{O}_A(\Pi) &= \{o \in \mathcal{O}(\Pi) : \text{the formula labelling } o \text{ is } A\}, \\ \mathcal{O}_\Gamma(\Pi) &= \{o \in \mathcal{O}(\Pi) : \text{the formula labelling } o \text{ belongs to } \Gamma\}. \end{align*} Then every undischarged assumption occurrence of $\Pi$ lies in $\mathcal{O}_A(\Pi) \cup \mathcal{O}_\Gamma(\Pi)$. [guided] We begin by unpacking the hypothesis. The assertion $\Gamma \cup \{A\} \vdash_{\mathsf{ND}_{\to}} B$ means that there is a finite natural deduction derivation $\Pi$ whose final line is $B$, and whose open assumptions are all among the formulas in $\Gamma \cup \{A\}$. We name the open assumption occurrences because implication introduction discharges occurrences, not merely formula names. Let $\mathcal{O}(\Pi)$ be the set of all undischarged assumption occurrences in $\Pi$. Among these, define \begin{align*} \mathcal{O}_A(\Pi) &= \{o \in \mathcal{O}(\Pi) : \text{the formula labelling } o \text{ is } A\}, \\ \mathcal{O}_\Gamma(\Pi) &= \{o \in \mathcal{O}(\Pi) : \text{the formula labelling } o \text{ belongs to } \Gamma\}. \end{align*} The hypothesis ensures that no other kind of open assumption occurrence is present. Thus every open assumption of $\Pi$ is either an occurrence of $A$ or an occurrence of some formula from $\Gamma$. [/guided] [/step] [step:Build an $A$-subderivation of $B$ before applying implication introduction] If $\mathcal{O}_A(\Pi) \neq \varnothing$, set $\Pi_A := \Pi$ and set $D_A := \mathcal{O}_A(\Pi)$. If $\mathcal{O}_A(\Pi) = \varnothing$, let $a$ be a fresh assumption occurrence labelled $A$, with $a \notin \mathcal{O}(\Pi)$, and define $\Pi_A$ to be the derivation obtained by opening the assumption occurrence $a$ and then reproducing the derivation $\Pi$ of $B$ inside that subderivation. Set $D_A := \{a\}$ in this case. This use of $\Pi$ under the additional fresh assumption is the admissible weakening property for natural deduction: adding an unused open assumption occurrence does not alter any inference already occurring in a derivation. Indeed, every line of $\Pi$ is copied with the same formula and the same rule justification, and the new occurrence $a$ is not cited by any inference in the copied derivation. Hence $\Pi_A$ is a derivation of $B$ whose undischarged assumptions are contained in $\mathcal{O}_\Gamma(\Pi) \cup D_A$. Apply the implication introduction rule of $\mathsf{ND}_{\to}$ to the derivation $\Pi_A$, discharging exactly the assumption occurrences in $D_A$. The rule is applicable because $D_A$ is a nonempty set of open assumption occurrences labelled $A$ in the subderivation concluding $B$. This produces a derivation $\Pi'$ with conclusion $A \to B$. [guided] The implication introduction rule requires an actual subderivation of $B$ under at least one open assumption occurrence labelled $A$. Therefore we first make sure such an occurrence is present. If $\mathcal{O}_A(\Pi) \neq \varnothing$, the original derivation already has open occurrences labelled $A$. In that case we put $\Pi_A := \Pi$ and choose the set to be discharged as \begin{align*} D_A := \mathcal{O}_A(\Pi). \end{align*} Then $\Pi_A$ is already a derivation of $B$ whose open assumptions are contained in $\mathcal{O}_\Gamma(\Pi) \cup D_A$. If $\mathcal{O}_A(\Pi) = \varnothing$, the derivation $\Pi$ proves $B$ without using any open occurrence of $A$. To apply implication introduction in the standard non-vacuous form, choose a fresh assumption occurrence $a$ labelled $A$, with $a \notin \mathcal{O}(\Pi)$, and reproduce the whole derivation $\Pi$ below that assumption. This is justified by structural weakening for natural deduction: adding an unused open assumption occurrence preserves derivability, because each copied line of $\Pi$ has the same formula and the same rule justification as before, and the new assumption occurrence $a$ is not used by any inference in the copied derivation. In this case we define \begin{align*} D_A := \{a\}. \end{align*} Thus, in both cases, we have a derivation $\Pi_A$ of $B$ whose undischarged assumptions are contained in $\mathcal{O}_\Gamma(\Pi) \cup D_A$, where every occurrence in $D_A$ is labelled $A$ and $D_A$ is nonempty. Now implication introduction applies to the subderivation $\Pi_A$: from a derivation of $B$ under the selected open assumption occurrences $D_A$ labelled $A$, infer $A \to B$ while discharging exactly those occurrences. The resulting derivation is denoted $\Pi'$, and its final formula is $A \to B$. [/guided] [/step] [step:Verify that the remaining open assumptions belong to $\Gamma$] By construction, $\Pi_A$ has undischarged assumption occurrences contained in $\mathcal{O}_\Gamma(\Pi) \cup D_A$, and implication introduction removes exactly the occurrences in $D_A$. Therefore every undischarged assumption occurrence of $\Pi'$ belongs to $\mathcal{O}_\Gamma(\Pi)$, and hence is labelled by a formula in $\Gamma$. Thus $\Pi'$ is an $\mathsf{ND}_{\to}$ derivation of $A \to B$ whose undischarged assumptions are contained in $\Gamma$. Hence $\Gamma \vdash_{\mathsf{ND}_{\to}} A \to B$, as required. [/step]