\renewcommand{\inl}{\textsf{inl}\;}
\renewcommand{\inr}{\textsf{inr}\;}
\newcommand{\caseof}[3]{\textsf{case}\,#1\,\textsf{of inl}\,x \Rightarrow #2 \mid \textsf{inr}\,y \Rightarrow #3}


\section{Extension: Disjoint sums}

We will now extend our simply-typed lambda-calculus to disjoint sums.

\[
\begin{array}{llcl}
\mbox{Types}  & A & \bnfas & \ldots \mid A + B\\
\mbox{Terms}  & M & \bnfas & \ldots \mid \inl M \mid \inr M \mid \caseof{M}{N_1}{N_2}
\end{array}
\]

Let us first extend our definition of $\SN$ and $\SNe$ (see Fig.~\ref{fig:sncase}).

\begin{figure}
 \centering

\[
\begin{array}{c}
\multicolumn{1}{l}{\mbox{Neutral terms}} \\% [0.5em]
\infer{\Gamma \vdash \caseof{M}{N_1}{N_2} : C \in \SNe}{\Gamma \vdash M : A + B \in \SNe & \Gamma, x{:}A \vdash N_1 : C \in \SN & \Gamma, y{:}B \vdash N_2 : C\in \SN}
\\% [0.5em]
%
\multicolumn{1}{l}{\mbox{Normal terms}} \\% [0.5em]
\infer{\Gamma \vdash \inl M : A + B \in \SN}{\Gamma \vdash M : A \in \SN} \qquad \infer{\Gamma \vdash \inr M : A + B \in \SN}{\Gamma \vdash M : B \in \SN}
\\% [0.5em]
\multicolumn{1}{l}{\mbox{Strong head reduction}} \\[1em]
\infer{\Gamma \vdash \caseof{(\inl M)}{N_1}{N_2} \redSN [M/x]N_1 : C}{\Gamma \vdash M : A \in \SN & \Gamma, y{:}B \vdash N_2 : C \in \SN}
\\[0.75em]
\infer{\Gamma \vdash \caseof{(\inr M)}{N_1}{N_2} \redSN [M/x]N_2 : C}{\Gamma \vdash M : B \in \SN & \Gamma, x{:}A \vdash N_1 : C \in \SN}
\\[0.75em]
\infer{\Gamma \vdash \caseof{M}{N_1}{N_2} \redSN \caseof{M'}{N_1}{N_2} : C}{\Gamma \vdash M \redSN M' : A + B}
\end{array}
\]

   \caption{Inductive definition of strongly normalizing terms - extended for case-expressions and injections}
   \label{fig:sncase}
 \end{figure}


Next, we extend our definition of semantic type to disjoint sums. A first attempt might be to define $\denot{A + B}$ as follows:

\paragraph{Attempt 1}
\begin{alignat*}{3}
\inden{\Gamma}{M}{A + B} ~\text{iff} &&M = \inl M' &~\text{and}~ \inden{\Gamma}{M'}{A}, \\
& ~~\emph{or}~ &M = \inr M' &~\text{and}~ \inden{\Gamma}{M'}{B}.
% \den{A+B} := \{\inl M \mid M \in \den{A} \} \cup \{\inr M \mid M \in \den{B} \}
\end{alignat*}

However, this definition would not satisfy the key property $\CR3$ and hence would fail to be a reducibility candidate. For example,  while we have $\inden{y : A}{\inl y}{A + B}$, it is not the case that $\inden{y : A}{(\lambda x. \inl x)\;y}{A + B}$, despite the fact that $(\lambda x. \inl x)\;y \redSN \inl y$.
\\[1em]
Our definition of $\denot{A + B}$ is not closed under the reduction relation $\redSN$. Let $\A$ denote the denotation of $\denot{A}$. We then define the closure of $\denot{A} = \A$, written as  $\clos\A$, inductively as follows:

%\[
%\begin{array}{c}
%\ianc{M \in \A}{M\in \clos\A}{}  \qquad
%\ianc{M \in \SNe}{M \in \clos\A}{} \qquad
%\ibnc{M \in \clos\A}{N \redSN M}{N \in \clos\A}{}
%\end{array}
%\]

