\newcommand{\dsats}{\models_{\!\cS\bar\cS'} \!}
\newcommand{\insss}{\ins\cS\bar\cS'}

Lemma 6.12 (Schema Weakening)
Let $\ga\inss$. Then
\ben
\item If $\dsat D$, then $\dsats D$.
\item If $\ga\sla G\inss$, then $\ga\sla G\insss$.
\item If $\ga\ins\cS$ then $\ga\ins \cS\mbar \cS'$.
\enen


must be 

\renewcommand{\dsats}{\models_{\!\cS\bar\cS'} \!}
\renewcommand{\insss}{\ins\cS\bar\cS'}
Lemma 6.12 (Schema Weakening)
Let $\ga\inss$. Then
\ben
\item If $\dsat D$, then $\dsats D$.
\item If $\ga\sla G\inss$, then $\ga\sla G\insss$.
\item If $\ga\ins\cS$ then $\ga\ins \cS\mbar \cS'$.
\enen

\begin{proof}
By mutual induction on the structure of $\pi::\  \dsat D$, $\gamma
::\ga\sla G\inss$ and  $\sigma::\ga\ins\cS$. We show the crucial cases:
\bit
\itc $$\pi=\ianc{X\in\{Q,\top,\perp\}}{\dsat X}{\dsat X}$$
Trivially $$\pi'=\ianc{X\in\ \{Q,\top,\perp\}}{\dsats Q}{\dsat X}$$

\itc$$\pi=\ibnc{\dsat D}{\emp\sla G\inss}{\dsat G\Imp  D}{\dsat\Imp}$$
\btab
%$\ga\inss$\bh
$\dsat D$\bs
$\dsats D$\bi $1$\\
$\emp\sla G\inss$\bs
$\emp\sla G\insss$\bi $2$\\
$\dsats G\Imp D$\br $\dsat\Imp$
\etab
\itc $$\gamma=\ibnc{X\in\{Q,\top,\perp\}\mbox{ or (dis)eq}}{\ga\inss}{\ga\sla X\inss}{\sla X}$$
\btab
$\ga\inss$\bs
$\ga\insss$\bi $3$\\
$\ga\sla X\insss$\br $\sla X$
\etab
\itc$$\gamma=\ibnc{\dsat D}{\GG;\cD\And D\sla G\inss}{\ga\sla D\Imp
  G\inss}{\sla\Imp}$$
\btab
$\dsat D$\bs
$\dsats D$\bi $1$\\
$\GG;\cD\And D\sla G\inss$\bs
$\GG;(\cD\And D)\sla G\insss$\bi $2$\\
$\ga\sla D\Imp G\insss$\br $\sla\Imp$
\etab
\itc $$\sigma=\ianc{}{\cdot;\top\ins \cS}{\ins_1}$$
Then immediately:
 $$\sigma'=\ianc{}{\cdot;\top\ins \cS\mbar\cS'}{\ins_1}$$
\itc$$\sigma=\ianc{\GG\vd(\GG';\cD')\in
\cS\quad \dsat\cD'\quad(\GG;\cD)\ins \cS}{(\GG,\block{\GG'});(\cD\And\block{\cD'})\ins
\cS}{\ins_2}$$
\btab
$\ga\inss$\bs
$\ga\insss$\bi $3$\\
$\gapp\in\cS$\bs
$\gapp\in\cS\mbar\cS'$\` By Lemma \ref{le:w1}\\
$\dsat\cD'$\bs
$\dsats D$\bi $1$\\
$(\GG,\block{\GG'});(\cD\And\block{\cD'})\insss$\br $\ins_2$
\etab
\enit
\end{proof}



\begin{figure}
\[
\begin{array}{c}
\ianc{}{\top\tensor D \setminus \top}{\tensor\top D}\qquad
\ianc{}{D\tensor\top \setminus \top}{\tensor D \top }\vsk
\ianc{}{\perp\tensor D \setminus D}{\tensor\perp D}\qquad
\ianc{}{D\tensor\perp \setminus D}{\tensor D \perp }
\vsk
\ianc{}{\Pi(q\ \vN_{1}\If G_{1})\tensor  \Pi(q\ \vN_{2}\If G_{2}) \setminus
\Pi(q\ \vN_{1}\If (\vN_{1}\eqd \vN_{2}) \And G_{1}\And G_{2})}{\tensor{\rm 
At}\atm}\vsk
\ianc{q\not\equiv q'}{\Pi(q\ \vN_{1}\If G_{1})\tensor  \Pi(q'\
  \vN_{2}\If G_{2}) \setminus\top}{\tensor{\rm At}\atm\not\equiv}\vsk 
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{(D_{1}\tensor D'_{1})\tensor D_{2}\setminus D\tensor
  D'}{\tensor\tensor L}
\qquad
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{(D_{1}\And D'_{1})\tensor D_{2}\setminus D\And D'}{\tensor\And L}
\vsk
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{D_2\tensor (D_{1}\tensor D'_{1})\setminus D\tensor
  D'}{\tensor\tensor R}
\qquad
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{D_2\tensor (D_{1}\And D'_{1})\setminus D\And D'}{\tensor\And R}
\end{array}
\]
\caption{$\tensor$-Elimination: $D_{1}\tensor D_{2}\setminus D$}
\label{fig:otimes}
\end{figure}

% \ibnc{\Pi(q\ \vN\If G)\tensor D_{1}\setminus D}{\Pi(q\ \vN\If
%   G)\tensor D_{2}\setminus D'} 
% {\Pi(q\ \vN\If G)\tensor (D_{1}\tensor D_{2})\setminus D\tensor
%   D'}{\tensor\atm\tensor}
% \vsk
% \ibnc{\Pi(q\ \vN\If G)\tensor D_{1}\setminus D}{\Pi(q\ \vN\If
%   G)\tensor D_{2}\setminus D'} 
% {\Pi(q\ \vN\If G)\tensor (D_{1}\And D_{2})\setminus D\And
%   D'}{\tensor\atm\And}
% \vsk

%  \ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D'_{2}\setminus D'}
%  {(D_{1}\And D'_{1})\tensor (D_{2}\tensor D'_2)\setminus D\tensor D'}{\tensor\And\Or}
% \vsk
%  \ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D'_{2}\setminus D'}
%  {(D_{1}\tensor D'_{1})\tensor (D_{2}\tensor D'_2)\setminus D\tensor D'}{\tensor\And\Or}



