
\section{Proofs of Language Properties}

Here we present the formal proofs of language properties. Each of these proofs is by induction over the derivation of a typing judgement. When presenting each case, we assume the statement being considered and then invoke the standard inversion lemmas to fill in the appropriate premises.

For example, the proof of Substitution of Values in Values contains the case $\teLAM{a}{\kappa}{t_1}$. We assume the statement 
\ 
	$\tyJudge{\Gamma, \ x : \tau_2}{\Sigma}
		{\teLAM{a}{\kappa}{t_1}}
		{\tyForall{a}{\kappa}{\tau_1}}
		{\sigma}$, 
and use the inversion lemma to give \
 	$\tyJudge
		{\Gamma, \ x : \tau_2, \ a : \kappa}{\Sigma}
		{t_1}
		{\tau_1}
		{\sigma}$

$$
	\frac
	{ (4) \ 
	  \tyJudge
		{\Gamma, \ x : \tau_2, \ a : \kappa}{\Sigma}
		{t_1}
		{\tau_1}
		{\sigma}
	}
	{ (\un{1}) \ 
	  \tyJudge
		{\Gamma, \ x : \tau_2}{\Sigma}
		{\teLAM{a}{\kappa}{t_1}}
		{\tyForall{a}{\kappa}{\tau_1}}
		{\sigma}
	}
$$

\medskip
Each statement is numbered for identification purposes, and we underline the numbers of statements that are assumptions. In some
cases not all statements obtained by the inversion lemmas will be used, but we include them as premises anyway so that the typing rules maintain their familiar shapes.

We will omit the quantifiers ``for all'' and ``for some'' when they are obvious from the context, as they clutter the proof without providing much additional information.

\flushleft
\input{Appendix/Formalities.tex}
\input{Appendix/Lemmas.tex}
\input{Appendix/ProofSubstValuesInValues.tex}
\input{Appendix/ProofSubstTypesInValues.tex}
\input{Appendix/ProofSubstTypesInTypes.tex}
\input{Appendix/ProofSubstTypesInKinds.tex}
\input{Appendix/ProofProgress.tex}
\input{Appendix/ProofPreservation.tex}
\input{Appendix/ProofVisibleActions.tex}
\input{Appendix/ProofCommutableResidues.tex}
\input{Appendix/ProofCommutableActions.tex}
