
\clearpage{}
\begin{lemma}[Substitution of Types in Values]

\medskip
\statement{
 	If  	&~ $\tyJudge{\Gamma, \ a : \kappa_2}{\Sigma}{t}{\tau_1}{\sigma}$ 
\\
 	\ and  	&~ $\kiJudge{\Gamma}{\Sigma}{\varphi_2}{\kappa_2}$ 
\\
	then	&~ $\tyJudge{\Gamma[\varphi_2/a]}{\Sigma}
				{t[\varphi_2/a]}{\tau_1[\varphi_2/a]}{\sigma[\varphi_2/a]}$ \\
}
\end{lemma}

\begin{proof}
By induction over the derivation of $\tyJudge{\Gamma, \ a : \kappa_2}{\Sigma}{t}{\tau_1}{\sigma}$

\tabbedstmts{
	(IH) 
	\> Subst. of Types in Values holds for all subterms of $t$.
	\> (assume) 
}


% -------------------------------------------------------------------------------------------------
\pCase{$t = x$ / TyVar} \\
\pCase{$t = ()$ / TyUnit} \\
\pCase{$t = l$ / TyLoc}

Trivial. No free type vars.


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = \teLAM{a}{\kappa}{t}$ / TyAbsT}
$$	\infer
	{ (\un{1}) \
	  \tyJudge
		{\Gamma, \ a : \kappa_2}
		{\Sigma}
		{\teLAM{a_{11}}{\kappa_{11}}{t_{12}}}
		{\tyForall{a_{11}}{\kappa_{11}}{\tau_{12}}}
		{\sigma_1}
	}
	{ (3) \
	  \tyJudge
	  	{\Gamma, \ a : \kappa_2, \ a_{11} : \kappa_{11}}
		{\Sigma}
		{t_{12}}
		{\tau_{12}}
		{\sigma_1}
	}
$$


\tabbedstmts{
	(\un{2}) 
		\> $\kiJudgeGS{\varphi_2}{\kappa_2}$
		\> (assume)
\\
	(4) 	\> $\kiJudge
			{\Gamma, \ a_{11} : \kappa_{11}}
			{\Sigma}
			{\varphi_2}
			{\kappa_2}$
		\> (Weak. Type Env 2)
\\[1ex]
	(5) 	\> ${(\Gamma, \  a_{11} : \kappa_{11})[\varphi_2/a]} 
			~|~ 	{\Sigma}$
\\
		\> \qq \qq \quad
			$\judge	{t_{12}[\varphi_2/a]} 
			~::~ {\tau_{12}[\varphi_2/a]}
			~;~  {\sigma_1[\varphi_2/a]}$
		\> (IH 3 4)
\\[1ex]
	(6)	\> ${\Gamma[\varphi_2/a], \ a_{11} : \kappa_{11}[\varphi_2/a]} 
			~|~ 	{\Sigma}$
\\
		\> \qq \qq \quad
			$\judge {t_{12}[\varphi_2/a]}
			~::~ {\tau_{12}[\varphi_2/a]}
			~;~  {\sigma_1[\varphi_2/a]}$
		\> (Def. Sub. 5)
\\[1ex]
	(7)	\> ${\Gamma[\varphi_2/a]} \ | \ {\Sigma} \ \ \vdash
			{(\teLAM
				{a_{11}}
				{\kappa_{11}}
				{t_{12}})
				[\varphi_2/a]
			}$
\\
		\> $\hspace{5.2em}
			:: \
			{(\tyForall 
				{a_{11}}
				{\kappa_{11}}
				{\tau_{12}})
				[\varphi_2/a]
			}
			\ ; \ 
			{\sigma_1[\varphi_2/a]}$
		\> (TyAbsT 6, Def. Sub)
}


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = \teLam{x}{\tau_{11}}{t_{12}}$ / TyAbs} \\

Similarly to TyAbsT case


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = t_{11} \ \varphi_{12}$ / TyAppT}
$$	\infer
	{ (\un{1}) \
	  \tyJudge
		{\Gamma, \ a : \kappa_3}
		{\Sigma}
		{t_1 \ \varphi_2}
		{\varphi_{12}[\varphi_2/a_1]}
		{\sigma_1}
	}
	{ (3) \
	  \tyJudge
	  	{\Gamma, \ a : \kappa_3}
		{\Sigma}
		{t_1}
		{\tyForall{a_1}{\kappa_{11}}{\varphi_{12}}}
		{\sigma_1}	
	  \quad
	  (4) \ 
	  \kiJudge
	  	{\Gamma, \ a : \kappa_3}
		{\Sigma}
		{\varphi_2}
		{\kappa_{11}}
	}
$$

