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

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

\begin{proof}
By induction over the derivation of
		$\kiJudge
			{\Gamma, \ a : \kappa_2}
			{\Sigma}
			{\varphi_1}
			{\kappa_1}$ 

\medskip
\tabbedstmts{
(IH) 	\> Substitution holds for all subterms of $\varphi_1$.
	\> (assume) 
}


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$\varphi = a$ / KiVar}

Similarly to Sub. Value/Value TyVar case.


\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$\varphi = \tyForall{b}{\kappa_1}{\tau}$ / KiAll}
$$
	\infer
	{ (\un{1}) \
	  \kiJudge
		{\Gamma, \ a : \kappa_2}
		{\Sigma}
		{\tyForall{b}{\kappa_{11}}{\tau_{12}}}
		{\kappa_1}
	}
	{ (3) \ 
	  \ksJudge
		{\Gamma, \ a : \kappa_2}
		{\Sigma}
		{\kappa_{11}}
		{\omega}
	  \quad
	  (4) \
	  \kiJudge
		{\Gamma, \ a : \kappa_2, \ b : \kappa_{11}}
		{\Sigma}
		{\tau_{12}}
		{\kappa_1}
	}
$$	

\tabbedstmts{
	(\un{2}) 
		\> $\kiJudgeGS{\varphi_2}{\kappa_2}$
		\> (assume)
\\
	(5) 	\> $\ksJudge
			{\Gamma[\varphi_2/a]}
			{\Sigma}
			{\kappa_{11}[\varphi_2/a]}
			{\omega     [\varphi_2/a]}$
		\> (Sub. Type/Kind 3 2)
\\
	(6) 	\> $\kiJudge
			{\Gamma, \ b : \kappa_{11}}
			{\Sigma}
			{\varphi_2}
			{\kappa_2}$
		\> (Weak. Type Env 2)
\\
	(7) 	\> $\kiJudge
			{(\Gamma,~ b:\kappa_{11})[\varphi_2/a]}
			{\Sigma}
			{\tau_{12}	[\varphi_2/a]}
			{\kappa_1	[\varphi_2/a]}$
		\> (IH 4 6)
\\
	(8) 	\> $\kiJudge
			{\Gamma[\varphi_2/a],~ b:\kappa_{11}[\varphi_2/a]}
			{\Sigma}
			{\tau_{12}[\varphi_2/a]}
			{\kappa_1 [\varphi_2/a]}$
		\> (Def. Sub. 7)
\\
	(9) 	\> $\kiJudge
			{\Gamma[\varphi_2/a]}
			{\Sigma}
			{(\tyForall
				{b}
				{\kappa_{11}	[\varphi_2/a]}
				{\tau_{12}	[\varphi_2/a]})}
			{\kappa_1[\varphi_2/a]}$
		\> (KiAll 5 8)
\\
	(10)	\> $\kiJudge
			{\Gamma[\varphi_2/a]}
			{\Sigma}
			{(\tyForall
				{b}
				{\kappa_{11}}
				{\tau_{12}}) [\varphi_2/a]}
			{\kappa_1[\varphi_2/a]}$
		\> (Def. Sub. 9)
}



\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$\varphi = \varphi_1 \ \varphi_2$ / KiApp}
$$
	\infer
	{ (\un{1}) \
	  \kiJudge
		{\Gamma, \ a : \kappa_3}
		{\Sigma}
		{\varphi_1 \ \varphi_2}
		{\kappa_{12} [\varphi_2/b]}
	}
	{ (3) \
	  \kiJudge
		{\Gamma, \ a : \kappa_3}
		{\Sigma}
		{\varphi_1}
		{\kiPi{b}{\kappa_{11}}{\kappa_{12}}}
	  \quad
	  (4) \
	  \kiJudge
		{\Gamma, \ a : \kappa_3}
		{\Sigma}
		{\varphi_2}
		{\kappa_{11}}
	}
$$

\tabbedstmts{
	(\un{2}) 
		\> $\kiJudgeGS{\varphi_3}{\kappa_3}$
		\> (assume)
\\
	(5) 	\> $\kiJudge
			{\Gamma[\varphi_3/a]}
			{\Sigma}
			{\varphi_1[\varphi_3/a]}
			{(\kiPi	{b}
				{\kappa_{11}}
				{\kappa_{12}}) [\varphi_3/a]}$
		\> (IH 4 2)
\\
	(6) 	\> $\kiJudge
			{\Gamma[\varphi_3/a]}
			{\Sigma}
			{\varphi_1[\varphi_3/a]}
			{\kiPi	{b}
				{\kappa_{11}[\varphi_3/a]}
				{(\kappa_{12}[\varphi_3/a])}}$
		\> (Def. Sub. 5)
\\
	(7) 	\> $\kiJudge
			{\Gamma[\varphi_3/a]}
			{\Sigma}
			{\varphi_2[\varphi_3/a]}
			{\kappa_{11}[\varphi_3/a]}$
		\> (IH 5 2)
\\[1ex]
	(8) 	\> ${\Gamma[\varphi_3/a]}
			\: | \:	{\Sigma} \:
			\vdash_{\trm{\tiny{T}}} \	{\varphi_1[\varphi_3/a] \ \varphi_2[\varphi_3/a]}$
\\
		\> \hspace{10ex} $:: \ \ {(\kappa_{12}[\varphi_3/a])[\varphi_2[\varphi_3/a]/b]}$
		\> (KiApp 6 7)
\\[1ex]
	(9) 	\> $\kiJudge
			{\Gamma[\varphi_3/a]}
			{\Sigma}
			{(\varphi_1 \ \varphi_2)[\varphi_3/a]}
			{(\kappa_{12}[\varphi_2/b])[\varphi_3/a]}$
		\> (Def. Sub. 8)
}

\bigskip
The remaining cases are similar to the KiApp case.
\end{proof}


