\begin{Lemma}
\label{le:flexunif}
Let $\godf\vd M\hastype A$ and $\gods\vd M\hastype A$ be \emph{compatible} 
type assignments; then $\godf\vd M\hastype A$ and 
$\gods\vd M\hastype A$ iff $\godt \vd M\hastype A$.
\end{Lemma}
\begin{proof}
($\Imp$). By induction on the structure of $\cD_1::\godf\vd M\hastype A$ and 
$\cD_2::\gods\vd M\hastype A$.  
\bit
\itc 
$$\cD_1=\ianc{c\oftp A\in \Sigma}{\GG_1;\O_1\cdot\vd c\hastype 
C}{Con}\qquad
\cD_2=\ianc{c\oftp A\in \Sigma}{\GG_{2};\O_{2}\cdot\vd c\hastype 
A}{Con}$$
Then
$$\cE=\ianc{c\oftp A\in \Sigma}{(\GG_1\cap\GG_{2});(\O_1,\O_{2});\cdot\vd c\hastype 
A}{Con}$$
\itc 
$$\cD_1=\ianc{}{(\GG_1,x \oftp A);\O_1\cdot\vd x\hastype 
A}{Id^u}\qquad
\cD_2=\ianc{}{(\GG_{2},x \oftp A);\O_{2}\cdot\vd x\hastype 
A}{Id^u}$$
Then
$$\cE=\ianc{}{(\GG_1\cap\GG_{2},x\oftp A);(\O_1,\O_{2});\cdot\vd x\hastype 
A}{Id^u}$$
\itc 
$$\cD_1=\ianc{}{\GG_1;\O_1;x\oftp A\vd x\hastype 
A}{Id^1}\qquad
\cD_2=\ianc{}{\GG_{2};\O_{2};x\oftp A\vd x\hastype 
A}{Id^1}$$
Then
$$\cE=\ianc{}{(\GG_1\cap\GG_{2});(\O_1,\O_{2});x\oftp A\vd x\hastype 
A}{Id^1}$$
\itc
\[
\cD_1 =  \ianc{(\Gamma_1, x\oftp A); \Omega_1; \Delta_1\vd M \hastype B}{\Gamma_1;
\Omega_1; \Delta \vd \lamb{ x^u }{A} M \hastype A \GImp{u}
B}{\GImp{u}I}\]
\[\cD_2 =  \ianc{(\Gamma_2, x\oftp A); \Omega_2; \Delta_{2}\vd M \hastype B}{\Gamma_1;
\Omega_2; \Delta_{2} \vd \lamb{ x^u }{A} M \hastype A \GImp{u}
B}{\GImp{u}I}
\]
\btab
$(\Gamma_1, x\oftp A); \Omega_1; \Delta_1\vd M \hastype B$\bv
$(\Gamma_2, x\oftp A); \Omega_2; \Delta_{2}\vd M \hastype 
B$\bv
$(\Gamma_1, x\oftp A)\cap (\Gamma_2, x\oftp A); (\Omega_1,\O_{2}); 
(\Delta_1,\D_{2})\vd M \hastype B$\bi\\
$(\Gamma_1\cap \GG_{2}, x\oftp A); (\Omega_1,\O_{2}); 
(\Delta_1,\D_2)\vd M \hastype B$\` By De Morgan\\
$\godt \vd \lamb{ x^u }{A} M \hastype A \GImp{u}
B$\br
\etab
\itc $\cD_i$ ends in $\ZImp I, \RImp I$: similarly.
\itc
$$\cD_1= \ibnc{(\Gamma_1, \Delta_N^1); \Omega_1; \Delta_M^1 \vd M \hastype A \RImp 
B}{(\Gamma_1, \Delta_M^1); \Omega_1; \Delta_N^1 \vd N \hastype 
A}{\Gamma_1; 
\Omega_1; (\Delta_M^1, \Delta_N^1) \vd M\ N^1 \hastype B}{\GImp1E}
$$
and
$$\cD_{2}= \ibnc{(\Gamma_{2}, \Delta_N^{2}); \Omega_{2}; \Delta_M^{2} \vd M \hastype A \RImp 
B}{(\Gamma_{2}, \Delta_M^{2}); \Omega_{2}; \Delta_N^{2} \vd N \hastype 
A}{\Gamma_{2}; 
\Omega_{2}; (\Delta_M^{2}, \Delta_N^{2}) \vd M\ N^1 \hastype B}{\GImp1E}
$$
\btab
$(\Gamma_1, \Delta_N^1); \Omega_1; \Delta_M^1 \vd M \hastype A \RImp 
B$\bv
$(\Gamma_{2}, \Delta_N^{2}); \Omega_{2}; \Delta_M^{2} \vd M \hastype A \RImp 
B$\bv
$(\Gamma_1, \Delta_N^1)\cap(\Gamma_{2}, \Delta_N^{2}); 
( \Omega_1,\Omega_{2});(\D_{M}^1, \Delta_M^{2}) \vd M \hastype A \RImp 
B$\bi\\
$(\Gamma_1, \Delta_M^1)\cap(\Gamma_{2}, \Delta_M^{2}); 
( \Omega_1,\Omega_{2});(\D_{N}^1, \Delta_N^{2} )\vd N \hastype A$\bi\\
$(\Gamma_1\cap \Gamma_{2},  \Delta_N^1, \Delta_N^{2}); 
( \Omega_1,\Omega_{2});(\D_{M}^1, \Delta_M^{2}) \vd M \hastype A \RImp 
B$\` By Remark \ref{rmk:compa}\\
$(\Gamma_1\cap \Gamma_{2}); ( \Omega_1,\Omega_{2});( \Delta_M^1,\Delta_M^{2},\D_{N}^1, 
\Delta_N^{2}) \vd N \hastype A$
\` By rule
\etab
\itc $\cD_i$ ends in $\TImp E, \ZImp E$: similarly.
\enit
($\If$). Similarly by induction on the structure of the derivation of\\
$\godt \vd M\hastype A$.
\end{proof}