\tabbedstmts{
	(\un{2})
		\> $\kiJudgeGS{\varphi_3}{\kappa_3}$
		\> (assume)
\\[1ex]
	(5)	\> ${\Gamma[\varphi_3/a]} ~|~ \Sigma ~\vdash~  t_1[\varphi_3/a]$
\\
		\> \quad
			$::~  (\tyForall{a_1}{\kappa_{11}}{\varphi_{12}})[\varphi_3/a]
			 ~;~  { \sigma_1[\varphi_3/a] }$
		\> (IH 3 2)
\\[1ex]
	(6)	\> ${\Gamma[\varphi_3/a]} ~|~ \Sigma \vdash {t_1[\varphi_3/a]}$
\\
		\> \quad	
			$::~	\tyForall
					{a_1}
					{\kappa_{11}[\varphi_3/a]}
					{\varphi_{12}[\varphi_3/a] }
			~;~	\sigma_1[\varphi_3/a]$
		\> (Def. Sub. 5)
\\[1ex]
	(7)	\> $\kiJudge
			{\Gamma[\varphi_3/a]}
			{\Sigma}
			{\varphi_2[\varphi_3/a]}
			{\kappa_{11}[\varphi_3/a]}$
		\> (Sub. Type/Type 4 2)
\\[1ex]
	(8)	\> ${\Gamma[\varphi_3/a]} \ \arrowvert \ {\Sigma} \vdash {t_1[\varphi_3/a] \ \ \varphi_2[\varphi_3/a]}$
\\
		\> \quad
			$::~ (\varphi_{12}[\varphi_3/a])[\varphi_2[\varphi_3/a]/a_1]
			 ;~  \sigma_1    [\varphi_3/a]$
		\> (TyAppT 6 7)
\\[1ex]
	(9)	\> ${\Gamma[\varphi_3/a]} \ \arrowvert \ {\Sigma} \ \vdash \
			{(t_1 \ \varphi_2)[\varphi_3/a]}$
\\
		\> \quad
			$::~ (\varphi_{12}[\varphi_2/a_1])[\varphi_3/a]
			 ;~ \sigma_1[\varphi_3/a]$
		\> (Def. Sub. 8)
}


\clearpage{}


% -------------------------------------------------------------------------------------------------
\pCase{$t = (t_1 \ t_2)$ / TyApp} \\
Similarly to TyAbsT case


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = \teLetR{r}{\ov{w_i = \delta_i}}{t_1}$ / TyLetRegion}
$$	\infer
	{ (\un{1}) \
	  \tyJudge
		{\Gamma, \ a : \kappa_2}
		{\Sigma}
		{\teLetR{r}{\ov{w_i = \delta_i}}{t_1}}
		{\tau}
		{\sigma}
	}
	{
	  \begin{array}{ll}
		(3) \
		\ov{\delta_i} \ \trm{well formed}
		\\
	  	(4) \
	  	\tyJudge
			{\Gamma, \ a : \kappa_2, \ r : \%, \ \ov{w_i = \kappa_i}}
			{\Sigma}
			{t_1}
			{\tau}
			{\sigma}
	  \end{array}
	  \quad
	  \begin{array}{ll}
		(5) \
		r \notin \ifv(\tau)
		\\
	        (6) \
	  	\ov{\kiJudge
			{\Gamma,~ a : \kappa_2}
			{\Sigma}
			{\delta_i}
			{\kappa_i}}^{~ i}
	  \end{array}
	}
$$

