The typing of Teleportation is given below:

$$
\begin{align*}
& \frac{\overline{\vdash |1\rangle : \mathbb{B}} A_{x|1\rangle} \quad \overline{\vdash |0\rangle : \mathbb{B}} A_{x|0\rangle}}{\vdash -|1\rangle : S(\mathbb{B}) S_I^\alpha \quad \vdash |0\rangle : S(\mathbb{B})} \stackrel{\le}{\preceq} \quad \overline{\text{If } y : \mathbb{B} \vdash y : \mathbb{B}} A_x \Rightarrow_E \\
& \qquad \frac{\overline{y : \mathbb{B} \vdash y?(-|1\rangle) \cdot |0\rangle : S(\mathbb{B})}}{\vdash Z : \mathbb{B} \Rightarrow S(\mathbb{B})} \Rightarrow_I \quad \overline{x : \mathbb{B} \vdash x : \mathbb{B}} A_x \Rightarrow_E \\
& \qquad \frac{x : \mathbb{B} \vdash Zx : S(\mathbb{B})}{x : \mathbb{B} \vdash Zx : S(\mathbb{B})} \Rightarrow_E \tag{E.1}
\end{align*}
$$

$$
\begin{align*}
& \frac{(E.1) \qquad \overline{w : \mathbb{B} \vdash w : \mathbb{B}} A_x}{w : \mathbb{B} \vdash Zw : S(\mathbb{B}) \qquad \overline{w : \mathbb{B} \vdash w : S(\mathbb{B})} \stackrel{\le}{\preceq} \qquad \text{If } \overline{y : \mathbb{B} \vdash y : \mathbb{B}} A_x \Rightarrow_E} \\
& \qquad \frac{w : \mathbb{B} \vdash ?Zw \cdot w : \mathbb{B} \Rightarrow S(\mathbb{B})}{y : \mathbb{B}, w : \mathbb{B} \vdash y?Zw \cdot w : S(\mathbb{B})} \Rightarrow_I \quad \overline{x : \mathbb{B}^3 \vdash x : \mathbb{B}^3} A_x \Rightarrow_E \\
& \qquad \frac{y : \mathbb{B} \vdash \lambda w^\mathbb{B} \cdot y?Zw \cdot w : \mathbb{B} \Rightarrow S(\mathbb{B})}{\vdash \lambda y^\mathbb{B} \cdot \lambda w^\mathbb{B} \cdot y?Zw \cdot w : \mathbb{B} \Rightarrow \mathbb{B} \Rightarrow S(\mathbb{B})} \Rightarrow_I \quad \overline{x : \mathbb{B}^3 \vdash \text{head } x : \mathbb{B}} \times_{E_r} \Rightarrow_E \\
& \qquad \frac{x : \mathbb{B}^3 \vdash Z^{(\text{head } x)} : \mathbb{B} \Rightarrow S(\mathbb{B})}{x : \mathbb{B}^3 \vdash Z^{(\text{head } x)} : \mathbb{B} \Rightarrow S(\mathbb{B})} \Rightarrow_E \tag{E.2}
\end{align*}
$$

$$
\begin{align*}
& \frac{\text{(D.3)} \quad \overline{\vdash \text{ not} : \mathbb{B} \Rightarrow \mathbb{B}} \quad \overline{z : \mathbb{B} \vdash z : \mathbb{B}} A_x}{z : \mathbb{B} \vdash \text{ not } z : \mathbb{B}} \quad \overline{z : \mathbb{B} \vdash z : \mathbb{B}} A_x} \stackrel{\Rightarrow_E}{\Rightarrow_E} \quad \overline{\text{If } y : \mathbb{B} \vdash y : \mathbb{B}} A_x \stackrel{\Rightarrow_E}{\Rightarrow_E} \\
& \qquad \frac{y : \mathbb{B}, z : \mathbb{B} \vdash y?\text{not } z \cdot z : \mathbb{B}}{y : \mathbb{B} \vdash \lambda z^\mathbb{B} \cdot y?\text{not } z \cdot z : \mathbb{B} \Rightarrow \mathbb{B}} \Rightarrow_I \quad \overline{x : \mathbb{B}^3 \vdash x : \mathbb{B}^3} A_x \times_{E_t} \Rightarrow_E \\
& \qquad \frac{\vdash \lambda y^\mathbb{B} \cdot \lambda z^\mathbb{B} \cdot y?\text{not } z \cdot z : \mathbb{B} \Rightarrow \mathbb{B} \Rightarrow \mathbb{B}}{x : \mathbb{B}^3 \vdash \text{not } (\text{head tail } x) : \mathbb{B} \Rightarrow \mathbb{B}} \Rightarrow_I \quad \overline{x : \mathbb{B}^3 \vdash \text{head tail } x : \mathbb{B}} \times_{E_r} \Rightarrow_E \tag{E.3}
\end{align*}
$$

