\documentclass{article}
\usepackage{latexsym}
\usepackage{lcom}
\usepackage{cdsty}
\input{minml-defns}
\newcommand{\mua}{\mu\alpha .\,}
%\newcommand{\mua}[1]{\mu \alpha .\, {#1}}
\newcommand{\nat}{\mua{\unit + \alpha}}
\newcommand{\unit}{\mbox{$\mathbf{1}$}}
\newcommand{\fold}{\mbox{\textbf{fold}}}
\newcommand{\foldt}{\mbox{\textbf{fold}}^{\mua{\tau}}}
\newcommand{\unfold}{\mbox{\textbf{unfold }}}
\newcommand{\unfoldn}{\mbox{\textbf{unfold}}^{nat}}
\newcommand{\apply}{\mbox{\textbf{apply}}}
\newcommand{\pair}[1]{\langle #1 \rangle}
\newcommand{\ep}{\pair{}}
\newcommand{\inl}[1]{\mbox{\textbf{inl}}^{#1}}
\newcommand{\inlt}{\mbox{\textbf{inl}}^{\tau_1+\tau_2}}
\newcommand{\inrt}{\mbox{\textbf{inr}}^{\tau_1+\tau_2}}
\newcommand{\inr}[1]{\mbox{\textbf{inr}}^{#1}}
\newcommand{\fun}[3]{\mbox{\textbf{fun }} {#1} {#2} \mbox{\textbf{ is }}
 { #3}\mbox{ \textbf{end} }}
\newcommand{\case}[5]{\mbox{\textbf{case }} {#1}\mbox{\textbf{ of }}
  {#2}\Rightarrow {#3}\mid {#4} \Rightarrow  {#5}} 
\newcommand{\caset}{\mbox{\textbf{case }} e'' \mbox{\textbf{ of }}
  \inl{} \ x_1\hastype\tau_1\Rightarrow e_1\mid \inr{} \ x_2\hastype\tau_2 \Rightarrow  e_2}

\begin{document}

For the sake of the following proofs we consider $\ep$ a degenerate
case of the pair construct and we'll omit the correspondent cases.
\newcommand{\et}{e\hastype\tau}
\renewcommand{\q}{[e/x]}
\newcommand{\gex}{\GG[x\oftp\tau]\vd}
We give the definition of substitution for the new constructs;
\beq
\q\inlt e & = & \inlt\q e\\
\q\inrt e & = & \inrt\q e\\
\q\case{e}{x_1\oftp\tau_1}{e_1}{x_2\oftp\tau_2}{e_2} & = &
\case{e}{x_1\oftp\tau_1}{ e_1}{x_2\oftp\tau_2}{ e_2} \\
&&\mbox{if } x\in \{x_1,x_2\}\\
& = & 
\case{e}{x_1\oftp\tau_1}{ e_1}{x_2\oftp\tau_2}{ \q e_2} \\
&&\mbox{if } x=x_1\\
& = & 
\case{e}{x_1\oftp\tau_1}{ \q e_1}{x_2\oftp\tau_2}{ e_2} \\
&&\mbox{if } x=x_2\\
& = & 
\case{\q e}{x_1\oftp\tau_1}{\q e_1}{x_2\oftp\tau_2}{\q e_2} \\
&&\mbox{otherwise}\\
\q\pair{e_1,e_2}& =& \pair{\q e_1}{\q e_2}\\
\q\Bind{p}{e_1}{e_2} & = & \Bind{p}{ \q e_1}{ e_2}\\
&&\mbox{if } x\in FV(p)\\
\q\Bind{p}{e_1}{e_2} & = & \Bind{p}{\q e_1}{\q e_2}\\
&&\mbox{otherwise }
\eneq
\begin{Lemma}[Substitution for sums and products]
If $\gex e'\hastype \tau'$ and $\GG\vd\et$, then
$\GG\vd[e/x]e'\hastype\tau'$. 
\end{Lemma}
\begin{proof}
By induction on the structure of the derivation of $\gex e'\hastype
\tau'$;
\bit
\item[PairType] $e'=\pair{e_1,e_2}$ and $\tau'=\tau_1*\tau_2$.  By
  subderivations $\gex 
  e_1\hastype \tau_1$ and $\gex e_2\hastype \tau_2$; by IH $\GG\vd \q
  e_1\hastype \tau_1$ and $\GG\vd \q e_2\hastype \tau_2$ and by the
  typing rule $\GG\vd \pair{\q e_1,\q e_2}\hastype \tau_1*\tau_2$.  By
  definition of substitution $\GG\vd \q\pair{e_1,e_2}\hastype
  \tau_1*\tau_2$ as required.
\item[InlType] $e'=\inlt{e_1}$ and $\tau'=\tau_+\tau_2$.  By
  subderivations $\gex e_1\hastype \tau_1$ ; by IH $\GG\vd \q
  e_1\hastype \tau_1$ and by the typing rule $\GG\vd \inlt{\q
    e_1}\hastype \tau_1+\tau_2$.  By definition of substitution
  $\GG\vd \q\inlt{e_1}\hastype \tau_1+\tau_2$ as required.
\item[InrType] $e'=\inrt{e_1}$ and $\tau'=\tau_1+\tau_2$. Symmetrical.
\item[CaseType] $e'=\caset$ and $\tau'=\tau''$. By reneaming
  we can choose $x_1,x_2$ such that
  $$\{x_1,x_2\}\cap(FV(e)\cup\{x\}\cup dom(\GG))=\eset$$
By sub-derivation $\gex e''\hastype \tau_1+\tau_2$,
$\GG[x_1\oftp\tau_1]\vd e_1\hastype \tau_1$ and
$\GG[x_2\oftp\tau_2]\vd e_2\hastype \tau_2$. By IH 
$\GG\vd \q e''\hastype \tau_1+\tau_2$,
$\GG[x_1\oftp\tau_1]\vd \q e_1\hastype \tau_1$ and
$\GG[x_2\oftp\tau_2]\vd \q e_2\hastype \tau_2$; by rule $\GG\vd
\case{\q e''}{x_1}{\q e_1}{x_2}{\q e_2}$ and by substitution
$\GG\vd\q\caset\hastype\tau''$ as required.
\item[BindType] $e'=\Bind{p}{e_1}{e_2}$ and $\tau'=\tau''$.  By renaming
  we can choose $p$ such that
  $$FV(p)\cap(FV(e)\cup\{x\}\cup dom(\GG))=\eset$$ By
  sub-derivations 
$\gex e_1\hastype\tau_1$,  $\gex p\hastype\tau_1\gens\GG'$ and $\GG'\vd e_2\hastype\tau_2$. By IH
$\GG\vd \q e_1\hastype\tau_1$. By weakening $\GG'\vd e\hastype\tau$. By IH
$\GG'\vd\q e_2\hastype\tau_ 2$. By strengthening extended to the patterm judgment, 
as $x\not\in FV(p)$ $\GG\vd p\hastype\tau_1\gens\GG'$. By rule $\GG\vd\Bind{p}{\q
  e_1}{\q e_2}\hastype\tau''$ and by substitution $\GG\vd\q\Bind{p}{
  e_1}{e_2}\hastype\tau''$ as required.
  \enit
\end{proof}
 
\begin{Lemma}[Canonical Forms for sums and products]
If $v$ is a closed well formed value of type $\tau$, then:
\ben
\item If $\tau=\tau_1*\tau_2$, then $v=\la v_1,v_2\ra$.
\item If $\tau=\tau_1+\tau_2$, then $v=\inlt v'$ or $v=\inrt v'$.
\enen
\end{Lemma}
\begin{proof}
By induction on the typing judgment, exploiting the definition of value.
\ben
\item Assume $\tau=\tau1*\tau_2$ and $v\hastype\tau$; by inversion on
  the typing rule $v= \la v_1,v_2\ra$ and there is $v_i : \tau_i$ for
  $i=1,2$.  By induction hypothesis $v_i$ is a value. Thus by
  definition of value $\la v1,v2\ra$ is a value. As a special case if
  $\tau=\unit$, then $v=\ep$.
\item Assume $\tau=\tau1+\tau_2$ and $v\hastype\tau$; by inversion on
  the typing rule either $v= \inlt v'$ and $v' : \tau_2$ or $v= \inrt
  v'$ and $v' : \tau_2$. In both cases, by induction hypothesis $v'$
  is a value. Thus by definition of value either $\inlt v'$ or $\inrt
  v'$ is a value.  
\enen
\end{proof}
\include{extra}
\end{document}