
\theorem{Preservation -- Extension to TyAbsMask}
Extending the previous proof of Preservation to handle TyAbsMask involves replacing the TyApp/EvAppAbs case with the following, and replacing the TySuspend/EvSuspendApp case similarly. This effectively replaces all uses of the TyAbs rule with TyAbsMask. We must also use the Extended Sub. Value/Value and Sub. Type/Value Lemmas discussed in the following sections, instead of the originals.


\bigskip
\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = t_1 \ t_2$ / TyApp + TyAbsMask / EvAppAbs}
$$
 	\infer	
	{ (\un{1}) \ 
	   \tyJudgeES
		{(\teLam{x}{\tau_{11}}{t_{12}}) \ v^\circ}
		{\tau_{12}}
		{\sigma'}
	}
	{ 	\infer 
	  	{ (5) \ 
		  \tyJudgeES
			{\teLam{x}{\tau_{11}}{t_{12}}}
			{\tau_{11} \toa{\sigma'} \tau_{12}}
			{\bot}
		}
		{ \begin{array}{ll}
			&
			(9) \
			\ov{r_i \notin fv(\tau_{11}) \cup fv(\tau_{12})}^{\: i}
			\\
			(7) \ 
			\tyJudge
				{x : \tau_{11}}{\Sigma}
				{t_{12}}
				{\tau_{12}}
				{\sigma}
			&
			(8) \
			\sigma' = \sigma \setminus \ov{(\iRead~ r_i \lor \iWrite~ r_i)}^i
		  \end{array}
		}
		& \quad
		(6) \
		\tyJudgeES
			{v^\circ}
			{\tau_{11}}
			{\bot}
	}
$$	
$$
	(\un{2}) \
	\evJudge	
		{H}
		{(\teLam{x}{\tau_{11}}{t_{12}}) \ v^\circ}
		{H}
		{t_{12}[v^\circ/x]}
$$
\tabbedstmts{
	(\un{3..4})	\> $\Sigma \models H, \ \Sigma \vdash H$
			\> \hspace{-2em}(assume)
\\
	(10)		\> $\tyJudgeES
				{t_{12}[v^\circ/x]}
				{\tau_{12}}
				{\sigma}$ 
			\> \hspace{-2em}(Ext. Sub. Value/Value 7 6)
\\
	(11)		\> $\tyJudgeES
				{t_{12}[v^\circ/x]}
				{\tau_{12}}
				{\sigma \setminus \ov{(\iRead~ r_i \lor \iWrite~ r_i)}^{\: i}}$ 
			\> \hspace{-2em}(TyObs 10 9)
\\
	(12)		\> $\sigma \setminus \ov{(\iRead~ r_i \lor \iWrite~ r_i)}^{\: i} \tle_{\Sigma} \sigma'$
			\> \hspace{-2em}(Def. $\tle$)
}


\clearpage{}
% -----------------------------------------------------------------------------
\lemma{Substitution of Values in Values -- Extension to TyAbsMask}
This Lemma is similar to the original except that we add the following case, and require the top-level type environment to be empty. Requiring the environment to be empty is natural because the term being reduced is closed, and we do not reduce under lambda abstractions. Requiring the top-level type environment to be empty ensures that when we're masking an effect involving some region variable, that variable is not free in the type of the value being substituted.

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




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

$$	\infer
	{ \tyJudge
		{a : \kappa_2 }
		{\Sigma}
		{\teLam{x}{\tau_{11}}{t_{12}}}
		{\sigma}
	}
	{dude}
$$


\lemma{Substitution of Types in Values -- Extension to TyAbsMask}
\statement{
 	If  	&~ $\tyJudge{a : \kappa_2}{\Sigma}{t}{\tau_1}{\sigma}$ 
\\
 	\ and  	&~ $\kiJudgeES
			{\varphi_2}{\kappa_2}$ 
\\
	then	&~ $\tyJudgeES
			{t[\varphi_2/a]}{\tau_1[\varphi_2/a]}{\sigma[\varphi_2/a]}$ \\
}