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

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

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

\tabbedstmts{
(IH) 	\> Sub. of Types in Kinds holds for all subterms of $\kappa_1$.
	\> (IH) 
}

% -------------------------------------------------------------------------------------------------
\pCase{$\kappa_1 \in \{*,~ \%,~ !,~ Const,~ Mutable,~ Pure\}$}

Trivial, $\kappa_1$ contains no variables.

\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$\kappa_1 = \kappa_{11}~ \varphi_{12}$ / KsApp}
\[
	\infer
	{ (\un{1})~
	  \ksJudge
		{\Gamma,~ a:\kappa_2}
		{\Sigma}
		{\kappa_{11}~ \varphi_{12}}
		{\omega}
	}
	{ (3)~
	  \ksJudge
		{\Gamma,~ a:\kappa_2}
		{\Sigma}
		{\kappa_{11}}
		{\kappa_{12} \to \omega}
	  \quad
	  (4)~
	  \kiJudge
		{\Gamma,~ a:\kappa_2}
		{\Sigma}
		{\varphi_{12}}
		{\kappa_{12}}
	}
\]	

\tabbedstmts{
	(\un{2})	\> $\kiJudgeGS
				{\varphi_2}
				{\kappa_2}$
			\> (assume)
\\
	(5)		\> $\kiJudge
				{\Gamma	  [\varphi_2/a]}
				{\Sigma}
				{\kappa_{11}[\varphi_2/a]}
				{(\kappa_{12} \to \omega) [\varphi_2/a]}$
			\> (IH 3 2)
\\
	(6)		\> $\kiJudge
				{\Gamma	[\varphi_2/a]}
				{\Sigma}
				{\kappa_{11}[\varphi_2/a]}
				{\kappa_{12}[\varphi_2/a] \to \omega[\varphi_2/a]}$
			\> (Def. Sub. 5)
\\
	(7)		\> $\kiJudge
				{\Gamma [\varphi_2/a]}
				{\Sigma}
				{\varphi_{12}	[\varphi_2/a]}
				{\kappa_{12}	[\varphi_2/a]}$
			\> (Sub. Type/Type 4 2)
\\
	(8)		\> $\ksJudge
				{\Gamma [\varphi_2/a]}
				{\Sigma}
				{\kappa_{11} [\varphi_2/a]~~ \varphi_{12}[\varphi_2/a]}
				{\omega	     [\varphi_2/a]}$
			\> (KsApp 6 7)
\\
	(9)		\> $\ksJudge
				{\Gamma [\varphi_2/a]}
				{\Sigma}
				{(\kappa_{11}~ \varphi_{12})[\varphi_2/a]}
				{\omega	[\varphi_2/a]}$
			\> (Def. Sub 8)
}

\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$\kappa_1 = \kiPi{b}{\kappa_{11}}{\kappa_{12}}$ / KsAbs}

\[
	\infer
	{ (\un{1})~
	  \ksJudge
		{\Gamma,~ a:\kappa_3}
		{\Sigma}
		{\kiPi{b}{\kappa_{11}}{\kappa_{12}}}
		{\omega_{12}}
	}
	{ (3)~
	  \ksJudge
		{\Gamma,~ a:\kappa_3}
		{\Sigma}
		{\kappa_{11}}
		{\omega_{11}}
	  \quad
	  (4)~
	  \ksJudge
		{\Gamma,~ a:\kappa_3,~ b:\kappa_{11}}
		{\Sigma}
		{\kappa_{12}}
		{\omega_{12}}
	}
\]

\tabbedstmts{
	(\un{2})	\> $\kiJudgeGS
				{\varphi_2}
				{\kappa_2}$
			\> (assume)
\\
	(5)		\> $\ksJudge
				{\Gamma [\varphi_2/a]}
				{\Sigma}
				{\kappa_{11}[\varphi_2/a]}
				{\omega_{11}[\varphi_2/a]}$
			\> (IH 3 2)
\\
	(6)		\> $\ksJudge
				{(\Gamma,~ b:\kappa_{11})[\varphi_2/a]}
				{\Sigma}
				{\kappa_{12} [\varphi_2/a]}
				{\omega_{12} [\varphi_2/a]}$
			\> (IH 4 2)
\\
	(7)		\> $\ksJudge
				{\Gamma[\varphi_2/a],~ b:\kappa_{11}[\varphi_2/a]}
				{\Sigma}
				{\kappa_{12} [\varphi_2/a]}
				{\omega_{12} [\varphi_2/a]}$
			\> (Def. Sub. 6)
\\
	(8)		\> $\ksJudge
				{\Gamma[\varphi_2/a]}
				{\Sigma}
				{\kiPi{b}{\kappa_{11}[\varphi_2/a]}{\kappa_{12}[\varphi_2/a]}}
				{\omega_{12}[\varphi_2/a]}$
			\> (KsAbs 5 7)
\\
	(9)		\> $\ksJudge
				{\Gamma[\varphi_2/a]}
				{\Sigma}
				{(\kiPi{b}{\kappa_{11}}{\kappa_{12}}) [\varphi_2/a]}
				{\omega_{12}[\varphi_2/a]}$
			\> (Def. Sub 8)
}

\end{proof}