\tabbedstmts{
	(\un{2}) 
		\> $\kiJudgeGS{\varphi_2}{\kappa_2}$
		\> (assume)
\\
	(7) 	\> $\kiJudge
			{\Gamma, \ r : \%, \ \ov{w_i : \kappa_i}}
			{\Sigma}
			{\varphi_2}
			{\kappa_2}$
		\> (Weak. Type Env 2)
\\[1ex]
	(8)	\> ${(\Gamma, \ r : \%, \ \ov{w_i : \kappa_i})[\varphi_2/a]} ~|~ {\Sigma}$
\\
		\> \qq \qq $\vdash {t[\varphi_2/a]}
		    ~::~   {\tau[\varphi_2/a]}
		    ~;~    {\sigma[\varphi_2/a]}$
		\> (IH 4 7)
\\[1ex]
	(9)	\> ${\Gamma[\varphi_2/a], \ r : \%, \ \ov{w_i : \kappa_i[\varphi_2/a]}} ~|~ {\Sigma}$
\\
		\> \qq \qq $\vdash {t[\varphi_2/a]}
		    ~::~  {\tau[\varphi_2/a]}
		    ~;~   {\sigma[\varphi_2/a]}$
		\> (Def. Sub. 8)
\\[1ex]
	(10)	\> $\kiJudge
			{\Gamma[\varphi_2/a]}
			{\Sigma}
			{\delta_i[\varphi_2/a]}
			{\kappa_i[\varphi_2/a]}$
		\> (Sub. Type/Type 6 2)
\\[1ex]
	(11)	\> $\ov{\delta_i[\varphi_2/a]} \ \trm{well formed}$
		\> (Def. Well Formed 6)
\\[1ex]
	(12)	\> ${\Gamma[\varphi_2/a]} \ 
			\arrowvert \ {\Sigma}
			\vdash \ {\teLetR{r}{\ov{w_i = \delta_i[\varphi_2/a]}}{t[\varphi_2/a]}}$
\\
		\> $\hspace{4.8em}
			:: \ {\tau[\varphi_2/a]} \ ; {\sigma[\varphi_2/a]}$
		\> (TyLetRegion 5 9..11)
\\[1ex]
	(13)	\> ${\Gamma[\varphi_2/a]} \
			\arrowvert \ {\Sigma}
			\vdash \ {(\teLetR{r}{\ov{w_i = \delta_i}}{t})[\varphi_2/a]}$
\\
		\> $\hspace{4.8em}
			:: \ {\tau[\varphi_2/a]} \ ; {\sigma[\varphi_2/a]}$
		\> (Def. Sub. 12)
}


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = (\teWithR{\un{\rho}}{\ov{\Delta_i}})$ / TyWithR} \\
\pCase{$t = (\kcase \ t \ \kof \ \ov{K \ \ov{x : \tau} \to t' })$ / TyCase} \\
\pCase{$t = K~ \ov{\varphi}~ \ov{t}$ ~ / TyAlloc} \\
\pCase{$t = update_{K,i}~ \ov{\varphi}~ t_1~ t_2$ / TyUpdate} \\
\pCase{$t = suspend~ \ov{\varphi}~ t_1~ t_2$ / TySuspend} 

Similarly to TyAppT case.

\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = \kmask~ \delta~ \kin~ t$ / TyMask}
$$
	\infer
	{ (\un{1})~
	  \tyJudge
		{\Gamma,~ a_2 : \kappa_2}
		{\Sigma}
		{\kmask~ \delta~ \kin~ t}
		{\tau}
		{\sigma \setminus \sigma'} }
	{ (3)~
	  \tyJudge
		{\Gamma,~ a_2 : \kappa_2}
		{\Sigma}
		{t}
		{\tau}
		{\sigma}
	 \quad
	 (4)~
	 \kiJudge
		{\Gamma,~ a_2 : \kappa_2}
		{\Sigma}
		{\delta}
		{Pure~ \sigma'}
	}
$$
\tabbedstmts{
	(\un{2})	
		\> $\kiJudgeGS{\varphi_2}{\kappa_2}$
		\> (assume)
\\
	(5)	\> $\tyJudge
			{\Gamma[\varphi_2/a]}
			{\Sigma}
			{t      [\varphi_2/a]}
			{\tau   [\varphi_2/a]}
			{\sigma [\varphi_2/a]}$
		\> (IH 3 2)
\\
	(6)	\> $\kiJudge
			{\Gamma[\varphi_2/a]}
			{\Sigma}
			{\delta [\varphi_2/a]}
			{(Pure~ \sigma')[\varphi_2/a]}$
		\> (Sub. Type/Type 4 2)
\\
	(7)	\> $\kiJudge
			{\Gamma[\varphi_2/a]}
			{\Sigma}
			{\delta [\varphi_2/a]}
			{Pure~ \sigma'[\varphi_2/a]}$
		\> (Def. Sub. 6)
\\[1ex]
	(8)	\> ${\Gamma[\varphi_2/a]} 
			~|~     {\Sigma} 
			\vdash~ {\kmask~ \delta[\varphi_2/a]~ \kin~ t[\varphi_2/a]}$
\\
		\> \hspace{4.5em} $::~    {\tau    [\varphi_2/a]}
		    ~;~     {\sigma[\varphi_2/a] / \sigma'[\varphi_2/a]}$
		\> (TyMask 5 7)
\\[1ex]
	(9)	\> ${\Gamma[\varphi_2/a]} 
			~|~ 	{\Sigma}
			\vdash~	{(\kmask~ \delta~ \kin~ t)[\varphi_2/a]}$
\\
		\> \hspace{4.5em} 
		  $ ::~ 	{\tau[\varphi_2/a]}
		   ~;~		{(\sigma \setminus \sigma') [\varphi_2/a]}$
		\> (Def. Sub. 8)
}

\end{proof}