\[
\begin{array}{c}
\ianc{\Gamma \vdash M \in \A}{\Gamma \vdash M \in \clos\A}{} \qquad
\ianc{\Gamma \vdash M : A \in \SNe}{\Gamma \vdash M \in \clos\A}{} \qquad
\ibnc{\Gamma \vdash M : \clos\A}{\Gamma \vdash N \redSN M : A}{\Gamma \vdash N : \clos\A}{}
\end{array}
\]

and we define

\[
\begin{array}{lcl}
\inden{\Gamma}{M}{A + B} & \text{iff} & \Gamma \vdash M \in \clos{ \{\inl M' \mid \inden{\Gamma}{M'}{A} \} \cup \{\inr M' \mid \inden{\Gamma}{M'}{B} \}  }
\end{array}
\]

\subsection{Semantic type $\denot{A + B}$ is a reducibility candidate}
We first extend our previous theorem which states that all denotations of types must be in $\CR$.

\begin{theorem}
For all types $C$, $\denot{C}  \in \CR$.
\end{theorem}
\begin{proof}
By induction on the structure of $C$. We highlight the case for disjoint sums.

\paragraph{Case $C = A + B$.}

  \begin{enumerate}
  \item \textit{Show} $\CR1$. Assume that $\inden{\Gamma}{M}{A + B}$. We consider different subcases and prove by an induction on the closure defining $\denot{A + B}$ that $\Gamma \vdash M : A + B \in \SN$.

\paragraph{Subcase:} $\Gamma \vdash M \in \{\inl N \mid \inden{\Gamma}{N}{A}\}$. Therefore $M = \inl N$. Since $\inden{\Gamma}{N}{A}$ and by i.h. ($\CR1$), $\Gamma \vdash N : A \in \SN$. By definition of $\SN$, we have that $\Gamma \vdash \inl N : A + B \in \SN$.

\paragraph{Subcase:} $\Gamma \vdash M \in \{\inr N \mid \inden{\Gamma}{N}{B}\}$. Therefore $M = \inr N$. Since $\inden{\Gamma}{N}{B}$ and by i.h. ($\CR1$), $\Gamma \vdash N : B \in \SN$. By definition of $\SN$, we have that $\Gamma \vdash \inr N : A + B \in \SN$.

\paragraph{Subcase:} $\Gamma \vdash M : A + B \in \SNe$. By definition of $\SN$, we conclude that $\Gamma \vdash M : A + B \in \SN$.

\paragraph{Subcase:} $\Gamma \vdash M \redSN M' : A + B$ and $\inden{\Gamma}{M'}{A+B}$.
\\[0.5em]
$\Gamma \vdash M \redSN M' : A + B$ and $\inden{\Gamma}{M'}{A + B}$ \hfill by assumption\\
$\Gamma \vdash M' : A + B \in \SN$ \hfill by inner i.h. \\
$\Gamma \vdash M : A + B \in \SN$ \hfill by reduction $\redSN$

 \item \textit{Show} $\CR2$. If $\Gamma \vdash M : A + B \in \SNe$, then $\inden{\Gamma}{M}{A + B}$. \\
By definition of the closure, if $\Gamma \vdash M : A + B \in \SNe$, we have $\inden{\Gamma}{M}{A + B}$.


  \item \textit{Show} $\CR3$. If $\Gamma \vdash M \redSN M' : A + B$ and $\inden{\Gamma}{M'}{A+B}$
    then $\inden{\Gamma}{M}{A+B}$.\\
By definition of the closure, if $\Gamma \vdash M \redSN M' : A + B$ and $\inden{\Gamma}{M'}{A+B}$, we have
$\inden{\Gamma}{M}{A+B}$.
\end{enumerate}

