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

\statement{
	If  	&~  $\tyJudge{\Gamma, \ x : \tau_2}{\Sigma}{t}{\tau_1}{\sigma}$ \\
	\ and  	&~  $\tyJudge{\Gamma}{\Sigma}{v^\circ}{\tau_2}{\bot}$ \\
	then 	&~  $\tyJudge{\Gamma}{\Sigma}{t[v^\circ/x]}{\tau_1}{\sigma}$ \\
}
\end{lemma}

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

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

% -------------------------------------------------------------------------------------------------
\pCase{$t = y$ / TyVar}

Trivial. $x \neq y$ so $t$ is unaffected.


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = x$ / TyVar}
$$
	{ (\un{1}) \ 
	  \tyJudge
		{\Gamma, \ x : \tau_1, \ x : \tau_2}{\Sigma}
		{x}
		{\tau_1}
		{\bot}
	}
$$	
\tabbedstmts{
	(\un{2})	\> $\tyJudge{\Gamma}{\Sigma}{v^\circ}{\tau_2}{\bot}$
			\> (assume)
\\
	(3) \quad	\> $\tau_1 \equiv \tau_2$
			\> (Def. Type Env 1)
\\
	(4) \quad	\> $\tyJudge{\Gamma}{\Sigma}{x[v^\circ/x]}{\tau_1}{\bot}$
			\> (Def. Sub. 2 3)
}


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = l$ / TyLoc} 

Trivial. Locations do not contain value variables.


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = ()$ / TyUnit} 

Trivial. Unit does not contain value variables. 

\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = \teLAM{a}{\kappa}{t_1}$ / TyAbsT}
$$
	\frac
	{ (3) \ 
	  \tyJudge
		{\Gamma, \ x : \tau_2, \ a : \kappa}{\Sigma}
		{t_1}
		{\tau_1}
		{\bot}
	}
	{ (\un{1}) \ 
	  \tyJudge
		{\Gamma, \ x : \tau_2}{\Sigma}
		{\teLAM{a}{\kappa}{t_1}}
		{\tyForall{a}{\kappa}{\tau_1}}
		{\bot}
	}
$$
\tabbedstmts{
	(\un{2}) 	\> $\tyJudge{\Gamma} {\Sigma} {v^\circ} {\tau_2} {\bot}$
			\> (assume)
\\
	(4)		\> $\tyJudge{\Gamma, \ a : \kappa}{\Sigma}
				{v^\circ}
				{\tau_2}
				{\bot}$
			\> (Weak. Type Env 2)
\\
	(5)		\> $\tyJudge
				{\Gamma, \ a : \kappa}
				{\Sigma}
				{t_1[v^\circ/x]}
				{\tau_1}
				{\bot}$
			\> (IH 3 4)
\\
	(6)		\> $\tyJudge
				{\Gamma}{\Sigma}
				{\teLAM{a}{\kappa}{(t_1[v^\circ/x]})}
				{\tau_1}
				{\bot}$
			\> (TyAbsT 5)
\\
	(7) 		\> $\tyJudge
				{\Gamma}{\Sigma}
				{(\teLAM{a}{\kappa}{t_1})[v^\circ/x]}
				{\tau_1}
				{\bot}$
			\> (Def. Sub. 6)
}


% -------------------------------------------------------------------------------------------------
\pCase{$t = \teLam{x}{\tau}{t_1}$ / TyAbs}

Similarly to TyAbsT case.
\medskip

% -------------------------------------------------------------------------------------------------
\pCase{$t = t_1 \ \varphi_2$ / TyAppT}

$$
	\frac
	{ (3) \ \tyJudge{\Gamma, \ x : \tau_2} 
			{\Sigma} 
			{t_1} 
			{\tyForall{a}{\kappa_{11}}{\varphi_{12}}} 
			{\sigma} 
	  \quad
	  (4) \ \kiJudge{\Gamma, \ x : \tau_2} 
	  		{\Sigma} 
			{\varphi_2} 
			{\kappa_{11}}
	}
	{ (\un{1}) \ \tyJudge
			{\Gamma, \ x : \tau_2} 
			{\Sigma} 
			{t_1 \ \varphi_2} {\varphi_{12}[\varphi_2/a]} 
			{\sigma} 
	}
$$

