[proofplan] The only possible information used by a conjunction-elimination rule is the corresponding component of the conjunction-introduction rule that immediately precedes it. We inspect the two possible elimination rules separately. The left projection discards the derivation of $B$ and retains the derivation of $A$, while the right projection discards the derivation of $A$ and retains the derivation of $B$. [/proofplan] [step:Identify the immediate conjunction redex] Let $\Pi_A$ denote the given derivation of $A$, and let $\Pi_B$ denote the given derivation of $B$. By the conjunction-introduction rule, the derivation \begin{align*} \Pi_{A \wedge B} = \frac{\Pi_A \quad \Pi_B}{A \wedge B}\; \wedge I \end{align*} has conclusion $A \wedge B$, with immediate left subderivation $\Pi_A$ and immediate right subderivation $\Pi_B$. An immediate conjunction redex is precisely a derivation in which a conjunction introduced by $\wedge I$ is used at once as the major premise of either $\wedge E_1$ or $\wedge E_2$. Thus the two redexes under consideration are \begin{align*} \frac{ \frac{\Pi_A \quad \Pi_B}{A \wedge B}\; \wedge I }{A}\; \wedge E_1 \end{align*} and \begin{align*} \frac{ \frac{\Pi_A \quad \Pi_B}{A \wedge B}\; \wedge I }{B}\; \wedge E_2. \end{align*} [/step] [step:Contract the left projection to the derivation of $A$] The local reduction rule for a conjunction introduced by $\wedge I$ and immediately projected by $\wedge E_1$ replaces the whole introduction-elimination pair by the left component derivation: \begin{align*} \frac{ \frac{\Pi_A \quad \Pi_B}{A \wedge B}\; \wedge I }{A}\; \wedge E_1 \;\longrightarrow\; \Pi_A. \end{align*} The conclusion of the reduced derivation is $A$, matching the conclusion of the original left-elimination derivation. Since the component $\Pi_B$ is discarded and no inference inside $\Pi_A$ is changed, the open assumptions of the reduced derivation are exactly the open assumptions of $\Pi_A$. [/step] [step:Contract the right projection to the derivation of $B$] The local reduction rule for a conjunction introduced by $\wedge I$ and immediately projected by $\wedge E_2$ replaces the whole introduction-elimination pair by the right component derivation: \begin{align*} \frac{ \frac{\Pi_A \quad \Pi_B}{A \wedge B}\; \wedge I }{B}\; \wedge E_2 \;\longrightarrow\; \Pi_B. \end{align*} The conclusion of the reduced derivation is $B$, matching the conclusion of the original right-elimination derivation. Since the component $\Pi_A$ is discarded and no inference inside $\Pi_B$ is changed, the open assumptions of the reduced derivation are exactly the open assumptions of $\Pi_B$. [/step] [step:Conclude the two beta reductions] The two possible immediate eliminations of a conjunction introduced from $\Pi_A$ and $\Pi_B$ have now been exhausted. The left elimination reduces to $\Pi_A$, and the right elimination reduces to $\Pi_B$, with open assumptions inherited from the retained component derivation in each case. This proves the claimed conjunction beta reductions. [/step]