\newcommand{\ms}{[\mua/ \alpha]\tau}

% \begin{Lemma}
% If $\tau$ is a type and $\q$ a type substitution, $\q\tau$ is a type.
% \end{Lemma}
% \begin{proof}
% By induction on the definition of type.
% \end{proof}
\renewcommand{\mua}{\mu\alpha .\,\tau}
\renewcommand{\foldt}{\mbox{\textbf{fold}}^{\mua}}
\begin{Lemma}[Canonical Forms for recursive types]
If $v'$ is a value of type $\mua$, then $v'=\foldt v$.
\end{Lemma}
\begin{proof}
By induction on the typing judgment, exploiting the definition of value.
\ben
\item Assume $v'\hastype\mua$; by inversion on
  the typing rule $v'= \foldt v$ and there is $v : [\mua/
  \alpha]\tau$.  By induction hypothesis $v$ is a value. Thus by
  definition of value $\foldt v$ is a value.
\enen
\end{proof}

The Substitution Lemma for terms is by now, straightforward.

\begin{Theorem}[Preservation for recursive types]
Assume $e\mapsto e'$; then if $e\hastype \tau$, then $e'\hastype\tau$.
\end{Theorem}
\begin{proof} By induction on the evaluation rules:
\bit
\item [FoldTest]
$e=\foldt e_1$ and $e'=e'_1$. By inversion $e_1\hastype\ms$. By IH
$e'_1\hastype\ms$ and by rule $\foldt e'_1\hastype\mua$.
\item [UnFoldTest]
$e=\unfold e_1$ and $e'=e'_1$. By inversion $e_1\hastype\mua$. By IH
$e'_1\hastype\mua$ and by rule $\unfold e'_1\hastype\ms$.
\item [FoldBeta]
$e=\unfold(\foldt v)$ and $e'=v$, where $\tau=\ms$. By inversion
$\foldt v\hastype \mua$; by inversion again $e\hastype \ms$ as required.
\enit
\end{proof}
\renewcommand{\mua}{\mu\alpha.\,\tau_1}
\begin{Theorem}[Progress for recursive types]
If $e\hastype \tau$, then either $e$ is a value or there is $e'$ such
that $e\mapsto e'$.
\end{Theorem}
\begin{proof}
By induction on the typing rules.
\bit
\item[TypeFold]$e=\foldt e_1$ and $\tau=\mua$. By IH either $e_1$ is a
  value or there is $e'_1$ such that $e_1\mapsto e'_1$. Subcase $e_1$
  is a value; then by definition of value $e=\foldt e_1$ is a
  value. Subcase $e_1\mapsto e'_1$; by rule $FoldTest$ $\foldt
  e_1\mapsto \foldt e'_1$.
\item[TypeUnfold]$e=\unfold e_1$ and $\tau=\ms$. By IH either $e_1$ is a
  value or there is $e'_1$ such that $e_1\mapsto e'_1$. Subcase $e_1$
  is a value; then by the Canonical Form lemma $e=\foldt v$; by rule
  $Fold Beta$ $\unfold (\foldt v)\mapsto v$.
 Subcase $e_1\mapsto e'_1$; by rule $UnfoldTest$ $\unfold
  e_1\mapsto \unfold e'_1$.
\enit
\end{proof}