\tabbedstmts{
	(\un{2}) 	\> $\tyJudge{\Gamma} {\Sigma} {v^\circ} {\tau_2} {\bot}$
			\> (assume)
\\
	(5) 		\> $\tyJudge
				{\Gamma} {\Sigma} 
				{t_1[v^\circ/x]}
				{\tyForall{a}{\kappa_{11}}{\varphi_{12}}}
				{\sigma}$
			\> (IH 3 2)
\\
	(6) 		\> $\kiJudge
				{\Gamma} 
		  		{\Sigma} 
				{\varphi_2} 
				{\kappa_2}$
			\> (Str. Type Env 4)
\\
	(7) 		\> $\tyJudge
				{\Gamma} {\Sigma} 
				{t_1[v^\circ/x] \ \varphi_2}
				{\varphi_{12}[\varphi_2/a]}
				{\sigma}$
			\> (TyAppT 5 6)
\\
	(8) 		\> $\tyJudge
				{\Gamma} {\Sigma}
				{(t_1 \ \varphi_2)[v^\circ/x]}
				{\varphi_{12}[\varphi_2/a]}
				{\sigma}$
			\> (Def. Sub. 7)
}
\medskip


% -------------------------------------------------------------------------------------------------
\pCase{$t = t_1 \ t_2$ / TyApp}
$$	\frac
	{ (3) \ 
	  \tyJudge
		{\Gamma, \ x : \tau_3}
		{\Sigma}
		{t_1}
		{\tau_{11} \toa{\sigma} \tau_{12}}
		{\sigma_1}
	  \quad
	  (4) \ 
	  \tyJudge
	  	{\Gamma, \ x : \tau_3} 
	  	{\Sigma}
		{t_2}
		{\tau_2}
		{\sigma_2}
	}
	{ (\un{1}) \ \tyJudge 
			{\Gamma, \ x : \tau_3}
			{\Sigma} {t_1 \ t_2} {\tau_{12}}
			{\sigma_1 \lor \sigma_2 \lor \sigma} 
	}
$$	

\tabbedstmts{
	(\un{2}) 	\> $\tyJudge{\Gamma} {\Sigma} {v^\circ} {\tau_3} {\bot}$
			\> (assume)
\\
	(5) 		\> $\tyJudgeGS
				{t_1[v^\circ/x]}
				{\tau_{11} \toa{\sigma} \tau_{12}} {\sigma_1}$
			\> (IH 3 2)
\\
	(6) 		\> $\tyJudge{\Gamma} {\Sigma} {t_2[v^\circ/x]} {\tau_2} {\sigma_2}$
			\> (IH 4 2)
\\
	(7) 		\> $\tyJudgeGS 
				{t_1[v^\circ/x] \ t_2[v^\circ/x]} {\tau_{12}} 
				{\sigma_1 \lor \sigma_2 \lor \sigma}$
			\> (TyApp 5 6)
\\
	(8) 		\> $\tyJudgeGS
				{(t_1 \ t_2)[v^\circ/x]} {\tau_{12}}
				{\sigma_1 \lor \sigma_2 \lor \sigma}$
			\> (Def. Sub. 7)
}


\medskip
% ---------------------
\pCase{$t = (\kcase \ t \ \kof \ \ov{K \ \ov{x : \tau} \to t' })$ / TyCase} \\

Similarly to TyApp case.
Uses the following lemma.

\medskip
\statement{
	If  	&~  $\tyJudge
			{\Gamma, \ x : \tau_2}
			{\Sigma}
			{K~ \ov{y} \to t}
			{T~ \varphi~ \ov{\varphi'} \to \tau_1}
			{\sigma}$ \\
	\ and  	&~  $\tyJudgeGS{v^\circ}{\tau_2}{\bot}$ 
\\
	then 	&~  $\tyJudgeGS
			{K~ \ov{y} \to t[v^\circ/x]}
			{T~ \varphi~ \ov{\varphi'} \to \tau_1}
			{\sigma}$ 
}


\medskip
% ---------------------
\pCase{$t = (\kmask \ \delta \ \kin \ t)$ / TyMask} \\
\pCase{$t = (\teLetR{r}{\ov{w_i :: \delta_i}}{t_1})$ / TyLetRegion} \\
\pCase{$t = (\teWithR{\un{\rho}}{\ov{\Delta_i}})$ / TyWithR} \\
\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} 

\medskip
Similarly to TyApp case. Note that value variables do not appear in type (or witness) expressions.
\end{proof}
