\documentclass{article}
\usepackage{lmodern}%
\usepackage{enumitem}
\usepackage[authoryear]{natbib}

\newtheorem{exercise}{Exercise}[section]
% \newenvironment{exercise}{\begin{@exercise}\rm}{\end{@exercise}}
\newenvironment{ADDITIONAL}[1]{#1}{}
\newenvironment{SOLUTION}[1]{\paragraph*{Solution}\begin{it}#1}{\end{it}}

%\oddsidemargin 0pt
%\evensidemargin \oddsidemargin
%\marginparwidth 0.5in



% \setlength{\topmargin}{15mm}
\setlength{\topmargin}{5mm}

%\setlength{\textwidth}{155mm}
\setlength{\textwidth}{155mm}
%\setlength{\textwidth}{165mm}
\setlength{\textheight}{200mm}
%\setlength{\textheight}{195mm}

\setlength{\evensidemargin}{5mm}
\setlength{\oddsidemargin}{5mm}

\newcommand{\hs}[1]{\hspace{#1}}

% \usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{latexsym}
\usepackage{amsfonts}
\usepackage{listings}
\usepackage{srcltx}
\usepackage{charter}
\usepackage{euler}

\usepackage{latexsym}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{comment}

\ifdefined\studentversion
  \excludecomment{exercise}
  \excludecomment{solution}
  \excludecomment{additional}
\else
% \excludecomment{additional}
\includecomment{exercise}
\includecomment{solution}
\includecomment{additional}
\fi

\newtheorem{@problem}{Exercise}[section]
\newenvironment{problem}{\begin{@problem}\rm}{\end{@problem}}

\newtheorem{@sol}{Solution}[section]
\newenvironment{sol}{\begin{@sol}\rm}{\end{@sol}}

\newcommand{\ext}[1]{\geq_{#1}}

\usepackage{proof}
\usepackage{cdsty}

\newcommand{\nl}{\overline{n}}

\newtheorem{@axiom}{Axiom}
\newenvironment{axiom}{\begin{@axiom}\rm}{\end{@axiom}}
% \newtheorem{@theorem}{Theorem}[section]
% \newenvironment{theorem}{\begin{@theorem}\rm}{\end{@theorem}}

 \newtheorem*{@lemma-nonum}{Lemma}
 \newenvironment{lemma*}{\begin{@lemma-nonum}\rm}{\end{@lemma-nonum}}

 \newtheorem*{@thm-nonum}{Theorem}
 \newenvironment{theorem*}{\begin{@thm-nonum}\rm}{\end{@thm-nonum}}



\input prelude

\usepackage{graphics}
\usepackage{graphicx}

\usepackage{lstextract}

% \includeonly{intro,assign,unif,memo,index,memo-implement,proving}
% \includeonly{index}

\newcommand{\B}{\mathcal{B}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\G}{\mathcal{G}}
\renewcommand{\H}{\mathcal{H}}
\renewcommand{\P}{\mathcal{P}}
\newcommand{\Q}{\mathcal{Q}}

\newcommand{\nf}[2]{#1 : #2 ~\mathsf{nf}}
\newcommand{\neu}[2]{#1 : #2 ~\mathsf{ne}}
\newcommand{\hole}{\mathsf{\_}}
\newcommand{\holetype}{\mathsf{~|~}}


 \newcommand{\one}{1}
\newcommand{\SN}{\mathsf{SN}}
\newcommand{\SNe}{\mathsf{SNe}}
\newcommand{\csn}{\mathsf{sn}}
\newcommand{\CR}{\textsf{CR}}
\newcommand{\denot}[1]{\mathcal{R}_{#1}}
\newcommand{\inden}[3]{#1 \vdash #2 \in \denot{#3}}
\newcommand{\mred}{\longrightarrow^*}
\newcommand{\red}{\longrightarrow}
\newcommand{\redsn}{\longrightarrow_\csn}
\newcommand{\redSN}{\longrightarrow_\SN}
\newcommand{\clos}[1]{\overline{#1}}
\newcommand{\imply}{\Longrightarrow}
\renewcommand{\vec}[1]{\overrightarrow #1}

\newcommand{\id}{\textsf{wk}}
\newcommand{\wk}{\textsf{wk}}

\def\lv{\mathopen{{[\kern-0.14em[}}}    % opening [[ value delimiter
\def\rv{\mathclose{{]\kern-0.14em]}}}   % closing ]] value delimiter
\newcommand{\A}{\mathcal{A}}
% \newcommand{\G}{\mathcal{G}}
\newcommand{\den}[1]{\lv #1 \rv}
\newcommand{\Den}[3][]{\den{#2}^{#1}_{#3}}
\newcommand{\dent}[2]{\llparenthesis#1\rrparenthesis_{#2}}


\long\def\ednote#1{\footnote{[{\it #1\/}]}\message{ednote!}}
% \long\def\note#1{\begin{quote}[{\it #1\/}]\end{quote}\message{note!}}

\begin{document}
\title{POPLMark Reloaded Benchmark: An Introduction \\
-- Work in Progress --}
\author{%
Brigitte Pientka \\ McGill University%
  \and Aliya Hameer \\ McGill University%
  \and Alberto Momigliano \\ University of Milan%
  \and Andreas Abel \\ Chalmers %
%
  }
\date{}
\maketitle

\input{intro.tex}

\section{Defining strongly normalizing terms}
\subsection{Definition of strong normalization via accessibility relation}
Intuitively, a term $M$ is strongly normalizing, if there exists no infinite reduction sequence. Constructively, we can define strong normalization as follows:

\begin{definition}\label{def:norm}
A term $M$ of type $A$ is strongly normalizing, if all its reducts are strongly
normalizing.\\
\[
\infer{\Gamma \vdash M : A \in \csn}
      {\Gamma \vdash M : A & \forall M'.~\Gamma \vdash M \red M' : A \imply \Gamma \vdash M' : A \in \csn}
\]
\end{definition}

The usual definition of strong normalization via accessibility does not only consider well-typed terms. However, as we follow a type-directed reduction strategy, it is natural to define strong normalization on well-typed terms.

From this definition, it easily follows:

 \begin{lemma}[Multi-step Strong Normalization]\label{lm:mredsn}
If  $\Gamma \vdash M \mred M' : B$ and
   $\D:\Gamma \vdash M : B \in \csn$ then $\D':\Gamma \vdash M' : B \in \csn$ and $\D' < \D$.
 \end{lemma}
 \begin{proof}
Induction on $\Gamma \vdash M\mred M' : B$ .

\paragraph{Case} $\ianc{\Gamma \vdash M \red M' : B}{\Gamma \vdash M \mred M' : B}{} \qquad$
\\[1em]
$\D' : \Gamma \vdash M' : B \in \csn$ and $\D' < \D$ \hfill by using $\D:\Gamma \vdash M : B \in \csn$

\paragraph{Case} $ \ibnc{\Gamma \vdash M \red N : B}{\Gamma \vdash N \mred M' : B}
      {\Gamma \vdash M \mred M' : B}{}$
\\[1em]
$\D : \Gamma \vdash M : B \in \csn$ \hfill by assumption\\
$\D_1 : \Gamma \vdash N : B \in \csn$ and $\D_1 < \D$ \hfill by using $\D: \Gamma \vdash M : B \in \csn$\\
$\D_2 : \Gamma \vdash M' : B \in \csn$ and $\D_2 < \D_1$ \hfill by IH using $\D_1$ \\
$\D_2 < \D$ \hfill since $\D_2 < \D_1$ and $\D_1 < \D$

 \end{proof}

To check strong normalizability of a term $M$ it is sufficient to consider every one-step
reduct of $M$ instead of all possible (potentially infinite) reduction sequences. In particular, we can show that it enjoys the expected closure and substitution properties, namely:
\begin{enumerate}
\item $\Gamma \vdash R : A \arrow B \in \csn$ and $\Gamma \vdash N : A \in \csn$
    iff $\Gamma \vdash R~N : B \in \csn$;
  \item $\Gamma, x{:}A \vdash M : B \in \csn$ iff $\Gamma \vdash  \lambda x{:}A.M : A \arrow B \in \csn$;
  \item Let  $\Gamma \vdash R : A \in
   \csn$. Then $\Gamma, x{:}A \vdash M : B \in \csn$ if $\Gamma \vdash [R/x]M : B \in \csn$.
\end{enumerate}


\begin{lemma}[Properties of strongly normalizing terms]\label{lem:psn}$\;$
  \begin{enumerate}
  \item\label{pp3} If $\Gamma \vdash [N/x]M : B \in \csn$ and $\Gamma \vdash N : A$ then $\Gamma, x{:}A \vdash M : B \in \csn$.
  \item\label{pp4} If $\Gamma, x{:}A \vdash M : B \in \csn$ then $\Gamma \vdash  \lambda x{:}A.M : A \arrow B \in \csn$.
  \item\label{pp6} If $\Gamma \vdash M~N : B \in \csn$ then
     $\Gamma \vdash M : A \arrow B \in \csn$ and $\Gamma \vdash N : A\in \csn$.
  \end{enumerate}
\end{lemma}
\begin{proof}
Each property is proven by induction on the first derivation.
\\[1em]
In all the proofs below we silently exploit type uniqueness and do not track explicitly the reasoning about well-typed terms.
\\[1em]
\fbox{\ref{pp3}. If $\Gamma \vdash [N/x]M : B \in \csn$ and $\Gamma \vdash N : A$ then $\Gamma, x{:}A \vdash M : B\in \csn$.}
\\
Induction on $\Gamma \vdash [N/x]M : B \in \csn$. \\[1em]
Assume $\Gamma, x{:}A \vdash M \red M' : B$\\
$\Gamma \vdash [N/x]M \red [N/x]M' : B$ \hfill by Lemma \ref{lem:redsubst}\\
$\Gamma \vdash [N/x]M' : B \in \csn$ \hfill by using  $\Gamma \vdash [N/x]M : B \in \csn$ \\
$\Gamma, x{:}A \vdash M' : B \in \csn$ \hfill by IH\\
$\Gamma, x{:}A \vdash M : B \in \csn$ \hfill since $\Gamma, x{:}A \vdash M \red M' : B$ was arbitrary.
\\[1em]
\fbox{\ref{pp4}. If $\Gamma, x{:}A \vdash M : B \in \csn$ then $\Gamma \vdash  \lambda x{:}A.M : A \arrow B\in \csn$}
\\[1em]
Induction on $\Gamma, x{:}A \vdash M : B \in \csn$. \\[1em]
Assume $\Gamma \vdash \lambda x{:}A.M \red Q : A \arrow B$\\
$\Gamma, x{:}A \vdash M \red M' : B$ and $Q = \lambda x{:}A.M'$ \hfill by reduction rule for $\lambda$.\\
$\Gamma, x{:}A \vdash M' : B \in \csn$ \hfill by assumption $\Gamma, x{:}A \vdash M : B\in \csn$ \\
$\Gamma \vdash \lambda x{:}A.M' : A \arrow B\in \csn$ \hfill by IH \\
$\Gamma \vdash Q : A \arrow B \in \csn$ \hfill since $Q = \lambda x{:}A.M'$\\
$\Gamma \vdash \lambda x.M : A \arrow B \in \csn$ \hfill since $\Gamma \vdash \lambda x.M \red Q : A \arrow B$ was arbitrary
\\[1em]
\fbox{\ref{pp6}. If $\Gamma \vdash M~N : B \in \csn$
                 then $\Gamma \vdash M : A \arrow B \in \csn$ and $\Gamma \vdash N : A \in \csn$.}
\\[1em]
We prove first: If $\Gamma \vdash M~N : B\in \csn$ then $\Gamma \vdash M : A \arrow B\in \csn$.
Proving $\Gamma \vdash M~N : B \in \csn$ implies also $\Gamma \vdash N : A\in \csn$ is similar.
\\
By induction on $\Gamma \vdash M~N : B \in \csn$.
\\[1em]
Assume $\Gamma \vdash M \red M': A \arrow B $\\
$\Gamma \vdash M~N \red M'~N : B $ \hfill by reduction rule for application \\
$\Gamma \vdash M'~N : B \in \csn$ \hfill by assumption $\Gamma \vdash M~N \in \csn$\\
$\Gamma \vdash M' : A \arrow B \in \csn$ \hfill by IH\\
$\Gamma \vdash M  : A \arrow B \in \csn$ \hfill since $\Gamma \vdash M \red M' : A \arrow B$ was arbitrary

\end{proof}

\subsection*{Closure properties of strongly normalizing terms}

Let us begin by contrasting weak and strong normalization. A term $M$ is said to be \emph{weakly} normalising if there is a  rewrite sequence starting in M that eventually ends in a  normal form. A  term $M$ is said to be \emph{strongly} normalising if all rewrite sequences starting in M end eventually in a  normal form.

As pointed out by \cite{Raamsdonk_onnormalisation}, we can easily characterize all weakly normalising terms as follows: a  weakly normalising term is a normal form or can be obtained as the result of some expansion starting in a  normal form. Following this idea, we can then characterize elegantly strongly normalizing terms also as the closure under expansion where expansion is subject to two restrictions: first, the argument of the redex introduced by the expansion step should be in the set of strongly normalising terms, and second, the expansion step should yield a new head redex (backwards closure) or a  new outermost redex in a  term without a  head redex. This idea will form the essence of the closure properties we state next and also gives rise to an inductive definition of strongly normalizing terms which we give in the next section.

\begin{lemma}[Neutral Terms]\label{lm:neu-step}
If $\Gamma \vdash R : A \arrow B$ is neutral and $\Gamma \vdash R~N
\red Q : B$, then $Q$ is neutral\ednote{It might be nice to have a
  judgment form for ``$M$ is neutral''? -ah Yes, indeed it would be
  good to add a judgment. - bp}.
\end{lemma}
\begin{proof}
By induction on $\Gamma \vdash R~N \red Q : B$.

\paragraph{Case}
$\D = \ibnc {\Gamma \vdash \lambda x{:}A.M : A \arrow B}
	          {\Gamma \vdash  N : A}
            {\Gamma \vdash (\lambda x{:}A.M)~N  \red [N/x]M : B }{\beta}$
\\
Contradiction with the assumption $\Gamma \vdash R : A \arrow B$ is neutral.

\paragraph{Case}
$\D = \ibnc {\Gamma \vdash R \red R' : A \arrow B}
	          {\Gamma \vdash N : A}
            {\Gamma \vdash R~N \red R'~N : B}{}$
\\
$\Gamma \vdash R : A \arrow B$ is neutral \hfill by assumption

\paragraph{Sub-case} $R = x$ \\
Contradiction with the assumption $\Gamma \vdash R \red R' : A \arrow B$.

\paragraph{Sub-case} $R = R''~M$ and $R''$ is neutral \\
$R''~M \red R' : A \arrow B$ \hfill by assumption \\
$\Gamma \vdash R' : A \arrow B$ is neutral \hfill by IH \\
$\Gamma \vdash R'~N : B$ is neutral \hfill by definition of neutral terms

\paragraph{Case}
$\D = \ibnc {\Gamma \vdash R : A \arrow B}
	          {\Gamma \vdash N \red N' : A}
            {\Gamma \vdash R~N \red R~N' : B}{}$
\\
$\Gamma \vdash R : A \arrow B$ is neutral \hfill by assumption \\
$\Gamma \vdash R~N' : B$ is neutral \hfill by definition of neutral terms

\end{proof}

We can now state elegantly that strongly normalizing terms are closed under expansion.

\begin{lemma}[Closure properties of neutral terms]\label{lm:closn}$\;$
  \begin{enumerate}
  \item\label{cp2} For all variables $x:A \in \Gamma$, $\Gamma \vdash x : A \in \csn$.
  \item\label{cp3} If $\Gamma \vdash R : A \arrow B \in \csn$ (where $R$ is neutral) and $\Gamma \vdash N : A \in \csn$
     then $\Gamma \vdash R~N : B \in \csn$.

\end{enumerate}
\end{lemma}
\begin{proof}\mbox{}~\\[1em]
\noindent
\fbox{\ref{cp2}.  For all variables $x:A \in \Gamma$, $\Gamma \vdash x : A \in \csn$.}
\\[1em]
$\forall M'.~\Gamma \vdash x \red M' : A \imply \Gamma \vdash M' : A \in \csn$ \hfill since $\Gamma \vdash x \red M'$ is impossible
\\
$\Gamma \vdash x : A $ \hfill since $x:A \in \Gamma$\\
$\Gamma \vdash x : A \in \csn$
\\[1em]
\fbox{\ref{cp3}.  If $\Gamma \vdash R : A \arrow B \in \csn$ (where $R$ is neutral) and $\Gamma \vdash N : A \in \csn$
     then $\Gamma \vdash R~N : B \in \csn$.}
\\[1em]
By simultaneous induction on $\Gamma \vdash R : A \arrow B \in \csn$, $\Gamma \vdash N : A \in \csn$.
\\[1em]
Assume $\Gamma \vdash R~N \red Q : B$

\paragraph{Case}
$\D = \ibnc {\Gamma \vdash \lambda x{:}A.M : A \arrow B}
{\Gamma \vdash  N : A}
{\Gamma \vdash (\lambda x{:}A.M)~N  \red [N/x]M : B }{\beta}$
\\
Contradiction with the assumption $\Gamma \vdash R : A \arrow B$ is neutral.

\paragraph{Case}
$\D = \ibnc {\Gamma \vdash R \red R' : A \arrow B}
{\Gamma \vdash N : A}
{\Gamma \vdash R~N \red R'~N : B}{}$
\\
$\Gamma \vdash R' : A \arrow B \in \csn$ \hfill by using $\Gamma \vdash R : A \arrow B \in \csn$ \\
$\Gamma \vdash R : A \arrow B$ is neutral \hfill by assumption \\
$\Gamma \vdash R \red R' : A \arrow B$ \hfill by assumption \\
$\Gamma \vdash R' N : B$ is neutral \hfill by Lemma \ref{lm:neu-step} \\
$\Gamma \vdash R' : A \arrow B$ is neutral \hfill by definition of neutral terms \\
$\Gamma \vdash R' N : B \in \csn$ \hfill by IH (since $\Gamma \vdash R' : A \arrow B \in \csn$ is smaller)

\paragraph{Case}
$\D = \ibnc {\Gamma \vdash R : A \arrow B}
{\Gamma \vdash N \red N' : A}
{\Gamma \vdash R~N \red R~N' : B}{}$
\\
$\Gamma \vdash N' : A \in \csn$ \hfill by using $\Gamma \vdash N : A \in \csn$ \\
$\Gamma \vdash R~N' : B \in \csn$ \hfill by IH (since $\Gamma \vdash N' : A \in \csn$ is smaller)

\end{proof}

\subsection{Inductive Definition of Strongly Normalizing Terms}
Following \cite{Raamsdonk_onnormalisation} and \cite{Joachimski2003} we define inductively the set of normal terms, $\SN$, and the set of neutral terms, $\SNe$, using the following judgments:

\begin{center}
\begin{tabular}{ll}
$\Gamma \vdash M : A \in \SN$  & $M$ is in the set of normal terms of  type $A$\\
$\Gamma \vdash M : A \in \SNe$ & $M$ is in the set of neutral terms of type $A$
\end{tabular}
\end{center}

Our inductive definition given in Fig.~\ref{fig:sn} tracks typing information, as before. This will allow us to easily extend our framework with the unit type.
As \cite{Raamsdonk_onnormalisation} observed, many proofs, not only normalization proofs, become simpler using the inductive definition, since it allows us  to prove properties by structural induction. This is in contrast to the accessibility notion of strong normalization where we often have to reason about reduction sequences and about positions of terms. As \cite{Joachimski2003}  put it: ``the reduct analysis becomes increasingly annoying in normalization proofs for more and more complex systems.'' Using the inductive definition of normal and neutral terms, we reduce the task of checking all one-step reducts to analysing no more than one standard reduct
and some subterms.  The proof of equivalence between the inductive notion of normalization and the accessibility notion given earlier is in fact the only place where reduct analysis has to be carried out.
Hence this approach seems particularly amendable to mechanizing proofs.

\begin{figure}
  \centering
\[
\begin{array}{c}
\multicolumn{1}{l}{\mbox{Neutral terms}} \\[1em]
\ianc{x{:}A \in \Gamma}{\Gamma \vdash x : A \in \SNe}{} \qquad
\ibnc{\Gamma \vdash R : A \arrow B \in \SNe}{\Gamma \vdash M : A \in \SN}{\Gamma \vdash R\,M : B \in \SNe}{}
\\[1em]
\multicolumn{1}{l}{\mbox{Normal terms}} \\[1em]
\ianc{\Gamma \vdash R : A \in \SNe}{\Gamma \vdash R : A \in \SN}{} \qquad
\ianc{\Gamma, x{:}A \vdash M : A \arrow B \in \SN}{\Gamma \vdash \lambda x{:}A.M : A \arrow B \in \SN}{} \qquad
\ibnc{\Gamma \vdash M \redSN M' : A}{\Gamma \vdash M' : A \in \SN}{\Gamma \vdash M : A \in \SN}{}
\\[1em]
\multicolumn{1}{l}{\mbox{Strong head reduction}} \\[1em]
\ianc{\Gamma \vdash N : A \in \SN \quad \Gamma, x{:}A \vdash M : B}{\Gamma \vdash (\lambda x.M)\;N \redSN [N/x]M : B}{} \qquad
\ianc{\Gamma \vdash R \redSN R' : A \arrow B \quad \Gamma \vdash M : A}{\Gamma \vdash R\,M \redSN R'\,M : B}{}
\end{array}
\]
  \caption{Inductive definition of strongly normalizing terms}
  \label{fig:sn}
\end{figure}

\begin{lemma}\label{lm:neusne}
	If $\Gamma \vdash M : A \in \SNe$ then $\Gamma \vdash M : A$ is neutral.
\end{lemma}
\begin{proof}
By induction on $\Gamma \vdash M : A \in \SNe$.

\paragraph{Case} $\D = \ianc{x{:}A \in \Gamma}{\Gamma \vdash x : A \in \SNe}{}$ \\
$\Gamma \vdash x : A$ is neutral \hfill by definition

\paragraph{Case} $\D = \ibnc{\Gamma \vdash R : A \arrow B \in \SNe}
                            {\Gamma \vdash M : A \in \SN}
                            {\Gamma \vdash R~M : B \in \SNe}{}$ \\
$\Gamma \vdash R : A \arrow B \in \SNe$ \hfill by assumption \\
$\Gamma \vdash R : A \arrow B$ is neutral \hfill by IH \\
$\Gamma \vdash R~M : B$ is neutral \hfill by definition of neutral terms

\end{proof}

We now define $\redsn$ (strong head reduction):

\[
\begin{array}{l}
\infer{\Gamma \vdash (\lambda x.M)\;N \redsn [N/x]M : B}{\Gamma, x{:}A \vdash M : B \quad \Gamma \vdash N : A \in \csn }
\qquad
\infer{\Gamma \vdash M\;N \redsn M'\;N : B}{\Gamma \vdash M \redsn M' : A \arrow B \quad \Gamma \vdash N : A}
\end{array}
\]

\noindent It satisfies a few  key properties:

% \begin{lemma}\label{lm:redsnred}
% If $\Gamma \vdash M \redsn N : B$ then $\Gamma \vdash M \red N : B$.
% \end{lemma}
% \begin{proof}
% Induction on the first derivation.
% \end{proof}

\begin{lemma}\label{lm:bclosed}
If $\Gamma \vdash N : A \in \csn$ and $\Gamma \vdash [N/x]M : B \in \csn$
then $\Gamma \vdash (\lambda x{:}A.M)~N : B \in \csn$.
\end{lemma}
\begin{proof}
Proof by induction -- either $\Gamma, x{:}A \vdash M : B \in \csn$ is getting smaller,
$\Gamma \vdash N : A \in \csn$ is getting smaller, or
$\Gamma \vdash [N/x]M : B \in \SN$  is getting smaller.\\[1em]
Assume $\Gamma \vdash (\lambda x{:}A.M)~N \red P : B$.

\paragraph{Case}
  $\D = \ianc {\Gamma \vdash \lambda x{:}A.M : A \arrow B
         \quad \Gamma \vdash  N : A}
              {\Gamma \vdash (\lambda x{:}A.M)~N  \red [N/x]M : B }{}$ and $ Q = [N/x]M$
 \\
$\Gamma \vdash [N/x]M : B \in \csn$ \hfill by assumption

\paragraph{Case}
 $\D = \ianc {\ianc{\Gamma, x{:}A \vdash M \red M' : B}
                   {\Gamma \vdash \lambda x{:}A.M \red \lambda x{:}A.M' : A \arrow B }{}
        \quad \Gamma \vdash N : A}
             {\Gamma \vdash (\lambda x{:}A.M)~N \red (\lambda x{:}A.M')~N : B}{}$
 and $Q = (\lambda x{:}A.M')~N$
\\[0.5em]
$\Gamma \vdash [N/x]M \red [N/x]M' : B$ \hfill by Lemma \ref{lem:redsubst} \\
$\Gamma \vdash [N/x]M' : B \in \csn$ \hfill using $\Gamma \vdash [N/x]M : B \in \csn$ \\
$\Gamma \vdash N : A \in \csn$ \hfill by assumption \\
% $\Gamma, x{:}A \vdash C[x] : B' \in \csn$ \hfill by assumption \\
$\Gamma \vdash (\lambda x{:}A.M')~N : B$ \hfill by IH (since $\Gamma \vdash [N/x]M' : B \in \csn$ is smaller)

\paragraph{Case}
 $\D = \ianc {\Gamma \vdash \lambda x{:}A.M : A \arrow B
        \quad \Gamma \vdash N \red N' : A}
             {\Gamma \vdash (\lambda x{:}A.M)~N \red (\lambda x{:}A.M)~N' : B}{}$
\\[0.5em]
$\Gamma \vdash \lambda x{:}A.M : A \arrow B$ \hfill by assumption \\
$\Gamma, x{:}A \vdash M : B $ \hfill by inversion on typing\\
$\C : \Gamma \vdash [N/x]M \mred [N'/x]M : B$ and $1 \leq \C$ \hfill by Lemma \ref{lm:mredprop}(\ref{lm:mredsubs}) using $\Gamma \vdash N \red N' : A$\\
% $\Gamma \vdash [N/x]M \red Q : B$ and $\Gamma \vdash Q \mred [N'/x]M : B$ \hfill since $\C \geq 1$ and multi-step red.\\
$\Gamma \vdash [N'/x]M : B \in \csn$ \hfill Lemma \ref{lm:mredsn} using $\Gamma \vdash [N/x]M : B' \in \csn$\\
$\Gamma \vdash N' : A \in \csn$ \hfill using $\Gamma \vdash N : A \in \csn$\\
$\Gamma \vdash (\lambda x{:}A.M)~N' : B \in \csn$ \hfill by IH  (since $\Gamma \vdash N' : A \in \csn$ is smaller)

\end{proof}


\begin{lemma}[Confluence $\csn$]\label{lm:confsn}$\;$
If $\Gamma \vdash M \redsn N : A$ and $\Gamma \vdash M \red N' : A$
  then either $N = N'$ or
  there $\exists Q$ s.t. $\Gamma \vdash N'  \redsn Q : A$
        and $\Gamma \vdash N \mred Q : A$.
\end{lemma}
\begin{proof}
By induction on    $\Gamma \vdash M \redsn N : A$.

\paragraph{Case}
$\D = \ianc{\Gamma \vdash N : A \in \csn \quad \Gamma, x{:}A \vdash M : B}{\Gamma \vdash (\lambda x.M)\;N \redsn [N/x]M : B}{}$
\qquad
$\ianc{\Gamma \vdash \lambda x{:}A.M : A \arrow B \quad \Gamma \vdash  N : A}
      {\Gamma \vdash (\lambda x{:}A.M)~N  \red [N/x]M : B }{}$
\\[1em]
$[N/x]M : B = [N/x]M : B $ \hfill by reflexivity

\paragraph{Case}
$\D = \ianc{\Gamma \vdash N : A \in \csn \quad \Gamma, x{:}A \vdash M : B}{\Gamma \vdash (\lambda x.M)\;N \redsn [N/x]M : B}{}$
\qquad
$\ianc {\Gamma \vdash \lambda x{:}A.M \red \lambda x{:}A.M' : A \arrow B \quad \Gamma \vdash N : A}
       {\Gamma \vdash (\lambda x{:}A.M)~N  \red (\lambda x{:}A.M')~N : B}{}$
\\[0.5em]
$\Gamma, x{:}A \vdash M \red M' : B$ \hfill by inversion \\[0.5em]
WE SHOW: there exists a $Q$ s.t. $\Gamma \vdash (\lambda x{:}A.M')~N  \redsn Q : B$ and
                                 $\Gamma \vdash [N/x]M \mred Q : B$
\\[0.5em]
Let $Q = [N/x]M'$.  \\
$\Gamma \vdash (\lambda x{:}A.M')~N \redsn [N/x]M' : B$ \hfill by def. of $\redsn$\\
$\Gamma \vdash [N/x]M \red [N/x]M' : B$ \hfill by Subst. of typed red. (Lemma \ref{lem:redsubst})\\
$\Gamma \vdash [N/x]M \mred [N/x]M' : B$ \hfill using def. of $\mred$

\paragraph{Case}
$\D = \ianc{\Gamma \vdash N : A \in \csn \quad \Gamma, x{:}A \vdash M : B}{\Gamma \vdash (\lambda x.M)\;N \redsn [N/x]M : B}{}$
\qquad
$\ianc {\Gamma \vdash N\red N' : A  \quad \Gamma \vdash \lambda x{:}A.M : A \arrow B}
       {\Gamma \vdash (\lambda x{:}A.M)~N  \red (\lambda x{:}A.M)~N' : B }{}$
\\[1em]
WE SHOW: there exists a $Q$ s.t. $\Gamma \vdash (\lambda x{:}A.M)~N' \redsn Q : B$ and $\Gamma \vdash  [N/x]M \mred Q : B$\\[0.5em]
Let $Q = [N'/x]M$.\\
$\Gamma \vdash (\lambda x{:}A.M)~N' \redsn [N'/x]M : B$ \hfill by def. of $\redsn$\\
$\Gamma \vdash [N/x]M \mred [N'/x]M : B $ \hfill by Lemma \ref{lm:mredprop}(\ref{lm:mredsubs}) with $\Gamma \vdash N\red N' : A$ and $\Gamma, x{:}A \vdash M : B$

\paragraph{Case}
$\D  = \ianc{\Gamma \vdash M \redsn M_1 : A \arrow B \quad \Gamma \vdash N : A}
            {\Gamma \vdash M\;N \redsn M_1\;N : B}{}$
\qquad
$\ianc {\Gamma \vdash M \red M_2 : A \arrow B \quad \Gamma \vdash N : A}
       {\Gamma \vdash M~N  \red M_2~N : B}{}$
\\[1em]
Either $M_2 = M_1$ or there exists a $P$ s.t. $\Gamma \vdash M_2 \redsn P : A \arrow B$ and $\Gamma \vdash M_1 \mred P : A \arrow B$ \hfill by IH

\paragraph{Sub-case}$M_2 = M_1$
\\[0.5em]
$M_1~N = M_2~N$ \hfill trivial


\paragraph{Sub-case} there exists a $P$ s.t. $\Gamma \vdash M_2 \redsn P : A \arrow B$ and $\Gamma \vdash M_1 \mred P : A \arrow B$\\[1em]
WE SHOW: there exists a $Q$ s.t. $\Gamma \vdash M_2~N \redsn Q : B$ and $\Gamma \vdash  M_1\;N \mred Q : B$
\\[0.5em]
Let $Q = P~N$\\[0.5em]
$\Gamma \vdash M_2~N \redsn P~N : B$ \hfill using def. of $\redsn$ and $\Gamma \vdash M_2 \redsn P : A \arrow B$\\
$\Gamma \vdash M_1\;N \mred P~N : B$ \hfill using Lemma \ref{lm:mredprop} (\ref{lm:mredappl}) on multi-step red. and $\Gamma \vdash M_1 \mred P : A \arrow B$


\paragraph{Case}
$\D  = \ianc{\Gamma \vdash M \redsn M' : A \arrow B \quad \Gamma \vdash N : A}
            {\Gamma \vdash M\;N \redsn M'\;N : B}{}$
\qquad
$\ianc {\Gamma \vdash N\red N' : A  \quad \Gamma \vdash M : A \arrow B}
       {\Gamma \vdash M~N  \red M~N' : B }{}$
\\[1em]
WE SHOW: there exists a $Q$ s.t. $\Gamma \vdash M~N' \redsn Q : B$ and $\Gamma \vdash M'\;N \mred Q : B$
\\[0.5em]
Let $Q = M'~N'$ \\[0.5em]
$\Gamma \vdash M~N' \redsn M'~N' : B$ \hfill by $\Gamma \vdash M \redsn M' : A \arrow B$ \\
$\Gamma \vdash \vdash N\mred N' : A$ \hfill by rule for $\mred$\\
$\Gamma \vdash M'~N \mred M'~N' : B$ \hfill by Multi-Step Reduction (Lemma \ref{lm:mredprop})(\ref{lm:mredappr}))

\end{proof}

\begin{lemma}\label{lm:backclosnaux}
If $\Gamma \vdash N : A \in \csn$, $\Gamma \vdash M : A \arrow B \in \csn$, $\Gamma \vdash M \redsn M': A \arrow B$ and $\Gamma \vdash M'~N : B \in \csn$, then $\Gamma \vdash M~N : B\in \csn$.
\end{lemma}

\begin{proof}
By induction on $\Gamma \vdash N: A \in \csn$ and $\Gamma \vdash M : A \arrow B \in \csn$. \\[1em]
Assume $\Gamma \vdash M~N \red Q : B$.

\paragraph{Case} $\mathcal{D} = \ianc{}{\Gamma \vdash (\lambda x{:}A.M)~N \red [N/x]M : B}{\beta}$
\\[1em]
Contradiction with $\Gamma \vdash (\lambda x{:}A.M) \redsn M' : A \arrow B$.

\paragraph{Case} $\mathcal{D} = \ianc{\Gamma \vdash M \red M'' : A \arrow B}{\Gamma \vdash M\,N \red M''\,N: B}{}$
\\[1em]
To show: $\Gamma \vdash M''\,N \in \csn$.
\\[1em]
$\Gamma \vdash M \red M'' : A $ \hfill by assumption \\
$\Gamma \vdash M \redsn M' : A \arrow B$ \hfill by assumption \\
$\Gamma \vdash M' = M''$ or $\exists P$ s.t. $\Gamma \vdash M'' \redsn P : A \arrow B$ and $\Gamma \vdash M' \mred P: A \arrow B$ \hfill by Conf. Lemma \ref{lm:confsn}

\paragraph{Sub-case} $\Gamma \vdash M' = M''$
\\[1em]
$\Gamma \vdash M'\,N : B \in \csn$ \hfill by assumption \\
$\Gamma \vdash M''\,N : B \in \csn$ \hfill since $M' = M''$

\paragraph{Sub-case} $\exists P$ s.t. $\Gamma \vdash M'' \redsn P : A \arrow B$ and $\Gamma \vdash M' \mred P: A \arrow B$
\\[1em]
$\Gamma \vdash M'~N \mred P~N : A \arrow B$ \hfill by Lemma \ref{lm:mredprop} (\ref{lm:mredappl}) \\
$\Gamma \vdash M'~N : B \in \csn$ \hfill by assumption \\
$\Gamma \vdash P\,N : B \in \csn$ \hfill by Lemma \ref{lm:mredsn} \\
$\Gamma \vdash M'' \redsn P : A \arrow B$ \hfill by assumption \\
$\Gamma \vdash M \red M'' : A \arrow B$ \hfill by assumption \\
$\Gamma \vdash M'' : A \arrow B \in \csn$ \hfill using $\Gamma \vdash M : A \arrow B \in \csn$ \\
$\Gamma \vdash M'': A \arrow B \in \csn$ \hfill using $\Gamma \vdash M : A \arrow B \in \csn$ and $\Gamma \vdash M \red M'' : A \arrow B$\\
$\Gamma \vdash M''\,N : B \in \csn$ \hfill by IH (since $\Gamma \vdash M'': A \arrow B \in \csn$ is smaller) \\
\\[0.5em]

\paragraph{Case} $\mathcal{D} = \ianc{\Gamma \vdash N \red N' : A}{\Gamma \vdash M\,N \red M\,N': B}{}$
\\[1em]
$\Gamma \vdash N \red N' : A $ \hfill by assumption \\
$\Gamma \vdash M \redsn M' : A \arrow B$ \hfill by assumption \\
$\Gamma \vdash M: A \in \csn$ \hfill  by assumption\\
$\Gamma \vdash M'\,N : B \in \csn$ \hfill by assumption\\
$\Gamma \vdash M'\,N': B \in \csn$ \hfill as $M'\,N \red M'\,N'$\\
$\Gamma \vdash N' : A \in \csn$ \hfill using $\Gamma \vdash N : A \in \csn$ and $\Gamma \vdash N \red N' : A$\\
$\Gamma \vdash M\,N' : B \in \csn$ \hfill by IH (since $\Gamma \vdash N': A \in \csn$ is smaller)

\end{proof}

\begin{lemma}[Backward closure of $\csn$]\label{lm:backclosn}$\;$
\\
 If $\Gamma \vdash M \redsn M' : A$ and $\Gamma \vdash M' : A \in \csn$ then
     $\Gamma \vdash M : A \in \csn$.
\end{lemma}
\begin{proof}
By induction on    $\Gamma \vdash M \redsn M' : A$.

\paragraph{Case}
$\D = \ianc{\Gamma \vdash N : A \in \csn \quad \Gamma, x{:}A \vdash M : B}{\Gamma \vdash (\lambda x.M)\;N \redsn [N/x]M : B}{}$
\\[1em]
$\Gamma \vdash  [N/x]M : B \in \csn$ \hfill by assumption \\
$\Gamma \vdash N : A \in \csn $ \hfill by assumption \\
$\Gamma \vdash (\lambda x{:}A.M)~N : B \in \csn$ \hfill by Lemma \ref{lm:bclosed}


\paragraph{Case}
$\D = \ianc{\Gamma \vdash M \redsn M' : A \arrow B \quad \Gamma \vdash N : A}{\Gamma \vdash M\,N \redsn M'\,N : B}{}$
\\[1em]
$\Gamma \vdash M'~N : B \in \csn$ \hfill by assumption \\
$\Gamma \vdash M' : A \arrow B \in \csn$ \hfill by Lemma \ref{lem:psn}(Prop. \ref{pp6})\\
$\Gamma \vdash M : A \arrow B \in \csn$ \hfill by IH \\
$\Gamma \vdash N: A \in \csn$ \hfill by Lemma \ref{lem:psn}(Prop. \ref{pp6}) \\
$\Gamma \vdash M~N : B \in \csn$ \hfill by Lemma \ref{lm:backclosnaux}

\end{proof}

\subsection{Soundness and Completeness}
We can now prove that the two definitions of strongly normalizing terms coincide (soundness and completeness).
For proving normalization, soundness of the inductive definition of $\SN$ suffices.

\begin{theorem}[Soundness of $\SN$]
\mbox{}
  \begin{enumerate}
  \item If $\Gamma \vdash M : A \in \SN$ then $\Gamma \vdash M : A \in \csn$.
  \item If $\Gamma \vdash M : A \in \SNe$ then $\Gamma \vdash M : A \in \csn$.
   \item If $\Gamma \vdash M \redSN M' : A$ then
           $\Gamma \vdash M \redsn M' : A$.
  \end{enumerate}
\end{theorem}
\begin{proof}
By mutual structural induction on the given derivations using the
closure properties. \\[1em]
\noindent
\fbox{1. If $\Gamma \vdash M : A \in \SN$ then $\Gamma \vdash M : A \in \csn$.}\\[1em]
Induction on $\Gamma \vdash M : A \in \SN$.

\paragraph{Case} $\D = \ianc{\Gamma \vdash R : A \in \SNe}{\Gamma \vdash R : A \in \SN}{}$
\\[1em]
$\Gamma \vdash R : A \in \csn$ \hfill by IH(2)

\paragraph{Case} $\D = \ianc{\Gamma, x{:}A \vdash M : B \in \SN}
                           {\Gamma  \vdash \lambda x{:}A.M  : A \arrow B \in \SN}{}$
\\[1em]
$\Gamma, x{:}A \vdash M : B \in \csn$ \hfill by IH(1) \\
$\Gamma \vdash \lambda x{:}A.M : A \arrow B \in \csn$ \hfill by  Property \ref{lem:psn}(\ref{pp4})

\paragraph{Case} $\D = \ibnc{\Gamma \vdash M \redSN M' : A}{
                             \Gamma \vdash M' : A \in \SN}
                            {\Gamma \vdash M  : A \in \SN}{} $
\\[1em]
$\Gamma \vdash M' : A \in \csn$ \hfill by IH(1)\\
$\Gamma \vdash M \redsn M' : A $ \hfill by IH (3) \\
$\Gamma \vdash M : A \in \csn$ \hfill by Backwards Closure (Lemma \ref{lm:backclosn}) 
% $\Gamma \vdash M \redsn M' : A$ \hfill by IH(3)\\
% {\color{red}{$\Gamma \vdash M  : A \in \csn$ \hfill by Closure Property \ref{lm:closn}(\ref{cp5}) -- should be proven differently without using $\redsn$}}
\\[1em]
\fbox{2. If $\Gamma \vdash M : A \in \SNe$ then $\Gamma \vdash M : A \in \csn$.}\\[1em]
Induction on $\Gamma \vdash M : A \in \SNe$.

\paragraph{Case} $\D = \ianc{x : A \in \Gamma}{\Gamma \vdash x : A \in \SNe}{}$ \\
$\Gamma \vdash x: A \in \csn$ \hfill by Lemma \ref{lm:closn} (\ref{cp2})

\paragraph{Case} $\D = \ibnc{\Gamma \vdash R : A \arrow B \in \SNe}
                            {\Gamma \vdash M : A \in \SN}
                            {\Gamma \vdash R~M : B \in \SNe}{}$ \\
$\Gamma \vdash R : A \arrow B \in \csn$ \hfill by IH (2)\\
$\Gamma \vdash M : A \in \csn$ \hfill by IH (1) \\
$\Gamma \vdash R : A \arrow B$ is neutral \hfill by Lemma \ref{lm:neusne} \\
$\Gamma \vdash R~M : B \in \csn$ \hfill by Lemma \ref{lm:closn} (\ref{cp3})
\\[1em]
\fbox{3. If $\Gamma \vdash M \redSN M' : A$ then
           $\Gamma \vdash M \redsn M' : A$.}\\[1em]
Induction on $\Gamma \vdash M \redSN M' : A$

\paragraph{Case}
$\D = \ianc{\Gamma \vdash N : A \in \SN \quad \Gamma, x{:}A \vdash M : B}{\Gamma \vdash (\lambda x.M)\;N \redSN [N/x]M : B}{}$
\\[1em]
$\Gamma \vdash N : A \in \csn$ \hfill by IH (1)\\
$\Gamma \vdash (\lambda x.M)\;N \redsn [N/x]M : B$ \hfill by def. of $\redsn$

\paragraph{Case}
$\D = \ianc{\Gamma \vdash R \redSN R' : A \arrow B \quad \Gamma \vdash M : A}{\Gamma \vdash R\,M \redSN R'\,M : B}{}$
\\[1em]
$\Gamma \vdash R \redsn R' : A \arrow B$ \hfill by IH(3) \\
$\Gamma \vdash  R\,M \redsn R'\,M : B$ \hfill by def. of $\redsn$
\end{proof}

\subsection{Properties of the inductive definition}

\begin{lemma}[$\SN$ and $\SNe$ characterize well-typed terms]\quad
	\begin{enumerate}
		\item If $\Gamma \vdash M : A \in \SN$ then $\Gamma \vdash M : A$.
		\item If $\Gamma \vdash M : A \in \SNe$ then $\Gamma \vdash M : A$.
		\item If $\Gamma \vdash M \redSN M' : A$ then $\Gamma \vdash M : A$ and $\Gamma \vdash M' : A$.
	\end{enumerate}
\end{lemma}
\begin{proof}
	By induction on the definition of $\SN$, $\SNe$, and $\redSN$.
\end{proof}

\begin{lemma}[Renaming]~\label{lm:renameSN}
	\begin{enumerate}
		\item If $\Gamma \vdash M : A \in \SN$ and $\Gamma' \ext{\rho} \Gamma$ then $\Gamma' \vdash [\rho]M : A \in \SN$
		\item If $\Gamma \vdash M : A \in \SNe$ and $\Gamma' \ext{\rho} \Gamma$ then $\Gamma' \vdash [\rho]M : A \in \SNe$
		\item If $\Gamma \vdash M \redSN N : A$ and $\Gamma' \ext{\rho} \Gamma$ then $\Gamma' \vdash [\rho]M \redSN [\rho]N : A$.
	\end{enumerate}
\end{lemma}
\begin{proof}
	By induction on the first derivation.

	\paragraph{Case:} $\D = \ianc{\Gamma \vdash R : A \in \SNe}{\Gamma \vdash R : A \in \SN}{} $
	\\[1em]
	$\Gamma' \vdash [\rho]R : A \in \SNe$ \hfill by IH (2) \\
	$\Gamma' \vdash [\rho]R : A \in \SN$ \hfill by def. of $\SN$

	\paragraph{Case:} $\D = \ianc{\Gamma, x{:}A \vdash M : B \in \SN}{\Gamma \vdash \lambda x{:}A.M : A \arrow B \in \SN}{}$
	\\[1em]
	$\Gamma', x{:}A \ext {\rho, x/x} \Gamma, x{:}A$ \hfill by def. of $\ext{\rho}$\\
	$\Gamma', x{:}A \vdash [\rho, x/x]M : B \in \SN$ \hfill by IH (1) \\
	$\Gamma' \vdash \lambda x{:}A.[\rho, x/x]M : A \arrow B \in \SN$ \hfill by def. of $\SN$\\
	$\Gamma' \vdash [\rho](\lambda x{:}A.M) : A \arrow B \in \SN$ \hfill by subst. def.

	\paragraph{Case:} $\D = \ibnc{\Gamma \vdash M \redSN M' : A}{\Gamma \vdash M' : A \in \SN}{\Gamma \vdash M : A \in \SN}{} $
	\\[1em]
	$\Gamma' \vdash [\rho]M \redSN [\rho]M' : A$ \hfill by IH (3) \\
	$\Gamma' \vdash [\rho]M' : A \in \SN$ \hfill by IH (1)\\
	$\Gamma' \vdash [\rho]M  : A \in \SN$ \hfill by def. of $\SN$

	\paragraph{Case:} $\D = \ianc{x{:}A \in \Gamma}{\Gamma \vdash x : A \in \SNe}{} $
	\\[1em]
	$\Gamma' \ext {\rho} \Gamma$ \hfill by assumption \\
	$\Gamma' \vdash [\rho]x : A$ \hfill by renaming of typing \\
	$\Gamma' \vdash [\rho]x : A \in \SNe$ \hfill by def. of $\SNe$

	\paragraph{Case:} $\D = \ibnc{\Gamma \vdash R : A \arrow B \in \SNe}{\Gamma \vdash M : A \in \SN}{\Gamma \vdash R\,M : A \arrow B \in \SNe}{} $
	\\[1em]
	$\Gamma' \vdash [\rho]R : A \arrow B \in \SNe$ \hfill by IH (2) \\
	$\Gamma' \vdash [\rho]M : A \in \SN$ \hfill by IH (1) \\
	$\Gamma' \vdash [\rho]R~[\rho]M : A \arrow B \in \SNe$ \hfill by def. of $\SNe$\\
	$\gamma' \vdash [\rho](R~M) : B \in \SNe$ \hfill by subst. def.

	\paragraph{Case:}$\D = \ianc{\Gamma, x{:}A \vdash M : B \qquad \Gamma \vdash N : A \in \SN}{\Gamma \vdash (\lambda x{:}A.M)\;N \redSN [N/x]M : B}{} \qquad$
	\\[1em]
	$\Gamma' \vdash [\rho]N : A\in \SN$ \hfill by IH (1) \\
	$\Gamma' \ext{\rho} \Gamma$ \hfill by assumption \\
	$\Gamma', x{:}A \ext{\rho} \Gamma$ \hfill by weakening\\
	$\Gamma', x{:}A \ext{\rho, x/x} \Gamma, x{:}A$ \hfill by def. of weakening subst\\
	$\Gamma', x{:}A \vdash [\rho, x/x]M : B$ \hfill by weakening lemma \\
	$\Gamma' \vdash (\lambda x{:}A.[\rho, x/x]M)~[\rho]N \redSN [\rho, [\rho]N/x]M : B$ \hfill by def. of $\redSN$\\
	$\Gamma' \vdash [\rho]((\lambda x{:}A M)~N) \redSN [\rho]([N/x]M) : B$ \hfill by def. of subst

	\paragraph{Case:}$\D = \ianc{\Gamma \vdash R \redSN R' : A \arrow B \quad \Gamma \vdash M : A}{\Gamma \vdash R\,M \redSN R'\,M : B}{}$\\[1em]
	$\Gamma' \vdash [\rho]R \redSN [\rho]R': A \arrow B$ \hfill by IH(3) \\
	$\Gamma' \vdash [\rho]M : A$ \hfill by weakening of typing \\
	$\Gamma \vdash [\rho]R~[\rho]M \redSN [\rho]R'~[\rho]M : B$ \hfill by def. of $\redSN$\\
	$\Gamma \vdash [\rho](R~M) \redSN [\rho](R'~M) : B$ \hfill by def. of subst.

\end{proof}

\begin{lemma}[Anti-Renaming]~\label{lm:anti-renameSN}
	\begin{enumerate}
		\item If $\Gamma' \vdash [\rho]M : A \in \SN$ and $\Gamma' \ext{\rho} \Gamma$ then $\Gamma \vdash M : A \in \SN$
		\item If $\Gamma' \vdash [\rho]M : A \in \SNe$ and $\Gamma' \ext{\rho} \Gamma$ then $\Gamma \vdash M : A \in \SNe$
		\item If $\Gamma' \vdash [\rho]M \redSN [\rho]N : A$ and $\Gamma' \ext{\rho} \Gamma$ then $\Gamma \vdash M \redSN N : A$.
	\end{enumerate}
\end{lemma}
\begin{proof}
	By induction on the first derivation\ednote{Should the proof be
		expanded. -bp}.
\end{proof}


We will use the extensionality of $\SN$ for function types in the proof of \CR1:

\begin{lemma}[Extensionality of $\SN$]\label{lm:pSN}
	If  $x{:}A \in \Gamma$ and $\Gamma \vdash M~x : B \in \SN$ then $\Gamma \vdash M : A \arrow B \in \SN$.
\end{lemma}
\begin{proof}
	By induction on $\SN$.

	\paragraph{Case:} $\D = \ianc{\Gamma \vdash M~x : B \in \SNe}{\Gamma \vdash M~x : B \in \SN}{} $  \\[1em]
	$\Gamma \vdash M : A \arrow B  \in \SNe$ \hfill by def. of $\SNe$ \\
	$\Gamma \vdash M : A \arrow B \in \SN$ \hfill by def. of $\SN$
	\\[1em]
	\paragraph{Case:} $\D = \ibnc{\Gamma \vdash M~x \redSN Q : B}{\Gamma \vdash Q : B\in \SN}
	{\Gamma \vdash M~x : B \in \SN}{} $
	\\[1em]
	\textbf{Sub-case}: $\Gamma \vdash (\lambda y{:}A.M')~x \redSN [x/y]M' : B$ \\[1em]
	$\Gamma \vdash [x/y]M' : B \in \SN$ \hfill by assumption \\
	$\Gamma, y{:}A \vdash M' : B \in \SN$ \hfill by Anti-Renaming Property (Lemma \ref{lm:anti-renameSN})\\
	$\Gamma \vdash \lambda y{:}A.M' : A \arrow B \in \SN$ \hfill by def. of $\SN$
	\\[1em]
	\textbf{Sub-case}: $\Gamma \vdash M~x \redSN M'~x : B$ and $Q = M'~x$ \\[1em]
	$\Gamma \vdash M \redSN M' : A \arrow B$ \hfill by def. of $\redSN$ \\
	$\Gamma \vdash M' : A \arrow B \in \SN$ \hfill by IH \\
	$\Gamma \vdash M  : A \arrow B \in \SN$ \hfill by def. of $\SN$

	% To Show: \Gamma \vdash M \in \SN$
\end{proof}

\input{reducibility.tex}

\input{extensions.tex}

\bibliographystyle{plainnat}
% \bibliography{../../bibliography/bibi,../../bibliography/bp}
\bibliography{bibi-extract}

\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "sn-proof-short"
%%% End:

%  LocalWords:  Girard Tait llcl lcl redex subterms iff reducts IH
%  LocalWords:  subst subterm todo Girard's instantiation inl inr
%  LocalWords:  subcases Subcase
