
For the other direction, we are going to prove a tronger result:
\begin{Theorem}
\label{thm:unif2}
\renewcommand{\GG}{\Psi} For any simple linear term $N_1$ and $N_2$
without shared variables such that $\GG \prv N_1 \hastype A$ and $\GG
\prv N_2 \hastype A$, for every $N$ such that $\GG\vd N_1\mcap
N_{2}\blip N$ if $\GG\prv M\in\|N\|\hastype A$, then $ \GG\prv
M\in\|N_1\|\hastype A$ and $\GG\prv M\in\|N_{2}\|\hastype A$ .
\end{Theorem}
\begin{proof}
\renewcommand{\GG}{\Psi}
By induction on the structure of $\cD::\GG\vd N_1\mcap N_{2}\blip  N$
and inversion on $\cD'::\GG\prv M\in\|N\|\hastype A$.
\bit
\itc $\cD$ ends in $\mcap FF$; by Remark \ref{rmk:compa} and the 
right-to-left direction of Lemma \ref{le:flexunif}.
\itc $\cD$ ends in  $\mcap FR $.
\btab
$\cD::\GG\vd E\ \Phi\mcap c\ \ol{Q_{n}^1} \blip  c\ \Nns$\bh
$\cD_i::\GG\vd E\ \Phi_i\mcap Q_i \blip N_i, 1\leq i\leq n$\bs
$\GG\vd c\ \Mns\in\|c\ \Nns\|$\bh
$\GG\vd M_{i}\in\|Q_{i}\|$ and $\GG\vd M_{i}\in\|E_{i}\ \Phi_{i}\|$
\bi on $\cD_i$\\
$M_{i}\equiv t\ \Phi$, where  $t\equiv \l\Phi\,.\,t_{i}$ 
for  $\Phi_{i}\vd t_{i}\hastype A_{i}$\br $grFlx$\\
$\Phi\vd c\ \ol{t^1_{n}}\hastype a$\` By  rule $\RImp 
E^{n}_{c}$ (Lemma \ref{le:derivec})\\
$\GG\vd c\ \Mns\in\|E\ \Phi\|$\br\\
$\GG\vd c\ \Mns\in\|c\ \ol{Q^1_{n}}\|$\br
\etab
\itc $\cD$ ends in  $\mcap FR^y$. Proceed as above, but using 
Lemma \ref{le:derivey}.
\itc $\cD$ ends in  $\mcap L$; by IH as in Theorem \ref{thm:unif1}
\itc $\cD$ ends in  $\mcap RR$; ditto.
\enit
\end{proof}
