\section{Proof of Thm.~\ref{thm:deduction}, Sect.~\ref{sect:preliminaries}}
\label{sect:app-preliminaries}

%Equality axioms:
%\[
% \begin{array}{rl}
%\refl & \forall x . x = x \\
%\symm & \forall x, y. (x = y \limp y = x )\\
%\trans & \forall x , y , z . ( x = y \limp y = z \limp x = z ) \\
%\subst_f & \forall \vec x , \vec y . (\vec x = \vec y \limp f(\vec x) = f(\vec y) ) \\
%\subst_P & \forall \vec x , \vec y. (\vec x = \vec y \limp P(\vec x) \limp P(\vec y)  )
% \end{array}
% \]

%\begin{theorem}[Theorem \ref{thm:deduction}]
%tt
%\end{theorem}
 
% \begin{proof}[Proof of Thm.~\ref{thm:deduction}]
Suppose $\theory \cup \{ A \}$ proves $B$ and let $\pi$ be a $\theory$-derivation with end-sequent $\seqar B$ and leaves $\seqar A$, i.e.:
\[
\vltreeder{\pi}{ \seqar B }{ \seqar A }{\vldots}{\seqar A}
\]

Then construct the following $\theory$-proof of $!A \limp B$,
\[
\vlderivation{
\vlin{\rigrul{\limp}}{}{\seqar !A \limp B}{
\vltr{!A, \pi }{ !A \seqar B }{
\vlin{\lefrul{!}}{}{!A \seqar A}{
\vlin{\id}{}{A\seqar A}{\vlhy{}}
}
}{ \vlhy{\vldots} }{
\vlin{\lefrul{!}}{}{!A \seqar A}{
\vlin{\id}{}{A\seqar A}{\vlhy{}}
}
}
}
}
\]
where $!A, \pi$ is obtained by appending $!A$ to the antecedent of each sequent in $\pi$, inserting left-contraction steps when necessary. Free variable conditions are satisfied since $A$ is closed (and so also $!A$) and side-conditions are satisfied since $!A$ is a $!$-formula.

For the other direction simply extend any $\theory$-proof of $!A \limp B$ as follows:
\[
\vlderivation{
\vliin{\cut}{}{ \seqar B }{
\vlin{\rigrul{!}}{}{\seqar !A }{\vlhy{\seqar A}}
}{
\vliq{ \inv{{\limp}} }{}{ !A \seqar B }{ \vlhy{\seqar !A \limp B }}
}
}
\]


% \end{proof}