Tree

\begin{prooftree}
    \AxiomC{$f: (\pi_P + \pi_Q) \rightarrow 0 \in f: (\pi_P + \pi_Q) \rightarrow 0, x: \pi_P$}
    \RightLabel{\textsc{Hyp}}
    \UnaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0, x: \pi_P \vdash f: (\pi_P + \pi_Q) \rightarrow 0$}
    \AxiomC{$x: \pi_P \in f: (\pi_P + \pi_Q) \rightarrow 0, x: \pi_P$}
    \RightLabel{\textsc{Hyp}}
    \UnaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0, x: \pi_P \vdash x: \pi_P$}
    \RightLabel{\textsc{+I$_1$}}
    \UnaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0, x: \pi_P \vdash L \; x: (\pi_P + \pi_Q)$}
    \RightLabel{\textsc{$\rightarrow$I}}
    \BinaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0, x: \pi_P \vdash f \; (L \; x): 0$}
    \UnaryInfC{$\Delta_1$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$f: (\pi_P + \pi_Q) \rightarrow 0 \in f: (\pi_P + \pi_Q) \rightarrow 0, y: \pi_Q$}
    \RightLabel{\textsc{Hyp}}
    \UnaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0, y: \pi_Q \vdash f: (\pi_P + \pi_Q) \rightarrow 0$}
    \AxiomC{$y: \pi_Q \in f: (\pi_P + \pi_Q) \rightarrow 0, y: \pi_Q$}
    \RightLabel{\textsc{Hyp}}
    \UnaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0, y: \pi_Q \vdash y: \pi_Q$}
    \RightLabel{\textsc{+I$_2$}}
    \UnaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0, y: \pi_Q \vdash R \; y: (\pi_P + \pi_Q)$}
    \RightLabel{\textsc{$\rightarrow$I}}
    \BinaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0, y: \pi_Q \vdash f \; (R \; y): 0$}
    \UnaryInfC{$\Delta_2$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$\Delta_1$}
    \UnaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0, x: \pi_P \vdash f \; (L \; x): 0$}
    \RightLabel{\textsc{$\rightarrow$I}}
    \UnaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0 \vdash \lambda x: \pi_P. f \; (L \; x): \pi_P \rightarrow 0$}
    \AxiomC{$\Delta_2$}
    \UnaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0, y: \pi_Q \vdash f \; (R \; y): 0$}
    \RightLabel{\textsc{$\rightarrow$I}}
    \UnaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0 \vdash \lambda y: \pi_Q. f \; (R \; y): \pi_Q \rightarrow 0$}
    \RightLabel{\textsc{$\times$I}}
    \BinaryInfC{$f: (\pi_P + \pi_Q) \rightarrow 0 \vdash \langle \lambda x: \pi_P. f \; (L \; x), \lambda y: \pi_Q. f \; (R \; y) \rangle: (\pi_P \rightarrow 0) \times (\pi_Q \rightarrow 0)$}
    \RightLabel{\textsc{$\rightarrow$I}}
    \UnaryInfC{$\cdot \vdash \lambda f: ((\pi_P + \pi_Q) \rightarrow 0). \langle \lambda x: \pi_P. f \; (L \; x), \lambda y: \pi_Q. f \; (R \; y) \rangle: ((\pi_P + \pi_Q) \rightarrow 0) \rightarrow (\pi_P \rightarrow 0) \times (\pi_Q \rightarrow 0)$}
\end{prooftree}