\end{proof}


 \subsection{Revisiting the fundamental lemma}

 We can now revisit the fundamental lemma.

 \begin{lemma}[Fundamental lemma]
 If $\Gamma \vdash M : C$ and $\inden{\Gamma'}{\sigma}{\Gamma}$
 then $\inden{\Gamma'}{[\sigma]M}{C}$.
 \end{lemma}
 \begin{proof}
 By induction on $\Gamma \vdash M : C$.

 \paragraph{Case} $\D = \ianc{\Gamma \vdash M \hastype A}{\Gamma \vdash \inl M \hastype A + B}{}$
 \\[1em]
 $\inden{\Gamma'}{\sigma}{\Gamma}$ \hfill by assumption \\
 $\inden{\Gamma'}{[\sigma]M}{A}$ \hfill by i.h. \\
 $\inden{\Gamma'}{\inl [\sigma]M}{A + B}$ \hfill by definition of $\denot{A + B}$ \\
 $\inden{\Gamma'}{[\sigma] \inl M}{A + B}$ \hfill by subst. definition

 \paragraph{Case} $\D = \ianc{\Gamma \vdash M \hastype B}{\Gamma \vdash \inr M \hastype A + B}{}$
 \\[1em]
 similar to the case above.

 \paragraph{Case} $\D = \icnc{\Gamma \vdash M : A + B}{\Gamma, x{:}A \vdash M_1 :  C}{\Gamma, y{:}B \vdash M_2 : C}
 {\Gamma \vdash \caseof{M}{M_1}{M_2} : C}{}$
 \\[1em]
 $\inden{\Gamma'}{\sigma}{\Gamma}$ \hfill by assumption \\
 $\inden{\Gamma'}{[\sigma]M}{A + B}$ \hfill by i.h.
 \\[1em]
 We consider different subcases and prove by induction on the closure defining $\denot{A + B}$, that $\inden{\Gamma'}{[\sigma](\caseof{M}{M_1}{M_2})}{C}$.

\paragraph{Subcase $\Gamma' \vdash [\sigma]M \in \{\inl N \mid \inden{\Gamma'}{N}{A}\}$}$\;$\\[1em]
$[\sigma]M = \inl N$ for some $\inden{\Gamma'}{N}{A}$ \hfill by assumption \\
$\Gamma' \vdash N : A \in \SN$ \hfill by $\CR1$ \\
$\Gamma' \vdash \inl N : A + B \in \SN$ \hfill by definition \\
% $x \in \den{A}$,
$\inden{\Gamma'}{\sigma}{\Gamma}$ \hfill by assumption \\
$\inden{\Gamma'}{[\sigma, N/x]}{\Gamma, x:A}$ \hfill by definition \\
$\inden{\Gamma'}{[\sigma, N/x]M_1}{C}$ \hfill by outer i.h \\
$\inden{\Gamma', y{:}B}{y}{B}$  \hfill by definition \\
$\inden{\Gamma', y{:}B}{[\sigma, y/y]}{\Gamma, y:B}$ \hfill by definition \\
$\inden{\Gamma', y{:}B}{[\sigma, y/y]M_2}{C}$ \hfill by outer i.h. \\
$\Gamma', y{:}B \vdash [\sigma, y/y]M_2 : C \in \SN$ \hfill by $\CR1$ \\
$\Gamma' \vdash \caseof{(\inl N)}{[\sigma,x/x]M_1}{[\sigma, y/y]M_2} \redSN [\sigma, N/x]M_1 : C$ \hfill by $\redSN$\\
$\caseof{(\inl N)}{[\sigma,x/x]M_1}{[\sigma, y/y]M_2}$ \\
$\qquad = [\sigma](\caseof{M}{M_1}{M_2}) $ \hfill by subst. definition and $[\sigma]M = \inl N$\\
$\inden{\Gamma'}{[\sigma](\caseof{M}{M_1}{M_2})}{C}$ \hfill by $\CR3$

\paragraph{Subcase $\Gamma' \vdash [\sigma]M \in \{\inr N \mid \inden{\Gamma'}{N}{B}\}$}$\;$\\[1em]
similar to the case above.

\paragraph{Subcase: $\Gamma' \vdash [\sigma]M : A + B \in \SNe$}.$\;$\\
$\inden{\Gamma'}{\sigma}{\Gamma}$ \hfill by assumption \\
$\inden{\Gamma', x{:}A}{x}{A}$ \hfill by definition \\
$\inden{\Gamma', y{:}B}{y}{B}$  \hfill by definition \\
$\inden{\Gamma', x{:}A}{[\sigma, x/x]}{\Gamma, x:A}$ \hfill by definition \\
$\inden{\Gamma', y{:}B}{[\sigma, y/y]}{\Gamma, y:B}$ \hfill by definition \\
$\inden{\Gamma', x{:}A}{[\sigma, x/x]M_1}{C}$ \hfill by outer i.h. \\
$\inden{\Gamma', y{:}B}{[\sigma, y/y]M_2}{C}$ \hfill by outer i.h. \\
$\Gamma', x{:}A \vdash [\sigma, x/x]M_1 : C \in \SN$ \hfill by $\CR1$ \\
$\Gamma', y{:}B \vdash [\sigma, y/y]M_2 : C \in \SN$ \hfill by $\CR1$ \\
$\Gamma' \vdash \caseof{[\sigma]M}{[\sigma, x/x]M_1}{[\sigma, y/y]M_2} : C \in \SNe$ \hfill by $\SNe$ \\
$\Gamma' \vdash [\sigma](\caseof{M}{M_1}{M_2}) : C \in \SNe$ \hfill by substitution def. \\
$\inden{\Gamma'}{[\sigma](\caseof{M}{M_1}{M_2})}{C}$ \hfill by $\CR2$


\paragraph{Subcase: $\Gamma' \vdash [\sigma]M \redSN M' : A + B$ and $\inden{\Gamma'}{M'}{A+B}$}$\;$\\
$\Gamma' \vdash [\sigma]M \redSN M' : A + B$ and $\inden{\Gamma'}{M'}{A+B}$ \hfill by assumption \\
$\inden{\Gamma'}{\caseof{M'}{[\sigma,x/x]M_1}{[\sigma,y/y]M_2}}{C}$ \hfill by inner i.h. \\
$\Gamma' \vdash \caseof{[\sigma]M}{[\sigma,x/x]M_1}{[\sigma,y/y]M_2} $ \\
$\qquad \qquad\redSN
\caseof{M'}{[\sigma,x/x]M_1}{[\sigma,y/y]M_2} : C$ \hfill by $\redSN$\\
$\inden{\Gamma'}{[\sigma](\caseof{M}{M_1}{M_2})}{C}$ \hfill by $\CR3$

\end{proof}


 \section{Extension: Recursion}
 \newcommand{\zero}{\mathsf{z}}
 % \renewcommand{\suc}{\textsf{s}\;}
 % \newcommand{\recnat}[3]{\textsf{rec} (#1,\,#2,\; #3)}
 \newcommand{\recnat}[3]{\recmatch{}{#1}{#2}{#3}}
 % \renewcommand{\nat}{\textsf{Nat}}
 We now extend our simply-typed lambda-calculus to include natural numbers
 defined by $\zero$ and $\suc t$ as well as a primitive recursion operator
 written as $\recnat{M}{M_z}{M_s}$ where $M$ is the argument we recurse over,
 $M_z$ describes the branch taken if $M = \zero$ and $M_s$ describes the branch
 taken when $M = \suc N$ where $n$ will be instantiated with $N$ and $f\;n$
 describes the recursive call.


\[
\begin{array}{llcl}
\mbox{Types}  & A & \bnfas & \ldots \mid \nat \\
\mbox{Terms}  & t & \bnfas & \ldots \mid \zero \mid \suc t \mid \recnat{t}{t_z}{t_s}
\end{array}
\]

To clarify, we give the typing rules for the additional constructs.

\[
\begin{array}{c}
\infer{\Gamma \vdash \zero : \nat}{} \qquad
\infer{\Gamma \vdash \suc M : \nat}{\Gamma \vdash M : \nat}
\\[1em]
\infer{\Gamma \vdash \recnat M {M_z} {M_s} : C}{
\Gamma \vdash M : \nat & \Gamma \vdash M_z : C &
\Gamma, n:\nat,\;f\,n:C \vdash M_s : C}
\end{array}
\]


We again extend our definition of $\SN$ and $\SNe$.

\[
\begin{array}{c}
\multicolumn{1}{l}{\mbox{Neutral terms}} \\[1em]
\infer{\Gamma \vdash \recnat{M}{M_z}{M_s} : C \in \SNe}{\Gamma \vdash M : \nat \in \SNe & \Gamma \vdash M_z : C \in \SN & \Gamma, n \hastype \nat, f~n \hastype C \vdash M_s : C \in \SN}\\[1em]
\multicolumn{1}{l}{\mbox{Normal terms}} \\[1em]
\infer{\Gamma \vdash \zero : \nat \in \SN}{} \qquad \infer{\Gamma \vdash \suc M : \nat \in \SN}{\Gamma \vdash M : \nat \in \SN}\\[1em]
\multicolumn{1}{l}{\mbox{Strong head reduction}} \\[1em]
\infer{\Gamma \vdash \recnat{\zero}{M_z}{M_s} \redSN M_z : C}{\Gamma, n \hastype \nat, f~n \hastype C \vdash M_s : C \in SN} \\[1em]
\infer{\recnat{(\suc N)}{M_z}{M_s} \redSN [N/n,\, f_r/f\,n]M_s : C}{
  \Gamma \vdash N : \nat \in \SN & \Gamma \vdash M_z : C \in \SN & \Gamma, n \hastype \nat, f~n \hastype C \vdash M_s : C \in SN & f_r = \recnat{N}{M_z}{M_s}} \\[1em]
\infer{\Gamma \vdash \recnat{M}{M_z}{M_s} \redSN \recnat{M'}{M_z}{M_s} : C}{\Gamma \vdash M \redSN M' : \nat}
\end{array}
\]

 \section{Extension: Natural numbers}
Here we add natural numbers to our language and show how the language remains normalizing.
\subsection{Semantic type $\denot{\nat}$} We define the denotation of $\nat$ as
 follows:

% \[
% \den{\nat} := \clos{\{\zero\}\cup \{\suc M \mid M \in \den{\nat}\} }
% \]

	\[
	\begin{array}{lcl}
	\inden{\Gamma}{M}{\nat} & \text{iff} & \Gamma \vdash M \in \clos{ \{\zero\}\cup \{\suc M' \mid \inden{\Gamma}{M'}{\nat}\} }
	\end{array}
	\]


\subsection{Semantic type $\denot{\nat}$ is a reducibility candidate}
We again extend our previous theorem which states that all denotations of types must be in $\CR$.

\begin{theorem}
For all types $C$, $\denot{C}  \in \CR$.
\end{theorem}
\begin{proof}
By induction on the structure of $C$. We highlight the case for $\nat$.

\paragraph{Case $C = \nat$.}

\begin{enumerate}
\item \textit{Show} $\CR1$. Assume $\inden{\Gamma}{M}{\nat}$. We consider different subcases
  and prove by induction on the closure defining $\denot{\nat}$ that $\Gamma \vdash M : \nat \in \SN$.
%

\paragraph{Subcase:} $M = \zero$. By definition of $\SN$, $\Gamma \vdash \zero : \nat \in \SN$.

\paragraph{Subcase:} $M = \suc N$ where $\inden{\Gamma}{N}{\nat}$.  By i.h. ($\CR1$),
$\Gamma \vdash N : \nat \in \SN$. By definition of $\SN$, $\Gamma \vdash \suc N : \nat \in \SN$.

 \paragraph{Subcase:} $\Gamma \vdash M  : \nat \in \SNe$. By definition of $\SN$, $\Gamma \vdash M : \nat \in \SN$.

 \paragraph{Subcase:} $\Gamma \vdash M \redSN M' : \nat$ and $\inden{\Gamma}{M'}{\nat}$.
 \\
 $\Gamma \vdash M \redSN M' : \nat$ and $\inden{\Gamma}{M'}{\nat}$ \hfill by assumption \\
 $\Gamma \vdash M' : \nat \in \SN$ \hfill by inner i.h. \\
 $\Gamma \vdash M  : \nat \in \SN$ \hfill by reduction $\redSN$


 \item \textit{Show} $\CR2$. If $\Gamma \vdash M : \nat \in \SNe$, then $\inden{\Gamma}{M}{\nat}.$ \\
	 By definition of the closure, if $\Gamma \vdash M : \nat \in \SNe$, then $\inden{\Gamma}{M}{\nat}$.

 \item \textit{Show} If $\Gamma \vdash M \redSN M' : \nat$ and $\inden{\Gamma}{M'}{\nat}$, then $\inden{\Gamma}{M}{\nat}$. \\
   By definition of the closure, if $\Gamma \vdash M \redSN M' : \nat$ and $\inden{\Gamma}{M'}{\nat}$, we have $\inden{\Gamma}{M}{\nat}$.
 \end{enumerate}
\end{proof}

 \subsection{Revisiting the fundamental lemma}

 We can now revisit the fundamental lemma.
 \begin{lemma}[Fundamental lemma]
 If $\Gamma \vdash M : C$ and $\inden{\Gamma'}{\sigma}{\Gamma}$
 then $\inden{\Gamma'}{[\sigma]M}{C}$.
 \end{lemma}
 \begin{proof}
 By induction on $\Gamma \vdash M : C$.

 \paragraph{Case} $\D = \ianc{}{\Gamma \vdash \zero : \nat}{}$
 \\
 $[\sigma]\zero = \zero$ \hfill by subst. def \\
 $\inden{\Gamma'}{\zero}{\nat}$ \hfill by definition.


 \paragraph{Case} $\D = \ianc{\Gamma \vdash M : \nat}{\Gamma \vdash \suc M :  \nat}{}$
 \\
 $\inden{\Gamma'}{\sigma}{\Gamma}$ \hfill by assumption \\
 $\inden{\Gamma'}{[\sigma]M}{\nat}$ \hfill by i.h. \\
 $\inden{\Gamma'}{\suc [\sigma]M}{\nat}$ \hfill by definition \\
 $\inden{\Gamma'}{[\sigma] \suc M}{\nat}$ \hfill by subst. def


 \paragraph{Case} $\D = \icnc
 {\Gamma \vdash M : \nat}
 {\Gamma \vdash M_z : C}
 {\Gamma, n:\nat,\,f~n:C \vdash M_s : C}
 {\Gamma \vdash \recnat M {M_z} {M_s} : C}{}$
 \\
 $\inden{\Gamma'}{\sigma}{\Gamma}$ \hfill by assumption \\
 $\inden{\Gamma'}{[\sigma]M}{\nat}$ \hfill by i.h. \\[1em]
 We distinguish cases based on $\inden{\Gamma'}{[\sigma]M}{\nat}$ and prove by induction on $\inden{\Gamma'}{[\sigma]M}{\nat}$ that $\inden{\Gamma'}{[\sigma](\recnat M {M_z} {M_s})}{C}$.

 \paragraph{Subcase } $[\sigma]M = \zero$.
 \\
 $\inden{\Gamma', n \hastype \nat, f~n \hastype C}{n}{\nat}$ \hfill by definition of $\SNe$, $\denot{\nat}$ \\
 $\inden{\Gamma', n \hastype \nat, f~n \hastype C}{f~n}{C}$ \hfill by definition of $\SNe$, $\denot{\nat}$ \\
 $\inden{\Gamma', n \hastype \nat, f~n \hastype C}{[\sigma, n/n, f~n/f~n]}{\Gamma, n:\nat, f~n:C}$ \hfill by definition \\
 $\inden{\Gamma', n \hastype \nat, f~n \hastype C}{[\sigma, n/n, f~n/f~n]M_s}{C}$ \hfill by outer i.h. \\
 $\Gamma', n \hastype \nat, f~n \hastype C \vdash [\sigma, n/n, f~n/f~n]M_s : C \in \SN$ \hfill by $\CR1$ \\
 $\inden{\Gamma'}{[\sigma]M_z}{C}$ \hfill by outer i.h. \\
 $\Gamma' \vdash \recnat \zero {[\sigma]M_z} {[\sigma, n/n,f~n/f~n]M_s} \redSN [\sigma]M_z : C$
 \hfill by $\redSN$ \\
 $\recnat \zero {[\sigma]M_z} {[\sigma, n/n,f~n/f~n]M_s}$ \\
 $\qquad = [\sigma](\recnat{M}
 {M_z} {M_s})$ \hfill by subst. def. and $[\sigma]M = \zero$\\
 $\inden{\Gamma'}{[\sigma](\recnat{M} {M_z}{M_s}}{C}$ \hfill by $\CR3$.

 \paragraph{Subcase } $[\sigma]M = \suc M'$ where $\inden{\Gamma'}{M'}{\nat}$.
 \\
 $\inden{\Gamma'}{M'}{\nat}$ \hfill by assumption \\
 $\Gamma \vdash M' : \nat \in \SN$ \hfill by $\CR1$ \\
 $\inden{\Gamma'}{[\sigma]M_z}{C}$ \hfill by outer i.h. \\
 $\Gamma' \vdash [\sigma]M_z \in \SN$ \hfill by $\CR1$ \\
 $\inden{\Gamma', n \hastype \nat, f~n \hastype C}{[\sigma, n/n, f~n/f~n]}{\Gamma, n:\nat, f~n:C}$ \hfill by definition \\
 $\inden{\Gamma', n \hastype \nat, f~n \hastype C}{[\sigma, n/n, f~n/f~n]M_s}{C}$ \hfill by outer i.h. \\
 $\Gamma', n \hastype \nat, f~n \hastype C \vdash [\sigma, n/n, f~n/f~n]M_s : C \in \SN$ \hfill by $\CR1$ \\
 $\inden{\Gamma'}{\recnat{M'}{[\sigma]M_z}{[\sigma, n/n, f~n/f~n]M_s}}{C}$ \hfill by inner i.h. \\
 $\inden{\Gamma'}{[\sigma, M'/n, (\recnat{M'}{[\sigma]M_z}{[\sigma, n/n, f~n/f~n]M_s})/f~n]}{\Gamma, n:\nat, f~n:C}$ \\
 $~$ \hfill by definition \\
 $\inden{\Gamma'}{[\sigma, M'/n, (\recnat{M'}{[\sigma]M_z}{[\sigma, n/n, f~n/f~n]M_s})/f~n]M_s}{C}$ \\
 $~$ \hfill by outer i.h. \\
 $\Gamma' \vdash \recnat{(\suc M')}{[\sigma]M_z}{[\sigma, n/n, f~n/f~n]M_s} $ \\
 $\qquad \qquad \redSN
 [\sigma, M'/n, (\recnat{M'}{[\sigma]M_z}{[\sigma, n/n, f~n/f~n]M_s})/f~n]M_s : C$ \\
 $~$ \hfill by $\redSN$ \\
 $\inden{\Gamma'}{[\sigma](\recnat{M}{M_z}{M_s})}{C}$ \hfill by $\CR3$.

 \paragraph{Subcase } $\Gamma' \vdash [\sigma]M : \nat \in \SNe$. \\
 $\inden{\Gamma'}{[\sigma]M_z}{C}$ \hfill by outer i.h.\\
 $\Gamma' \vdash [\sigma]M_z : C \in \SN$ \hfill by $\CR1$\\
 $\inden{\Gamma', n \hastype \nat, f~n \hastype C}{[\sigma, n/n, f~n/f~n]}{\Gamma, n:\nat, f~n:C}$ \hfill by definition \\
 $\inden{\Gamma', n \hastype \nat, f~n \hastype C}{[\sigma, n/n, f~n/f~n]M_s}{C}$ \hfill by outer i.h. \\
 $\Gamma', n \hastype \nat, f~n \hastype C \vdash [\sigma, n/n, f~n/f~n]M_s : C\in \SN$ \hfill by $\CR1$ \\
 $\Gamma \vdash \recnat{[\sigma]M}{[\sigma]M_z}{[\sigma, n/n, f~n/f~n]M_s} : C \in \SNe$ \hfill by $\SNe$\\
 $\Gamma' \vdash [\sigma](\recnat{M}{M_z}{M_s}) : C \in \SNe$ \hfill by subst. def. \\
 $\inden{\Gamma'}{[\sigma](\recnat{M}{M_z}{M_s})}{C}$ \hfill by $\CR2$.


 \paragraph{Subcase } $\Gamma' \vdash [\sigma]M \redSN M' : \nat$ and $\inden{\Gamma'}{M'}{\nat}$.\\
 $\Gamma' \vdash [\sigma]M \redSN M' : \nat$ and $\inden{\Gamma'}{M'}{\nat}$ \hfill by assumption.\\
 $\inden{\Gamma'}{\recnat{M'}{[\sigma]M_z}{[\sigma,n/n, f~n/f~n]M_s}}{C}$ \hfill by inner i.h. \\
 $\Gamma' \vdash \recnat{[\sigma]M}{[\sigma]M_z}{[\sigma,n/n, f~n/f~n]M_s}$ \\
 $\qquad \qquad \redSN \recnat{M'}{[\sigma]M_z}{[\sigma,n/n, f~n/f~n]M_s} : C$ \hfill by $\redSN$\\
 $\inden{\Gamma'}{[\sigma](\recnat{M}{M_z}{M_s})}{C}$ \hfill by $\CR3$.


 \end{proof}


%  \section{Exercises}
%  \begin{problem}
% % \begin{exercise}
%  The Def. \ref{def:norm}, defines strong normalization informally. We can replace this definition with a more formal definition.

%  \begin{definition}[Inductive definition of strongly normalizing terms] A term $M$ is strongly normalizing, if all its reducts are strongly normalizing, i.e.
%  $M \csn$ if for all $M'$, if $M \red M'$ then $M' \in \csn$.
%  \end{definition}

%  This definition gives rise to an induction principle to reason about strongly normalizing terms. To prove $\forall M \csn. P(M)$, we can assume the property holds for $P(M')$ for any $M'$ s.t. $M \red M'$. Using this induction principle, we can now prove  constructively that any subterm of a strongly normalizing term is itself normalizing.

%  Before we however, precisely define our notion of subterm to simplify our reasoning. We write $M = C[N]$ for $N$ is a subterm of $M$; $C$ denotes an evaluation context, i.e. the term $M$ where we identify $N$ as a subterm at a given position. Evaluation contexts can  be defined as follows.

%  \[
%  \begin{array}{lcl}
%  \mbox{Evaluation Context}\;C & \bnfas & [ ] \mid \lambda x. C \mid C\;N \mid M\;C
%  \end{array}
%  \]

%  As an alternative to the congruence rules, we can redefine evaluation using evaluation contexts:

%  \[
%  \ianc{M \red N}{C[M] \red C[N]}{}
%  \]

% \begin{theorem}
% Any subterm of a strongly normalizing term is strongly normalizing itself, i.e. if $M \csn$ and $N$ is a subterm of $M$, i.e. $M = C[N]$ then $N \in \csn$.
% \end{theorem}
% \end{exercise}
% \end{problem}



% \begin{problem}
%   \begin{exercise}
% Extend the semantic strong normalization proof to treat $A \times B$.
% \begin{itemize}
% \item Extend our definition of normal and neutral terms (i.e. $\SN$ and $\SNe$). You might also need to extend our definition of strong head reduction (i.e. $\redSN$).
% \item Define an appropriate denotation of $\den{A \times B}$.
% % \den{A * B} := {M | \fst(M) \in \den{A} or \snd{M} \in \den{B}}
% \item Show that $\den{A \times B}$ is a reducibility candidate.
% \item Show the additional cases in the fundamental lemma.
% \end{itemize}
%   \end{exercise}
% \end{problem}