$$
\begin{align*}
& \frac{\text{(E.2)} \qquad \overline{y : \mathbb{B}^3 \vdash Z^{(\text{head } y)} : \mathbb{B} \Rightarrow S(\mathbb{B})} \qquad \overline{x : \mathbb{B}^3, y : \mathbb{B}^3 \vdash \text{not } (\text{tail } y)(\text{tail tail } x) : \mathbb{B}} C}{x : \mathbb{B}^3 \vdash \text{not } (\text{tail } x)(\text{tail tail } x) : \mathbb{B}} \Rightarrow_E \\
& \qquad \frac{x : \mathbb{B}^3, y : \mathbb{B}^3 \vdash Z^{(\text{head } y)}(\text{not } (\text{head tail } x)(\text{tail tail } x)) : S(\mathbb{B})}{x : \mathbb{B}^3 \vdash Z^{(\text{head } x)}(\text{not } (\text{head tail } x)(\text{tail tail } x)) : S(\mathbb{B})} C \Rightarrow_I \\
& \qquad \frac{\vdash \text{Bob} : \mathbb{B}^3 \Rightarrow S(\mathbb{B})}{\vdash \text{Bob} : \mathbb{B}^3 \Rightarrow S(\mathbb{B})} \Rightarrow_I \tag{E.4}
\end{align*}
$$
$$
\begin{equation}
\begin{split}
\frac{(D.1)}{\substack{\vdash H : \mathbb{B} \Rightarrow S(\mathbb{B}) \\ x : \mathbb{B}^3 \vdash H(\text{head } x) : S(\mathbb{B})}} \quad & \frac{\overline{x : \mathbb{B}^3 \vdash x : \mathbb{B}^3}}{x : \mathbb{B}^3 \vdash \text{head } x : \mathbb{B}} \quad \mathit{Ax} \\
& \stackrel{\times_{E_r}}{\Rightarrow_E} \quad \frac{\overline{y : \mathbb{B}^3 \vdash y : \mathbb{B}^3}}{y : \mathbb{B}^3 \vdash \text{tail } y : \mathbb{B}^2} \quad \mathit{Ax} \\
& \stackrel{\times_{E_t}}{\times_I} \quad \frac{\overline{\phantom{y : \mathbb{B}^3 \vdash} \phantom{y : \mathbb{B}^3} \phantom{y : \mathbb{B}^3}}}{\phantom{\overline{\phantom{y : \mathbb{B}^3 \vdash} \phantom{y : \mathbb{B}^3} \phantom{y : \mathbb{B}^3}}} \quad \mathit{Ax} \\
& \stackrel{\times_I}{\Rightarrow_I} \quad \frac{\overline{x : \mathbb{B}^3, y : \mathbb{B}^3 \vdash (H(\text{head } x)) \times (\text{tail } y) : S(\mathbb{B}) \times \mathbb{B}^2}}{x : \mathbb{B}^3 \vdash (H(\text{head } x)) \times (\text{tail } x) : S(\mathbb{B}) \times \mathbb{B}^2} \quad C \\
& \stackrel{\times_I}{\Rightarrow_I} \quad \frac{\vdash H_1^3 : \mathbb{B}^3 \Rightarrow S(\mathbb{B}) \times \mathbb{B}^2}{\vdash H_1^3 : \mathbb{B}^3 \Rightarrow S(\mathbb{B}) \times \mathbb{B}^2}
\end{split}
\tag{E.5}
\end{equation}
$$

$$
\begin{equation}
\begin{split}
\frac{\overline{y : \mathbb{B}^2 \vdash y : \mathbb{B}^2}}{y : \mathbb{B}^2 \vdash \text{head } y : \mathbb{B}} \quad \mathit{Ax} &\quad \frac{\overline{x : \mathbb{B}^2 \vdash x : \mathbb{B}^2}}{x : \mathbb{B}^2 \vdash \text{not}(\text{tail } x) : \mathbb{B}} \quad \mathit{Ax} \\
&\quad \stackrel{\times_{E_l}}{\Rightarrow_E} \quad \frac{\overline{x : \mathbb{B}^2 \vdash x : \mathbb{B}^2}}{x : \mathbb{B}^2 \vdash \text{tail } x : \mathbb{B}} \quad \mathit{Ax} \\
&\quad \stackrel{\times_{E_l}}{\Rightarrow} \quad \frac{\overline{y : \mathbb{B}^2 \vdash y : \mathbb{B}^2}}{y : \mathbb{B}^2 \vdash \text{head } y : \mathbb{B}} \quad \mathit{Ax} \\
&\quad \stackrel{\times_{E_r}}{\Rightarrow_E} \quad \frac{\overline{x : \mathbb{B}^2 \vdash ?\text{not}(\text{tail } x) \cdot (\text{tail } x) : \mathbb{B}}{x : \mathbb{B}^2 \vdash (\text{head } y) ?\text{not}(\text{tail } x) \cdot (\text{tail } x) : \mathbb{B}} \quad C \\
&\quad \stackrel{\times_I}{\Rightarrow_I} \quad \frac{\overline{x : \mathbb{B}^2, y : \mathbb{B}^2 \vdash (\text{head } y) \times ((\text{head } y) ?\text{not}(\text{tail } x) \cdot (\text{tail } x)) : \mathbb{B}^2}}{x : \mathbb{B}^2 \vdash (\text{head } x) \times ((\text{head } y) ?\text{not}(\text{tail } x) \cdot (\text{tail } x)) : \mathbb{B}^2} \quad C \\
&\quad \stackrel{\times_I}{\Rightarrow_I} \quad \frac{\vdash \text{cnot} : \mathbb{B}^2 \Rightarrow \mathbb{B}^2}{\vdash \text{cnot} : \mathbb{B}^2 \Rightarrow \mathbb{B}^2}
\end{split}
\tag{E.6}
\end{equation}
$$

$$
\begin{equation}
\begin{split}
\frac{\overline{y : \mathbb{B}^3 \vdash y : \mathbb{B}^3}}{y : \mathbb{B}^3 \vdash \text{tail } y : \mathbb{B}^2} \quad \mathit{Ax} &\quad \frac{\overline{x : \mathbb{B}^3 \vdash x : \mathbb{B}^3}}{x : \mathbb{B}^3 \vdash \text{head } x : \mathbb{B}} \quad \mathit{Ax} \\
&\quad \stackrel{\times_{E_l}}{\Rightarrow_E} \quad \frac{\overline{y : \mathbb{B}^3 \vdash \text{head tail } y : \mathbb{B}}}{y : \mathbb{B}^3 \vdash \text{head tail } y : \mathbb{B}} \quad \mathit{Ax} \\
&\quad \stackrel{\times_I}{\Rightarrow_I} \quad \frac{\overline{y : \mathbb{B}^3 \vdash y : \mathbb{B}^3}}{y : \mathbb{B}^3 \vdash \text{tail } y : \mathbb{B}^2} \quad \mathit{Ax} \\
\frac{\overline{x : \mathbb{B}^3 \vdash x : \mathbb{B}^3}}{x : \mathbb{B}^3 \vdash \text{head } x : \mathbb{B}} \quad \mathit{Ax} &\quad \frac{\overline{x : \mathbb{B}^3, y : \mathbb{B}^3 \vdash (\text{head } x) \times (\text{head tail } y) : \mathbb{B}^2}}{x : \mathbb{B}^3 \vdash (\text{head } x) \times (\text{head tail } x) : \mathbb{B}^2} \quad C \\
&\quad \stackrel{\times_I}{\Rightarrow_E} \quad \frac{\overline{y : \mathbb{B}^3 \vdash y : \mathbb{B}^2}}{y : \mathbb{B}^3 \vdash \text{tail tail } y : \mathbb{B}} \quad \mathit{Ax} \\
\frac{\overline{x : \mathbb{B}^3 \vdash \text{cnot}((\text{head } x) \times (\text{head tail } x)) : \mathbb{B}^2}}{x : \mathbb{B}^3 \vdash \text{cnot}((\text{head } x) \times (\text{head tail } x))) \times (\text{tail tail } x) : \mathbb{B}^3} &\quad \mathit{Ax} \\
\frac{\overline{x : \mathbb{B}^3, y : \mathbb{B}^3 \vdash (\text{cnot}((\text{head } x) \times (\text{head tail } x))) \times (\text{tail tail } y) : \mathbb{B}^2}}{x : \mathbb{B}^3 \vdash (\text{cnot}((\text{head } x) \times (\text{head tail } x))) \times (\text{tail tail } x) : \mathbb{B}^3} &\quad C \\
&\quad \stackrel{\times_I}{\Rightarrow_I} \quad \frac{\overline{\vdash \text{cnot}^3_{12} : \mathbb{B}^3 \Rightarrow \mathbb{B}^3}}{\vdash \text{cnot}^3_{12} : \mathbb{B}^3 \Rightarrow \mathbb{B}^3}
\end{split}
\tag{E.7}
\end{equation}
$$

$$
\begin{equation}
\begin{split}
\frac{\overline{x : S(\mathbb{B}) \times S(\mathbb{B}^2) \vdash x : S(\mathbb{B}) \times S(\mathbb{B}^2)}}{x : S(\mathbb{B}) \times S(\mathbb{B}^2) \vdash x : S(\mathbb{B}) \times S(\mathbb{B}^2)} \quad \mathit{Ax} \\
\frac{\overline{x : S(\mathbb{B}) \times S(\mathbb{B}^2) \vdash \hat{\upharpoonright}_r x : S(\mathbb{B}) \times S(\mathbb{B}^2)}}{x : S(\mathbb{B}) \times S(\mathbb{B}^2) \vdash \hat{\upharpoonright}_l x : S(\mathbb{B}) \times S(\mathbb{B}^2)} \quad \mathit{Ax} \\
\frac{\overline{x : S(\mathbb{B}) \times S(\mathbb{B}^2) \vdash \hat{\upharpoonright}_l \hat{\upharpoonright}_r x : S(\mathbb{B}) \times S(\mathbb{B}^2)}}{x : S(\mathbb{B}) \times S(\mathbb{B}^2) \vdash \hat{\upharpoonright}_l \hat{\upharpoonright}_r x : S(\mathbb{B}^3)} \quad \Rightarrow_{ES}
\end{split}
\tag{E.8}
\end{equation}
$$
$$
\frac{(E.5) \qquad \frac{x : S(\mathbb{B}) \times S(\mathbb{B}^2) \vdash H_1^3 : S(\mathbb{B}^3) \Rightarrow S(\mathbb{B}) \times S(\mathbb{B}^2)}{\vdash H_1^3 : S(\mathbb{B}^3) \Rightarrow S(\mathbb{B}) \times S(\mathbb{B}^2)} \succeq \frac{(E.8) \qquad x : S(\mathbb{B}) \times S(\mathbb{B}^2) \vdash \text{cnot}_{12}^3 \hat{\otimes}_\ell \hat{\otimes}_r x : S(\mathbb{B}^3)}{\vdash H_1^3 : S(\mathbb{B}^3) \Rightarrow S(\mathbb{B}) \times S(\mathbb{B}^2)} \Rightarrow_{ES} \frac{x : S(\mathbb{B}) \times S(\mathbb{B}^2) \vdash H_1^3(\text{cnot}_{12}^3 \hat{\otimes}_\ell \hat{\otimes}_r x) : S(\mathbb{B}) \times S(\mathbb{B}^2)}{x : S(\mathbb{B}) \times S(\mathbb{B}^2) \vdash \hat{\otimes}_r H_1^3(\text{cnot}_{12}^3 \hat{\otimes}_\ell \hat{\otimes}_r x) : S(\mathbb{B}^3)} \hat{\otimes}_r \frac{S_E}{\vdash H_1^3(\text{cnot}_{12}^3 \hat{\otimes}_\ell \hat{\otimes}_r x) : S(\mathbb{B}) \times S(\mathbb{B}^2)} \Rightarrow_I \frac{\vdash \text{Alice} : S(\mathbb{B}) \times S(\mathbb{B}^2) \Rightarrow \mathbb{B}^2 \times S(\mathbb{B})}{\vdash \text{Alice} : S(\mathbb{B}) \times S(\mathbb{B}^2) \Rightarrow \mathbb{B}^2 \times S(\mathbb{B})} \Rightarrow_I \frac{(E.9)}}{(E.9)}
$$

$$
\frac{\frac{\vdash |0\rangle : \mathbb{B} \quad Ax_{|0\rangle} \quad \vdash |0\rangle : \mathbb{B} \quad Ax_{|0\rangle} \quad \vdash |1\rangle : \mathbb{B} \quad Ax_{|1\rangle} \quad \vdash |1\rangle : \mathbb{B} \quad Ax_{|1\rangle}}{\vdash |00\rangle : \mathbb{B}^2 \quad \times_I \quad \vdash |11\rangle : \mathbb{B}^2 \quad \times_I \quad \vdash |11\rangle : \mathbb{B}^2 \quad \times_I \quad \vdash |11\rangle : \mathbb{B}^2 \quad \times_I \quad \vdash \beta_{00} : S(\mathbb{B}^2)} \succeq \frac{S_I^+}{S_I^+} \qquad (E.10)
$$

$$
\frac{(E.4) \qquad \frac{\frac{\vdash \text{Alice} : S(\mathbb{B}) \times S(\mathbb{B}^2) \Rightarrow \mathbb{B}^2 \times S(\mathbb{B})}{\vdash \text{Bob} : \mathbb{B}^3 \Rightarrow S(\mathbb{B})} \succeq \frac{\frac{\vdash q : S(\mathbb{B}) \vdash \text{Alice} (q \times \beta_{00}) : \mathbb{B}^2 \times S(\mathbb{B})}{\vdash q : S(\mathbb{B}) \vdash \text{Alice} (q \times \beta_{00}) : S(\mathbb{B}^2 \times S(\mathbb{B}))} \succeq \frac{\vdash q : S(\mathbb{B}) \vdash \hat{\otimes}_\ell \text{Alice} (q \times \beta_{00}) : S(\mathbb{B}^3)}{\vdash q : S(\mathbb{B}) \vdash \text{Bob} (\hat{\otimes}_\ell \text{Alice} (q \times \beta_{00}))) : S(\mathbb{B})} \Rightarrow_{ES}}{\vdash \text{Bob} : S(\mathbb{B}^3 \Rightarrow S(\mathbb{B}))} \Rightarrow_I \frac{\frac{\vdash q : S(\mathbb{B}) \vdash \text{Bob} (\hat{\otimes}_\ell \text{Alice} (q \times \beta_{00}))) : S(\mathbb{B})}{\vdash q : S(\mathbb{B}) \vdash \text{Bob} (\hat{\otimes}_\ell \text{Alice} (q \times \beta_{00}))) : S(\mathbb{B})} \succeq \frac{\Rightarrow_I}{\vdash \text{Teleportation} : S(\mathbb{B}) \Rightarrow S(\mathbb{B})}}{(E.9)}}{\frac{\vdash q : S(\mathbb{B}) \vdash q : S(\mathbb{B}) \quad Ax}{\vdash q : S(\mathbb{B}) \vdash q \times \beta_{00} : S(\mathbb{B}) \times S(\mathbb{B}^2)} \Rightarrow_I \frac{\vdash \beta_{00} : S(\mathbb{B}^2)}{\vdash q : S(\mathbb{B}) \vdash q \times \beta_{00} : S(\mathbb{B}) \times S(\mathbb{B}^2)} \Rightarrow_E \frac{\vdash \text{Alice} (q \times \beta_{00}) : \mathbb{B}^2 \times S(\mathbb{B})}{\vdash q : S(\mathbb{B}) \vdash \text{Alice} (q \times \beta_{00}) : S(\mathbb{B}^2 \times S(\mathbb{B}))} \succeq \frac{\Rightarrow_I}{\vdash \text{Teleportation} : S(\mathbb{B}) \Rightarrow S(\mathbb{B})}}{(E.10)}}
$$