\documentclass[12pt,final,notitlepage,onecolumn,german]{article}%
\usepackage[all,cmtip]{xy}
\usepackage{lscape}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{amsmath}%
\setcounter{MaxMatrixCols}{30}
%TCIDATA{OutputFilter=latex2.dll}
%TCIDATA{Version=5.50.0.2960}
%TCIDATA{LastRevised=Sunday, June 05, 2011 22:42:57}
%TCIDATA{<META NAME="GraphicsSave" CONTENT="32">}
%TCIDATA{<META NAME="SaveForMode" CONTENT="1">}
%TCIDATA{BibliographyScheme=Manual}
%BeginMSIPreambleData
\providecommand{\U}[1]{\protect\rule{.1in}{.1in}}
%EndMSIPreambleData
\voffset=-2.5cm
\hoffset=-0.5cm
\setlength\textheight{23cm}
\setlength\textwidth{14.5cm}
\begin{document}

\begin{center}
\textbf{Remarks on Krivine's "Lambda-calculus, types and models", Chapter 1,
\S 2}

Darij Grinberg, 5 June 2011

\textbf{1. Introduction}
\end{center}

The point of this note is to

\textbf{1)} add some lemmata to Chapter 1 \S 2 of [1] (lemmata that are used
in [1] without mention, due to their intuitive obviousness);

\textbf{2)} show that the definition of $\alpha$-equivalence given in [1] is
equivalent to the definition of $\alpha$-equivalence given in some other sources;

\textbf{3)} prove some rules for substitution (in order to answer a
MathOverflow question of myself).

We are going to use the notations and the results of Chapter 1 of [1]. In
particular, the sign $\equiv$ will stand for the $\alpha$-equivalence defined
in [1]. The different notion of $\alpha$-equivalence that we consider will be
denoted by $=^{\alpha}$ (in order not to confuse it with $\equiv$ as long as
it is not yet proven that the two notions are equivalent).

\begin{center}
\textbf{2. Sidenotes to Chapter 1 \S 2 of [1]}
\end{center}

Here come several facts silently used in some proofs in \S 1.2 of [1]. These
facts are all pretty simple, intuitively clear and easy to prove, and I
suspect this is why they have not been explicitly stated in [1]. I am making
them explicit and proving them in detail in order to formalize the theory a
little bit more.

We begin with some properties of bound variables (and their behaviour under substitution).

\begin{quote}
\textbf{Definition:} If $u$ is a term in $L$, let $\operatorname*{BV}u$ denote
the set of bounded variables of the term $u$.
\end{quote}

Before we continue, let us give an inductive method to compute
$\operatorname*{BV}u$ for a term $u$:

If $u=x$ for a variable $x$, then $\operatorname*{BV}u=\varnothing$.

If $u=\left(  v\right)  w$ for terms $v$ and $w$, then $\operatorname*{BV}
u=\left(  \operatorname*{BV}v\right)  \cup\left(  \operatorname*{BV}w\right)
$.

If $u=\lambda xv$ for some variable $x$ and some term $v$, then
$\operatorname*{BV}u=\left\{  x\right\}  \cup\left(  \operatorname*{BV}
v\right)  $.

\begin{quote}
\textbf{Lemma 1.A.} Let $t$, $t_{1}$, $...$, $t_{m}$ be terms in $L$, and
$x_{1}$, $...$, $x_{m}$ be distinct variables. Then, $\operatorname*{BV}%
\left(  t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle \right)
\subseteq\left(  \operatorname*{BV}t\right)  \cup\left(  \operatorname*{BV}%
t_{1}\right)  \cup...\cup\left(  \operatorname*{BV}t_{m}\right)  $.
\end{quote}

\textit{Proof of Lemma 1.A.} We proceed by induction over $t$:

If $t$ is a variable or a term of the form $\left(  u\right)  v$, the
induction step is clear.

Remains to consider the case when $t=\lambda xu$ for some variable $x$ and
some term $u$.

In this case, $\operatorname*{BV}t=\left\{  x\right\}  \cup\left(
\operatorname*{BV}u\right)  $. There are two subcases to consider: the subcase
when $x\in\left\{  x_{1},...,x_{m}\right\}  $ and the subcase when
$x\notin\left\{  x_{1},...,x_{m}\right\}  $.

\textit{First, let us consider the subcase when }$x\in\left\{  x_{1}%
,...,x_{m}\right\}  $\textit{.} In this subcase, let us WLOG assume that
$x=x_{1}$. Thus, $t=\lambda x_{1}u$, so that $\operatorname*{BV}t=\left\{
x_{1}\right\}  \cup\left(  \operatorname*{BV}u\right)  $.

Now, $t=\lambda x_{1}u$ and the definition of $t\left\langle t_{1}%
/x_{1},...,t_{m}/x_{m}\right\rangle $ result in \newline$t\left\langle
t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle =\lambda x_{1}\left(  u\left\langle
t_{2}/x_{2},...,t_{m}/x_{m}\right\rangle \right)  $, so that%
\[
\operatorname*{BV}\left(  t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}%
\right\rangle \right)  =\left\{  x_{1}\right\}  \cup\operatorname*{BV}\left(
u\left\langle t_{2}/x_{2},...,t_{m}/x_{m}\right\rangle \right)  .
\]
Since $\operatorname*{BV}\left(  u\left\langle t_{2}/x_{2},...,t_{m}%
/x_{m}\right\rangle \right)  \subseteq\left(  \operatorname*{BV}u\right)
\cup\left(  \operatorname*{BV}t_{2}\right)  \cup...\cup\left(
\operatorname*{BV}t_{m}\right)  $ by the induction assumption, this becomes
\begin{align*}
&  \operatorname*{BV}\left(  t\left\langle t_{1}/x_{1},...,t_{m}%
/x_{m}\right\rangle \right) \\
&  \subseteq\underbrace{\left\{  x_{1}\right\}  \cup\left(  \operatorname*{BV}%
u\right)  }_{=\operatorname*{BV}t}\cup\left(  \operatorname*{BV}t_{2}\right)
\cup...\cup\left(  \operatorname*{BV}t_{m}\right) \\
&  =\left(  \operatorname*{BV}t\right)  \cup\left(  \operatorname*{BV}%
t_{2}\right)  \cup...\cup\left(  \operatorname*{BV}t_{m}\right)
\subseteq\left(  \operatorname*{BV}t\right)  \cup\left(  \operatorname*{BV}%
t_{1}\right)  \cup...\cup\left(  \operatorname*{BV}t_{m}\right)  .
\end{align*}


\textit{Now, let us consider the subcase when }$x\notin\left\{  x_{1}%
,...,x_{m}\right\}  $. In this subcase, $t=\lambda xu$ and the definition of
$t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle $ result in
$t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle =\lambda x\left(
u\left\langle t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle \right)  $. Thus,
\[
\operatorname*{BV}\left(  t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}%
\right\rangle \right)  =\left\{  x\right\}  \cup\operatorname*{BV}\left(
u\left\langle t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle \right)  .
\]
Since $\operatorname*{BV}\left(  u\left\langle t_{1}/x_{1},...,t_{m}%
/x_{m}\right\rangle \right)  \subseteq\left(  \operatorname*{BV}u\right)
\cup\left(  \operatorname*{BV}t_{1}\right)  \cup...\cup\left(
\operatorname*{BV}t_{m}\right)  $ by the induction assumption, this becomes%
\begin{align*}
\operatorname*{BV}\left(  t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}%
\right\rangle \right)   &  \subseteq\underbrace{\left\{  x\right\}
\cup\left(  \operatorname*{BV}u\right)  }_{=\operatorname*{BV}t}\cup\left(
\operatorname*{BV}t_{1}\right)  \cup...\cup\left(  \operatorname*{BV}%
t_{m}\right) \\
&  =\left(  \operatorname*{BV}t\right)  \cup\left(  \operatorname*{BV}%
t_{1}\right)  \cup...\cup\left(  \operatorname*{BV}t_{m}\right)  .
\end{align*}


In both subcases, we have proven that $\operatorname*{BV}\left(  t\left\langle
t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle \right)  \subseteq\left(
\operatorname*{BV}t\right)  \cup\left(  \operatorname*{BV}t_{1}\right)
\cup...\cup\left(  \operatorname*{BV}t_{m}\right)  $. This completes the
induction and thus proves Lemma 1.A.

Lemma 1.A is used in the proof of Lemma 1.12 in [1]. (In fact, this proof
claims that "no bound variable of this term is free in $\underline{u}%
_{1},...,\underline{u}_{n}$"\ \ \ \ \footnote{Here, "this term" refers to the
term $\underline{t}\left\langle \underline{t}_{1}/x_{1},...,\underline{t}%
_{m}/x_{m}\right\rangle $.}. The reason why this is true is the following:
Lemma 1.A yields that $\operatorname*{BV}\left(  \underline{t}\left\langle
\underline{t}_{1}/x_{1},...,\underline{t}_{m}/x_{m}\right\rangle \right)
\subseteq\left(  \operatorname*{BV}\underline{t}\right)  \cup\left(
\operatorname*{BV}\underline{t}_{1}\right)  \cup...\cup\left(
\operatorname*{BV}\underline{t}_{m}\right)  $, and we know that no bound
variable of any of the terms $\underline{t},\underline{t}_{1}%
,...,\underline{t}_{m}$ is free in $\underline{u}_{1},...,\underline{u}_{n}$.)

\begin{quote}
\textbf{Lemma 1.B.} Let $u$ be a term in $L$, and let $x$ and $y$ be two
variables. Then, $\operatorname*{BV}\left(  u\left\langle y/x\right\rangle
\right)  \subseteq\operatorname*{BV}u$.
\end{quote}

\textit{Proof of Lemma 1.B.} Apply Lemma 1.A to $m=1$, $t_{1}=y$, $x_{1}=x$
and $t=u$. This yields $\operatorname*{BV}\left(  u\left\langle
y/x\right\rangle \right)  \subseteq\left(  \operatorname*{BV}u\right)
\cup\underbrace{\left(  \operatorname*{BV}y\right)  }_{=\varnothing
}=\operatorname*{BV}u$, and thus Lemma 1.B is proven.

Lemma 1.B is used in the proof of Proposition 1.6 in [1]. (Namely, when this
proof says "the induction hypothesis gives", it silently uses the fact that no
free variable in $t_{1},...,t_{k}$ is bound in $u\left\langle y/x\right\rangle
$ or $u^{\prime}\left\langle y/x^{\prime}\right\rangle $ (this must be
guaranteed, lest we could not apply the induction hypothesis!). This holds
because Lemma 1.B yields $\operatorname*{BV}\left(  u\left\langle
y/x\right\rangle \right)  \subseteq\operatorname*{BV}u\subseteq\left\{
x\right\}  \cup\left(  \operatorname*{BV}u\right)  =\operatorname*{BV}t$
(since $t=\lambda xu$) and $\operatorname*{BV}\left(  u^{\prime}\left\langle
y/x^{\prime}\right\rangle \right)  \subseteq\operatorname*{BV}t^{\prime}$ (for
similar reasons), and because we know that no free variable in $t_{1}%
,...,t_{k}$ is bound in $t$ or $t^{\prime}$.)

Next some lemmata about free variables:

\begin{quote}
\textbf{Definition:} If $u$ is a term in $L$, let $\operatorname*{FV}u$ denote
the set of free variables of the term $u$.
\end{quote}

Before we continue, let us give an inductive method to compute
$\operatorname*{FV}u$ for a term $u$:

If $u=x$ for a variable $x$, then $\operatorname*{FV}u=\left\{  x\right\}  $.

If $u=\left(  v\right)  w$ for terms $v$ and $w$, then $\operatorname*{FV}
u=\left(  \operatorname*{FV}v\right)  \cup\left(  \operatorname*{FV}w\right)
$.

If $u=\lambda xv$ for some variable $x$ and some term $v$, then
$\operatorname*{FV}u=\left(  \operatorname*{FV}v\right)  \setminus\left\{
x\right\}  $.

\begin{quote}
\textbf{Lemma 1.C.} Let $u$ be a term in $L$, and let $y$ be a variable which
does not appear in $u$. Let $x$ be a variable. Then, $\operatorname*{FV}%
\left(  u\left\langle y/x\right\rangle \right)  =\operatorname*{map}%
\nolimits_{x,y}\left(  \operatorname*{FV}u\right)  $. Here,
$\operatorname*{map}\nolimits_{x,y}$ denotes the map $V\rightarrow V$ (where
$V$ is the set of variables) which maps $x$ to $y$ and maps $v$ to $v$ for
every variable $v\neq x$.
\end{quote}

\textit{Proof of Lemma 1.C.} We proceed by induction over $u$:

If $u$ is a variable, then everything is clear.

Consider the case when $u=\left(  v\right)  w$ for terms $v$ and $w$. In this
case, $u\left\langle y/x\right\rangle =\left(  v\left\langle y/x\right\rangle
\right)  \left(  w\left\langle y/x\right\rangle \right)  $, so that%
\begin{equation}
\operatorname*{FV}\left(  u\left\langle y/x\right\rangle \right)  =\left(
\operatorname*{FV}\left(  v\left\langle y/x\right\rangle \right)  \right)
\cup\left(  \operatorname*{FV}\left(  w\left\langle y/x\right\rangle \right)
\right)  . \label{1.c.pf.1}%
\end{equation}


By the induction assumption, $\operatorname*{FV}\left(  v\left\langle
y/x\right\rangle \right)  =\operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}v\right)  $ and $\operatorname*{FV}\left(  w\left\langle
y/x\right\rangle \right)  =\operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}w\right)  $. Thus (\ref{1.c.pf.1}) becomes%
\[
\operatorname*{FV}\left(  u\left\langle y/x\right\rangle \right)  =\left(
\operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}v\right)  \right)
\cup\left(  \operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}%
w\right)  \right)  =\operatorname*{map}\nolimits_{x,y}\left(  \left(
\operatorname*{FV}v\right)  \cup\left(  \operatorname*{FV}w\right)  \right)
.
\]
Since $\left(  \operatorname*{FV}v\right)  \cup\left(  \operatorname*{FV}%
w\right)  =\operatorname*{FV}u$ (due to $u=\left(  v\right)  w$), this becomes
$\operatorname*{FV}\left(  u\left\langle y/x\right\rangle \right)
=\operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}u\right)  $,
completing the induction (in the case $u=\left(  v\right)  w$).

It remains to complete the induction step in the case when $u=\lambda zv$ for
some variable $z$ and some term $v\in L$.

Consider this case. Clearly, $\operatorname*{FV}u=\left(  \operatorname*{FV}
v\right)  \setminus\left\{  z\right\}  $ in this case.

Two subcases are possible: the subcase $z=x$ and the subcase $z\neq x$.

Consider the subcase $z=x$. In this subcase, $u=\lambda zv=\lambda xv$, thus
$u\left\langle y/x\right\rangle =\lambda xv=u$, so that $\operatorname*{FV}%
\left(  u\left\langle y/x\right\rangle \right)  =\operatorname*{FV}u$. But we
want to prove that $\operatorname*{FV}\left(  u\left\langle y/x\right\rangle
\right)  =\operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}%
u\right)  $. So we only need to check that $\operatorname*{map}\nolimits_{x,y}%
\left(  \operatorname*{FV}u\right)  =\operatorname*{FV}u$. But this is clear
because $x\notin\operatorname*{FV}u$ (since $u=\lambda xv$, so that
$\operatorname*{FV}u=\left(  \operatorname*{FV}v\right)  \setminus\left\{
x\right\}  $) and because $\operatorname*{map}\nolimits_{x,y}$ leaves every
variable except of $x$ fixed.

Now consider the subcase $z\neq x$. In this subcase, $u=\lambda zv$ leads to
$u\left\langle y/x\right\rangle =\lambda z\left(  v\left\langle
y/x\right\rangle \right)  $, so that $\operatorname*{FV}\left(  u\left\langle
y/x\right\rangle \right)  =\left(  \operatorname*{FV}\left(  v\left\langle
y/x\right\rangle \right)  \right)  \setminus\left\{  z\right\}  $. By the
induction hypothesis, $\operatorname*{FV}\left(  v\left\langle
y/x\right\rangle \right)  =\operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}v\right)  $ (since $y$ does not appear in $v$, which is
because $y$ does not appear in $u$). Thus, $\operatorname*{FV}\left(
u\left\langle y/x\right\rangle \right)  =\underbrace{\left(
\operatorname*{FV}\left(  v\left\langle y/x\right\rangle \right)  \right)
}_{=\operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}v\right)
}\setminus\left\{  z\right\}  =\left(  \operatorname*{map}\nolimits_{x,y}%
\left(  \operatorname*{FV}v\right)  \right)  \setminus\left\{  z\right\}  $.
Let us now show that \newline$\left(  \operatorname*{map}\nolimits_{x,y}%
\left(  \operatorname*{FV}v\right)  \right)  \setminus\left\{  z\right\}
=\operatorname*{map}\nolimits_{x,y}\left(  \left(  \operatorname*{FV}v\right)
\setminus\left\{  z\right\}  \right)  $. In fact, $\operatorname*{FV}v$ does
not contain $y$ (because $y$ does not appear in $u$, and thus $y$ does not
appear in $v$ either), so that $\operatorname*{FV}v\subseteq V\diagdown
\left\{  y\right\}  $ (where $V$ denotes the set of all variables). Also,
$\left\{  z\right\}  \subseteq V\diagdown\left\{  y\right\}  $ (since $z\neq
y$ (which is because $y$ does not appear in $u=\lambda zv$, while $z$ does
appear in $\lambda zv$)). Now, $\operatorname*{map}\nolimits_{x,y}$ is
injective on $V\diagdown\left\{  y\right\}  $ (because $\left(  x,y\right)  $
is the only possible pair of distinct variables which have the same value
under $\operatorname*{map}\nolimits_{x,y}$, and therefore there is no such
pair inside $\left(  V\diagdown\left\{  y\right\}  \right)  \times\left(
V\diagdown\left\{  x\right\}  \right)  $). Thus, $\operatorname*{map}%
\nolimits_{x,y}\left(  \left(  \operatorname*{FV}v\right)  \setminus\left\{
z\right\}  \right)  =\left(  \operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}v\right)  \right)  \setminus\left(  \operatorname*{map}%
\nolimits_{x,y}\left\{  z\right\}  \right)  $ (since $\operatorname*{FV}v$ and
$\left\{  z\right\}  $ both are subsets of $V\diagdown\left\{  y\right\}  $).
Since $\operatorname*{map}\nolimits_{x,y}\left\{  z\right\}  =\left\{
z\right\}  $ (because $z\neq x$, and thus $\operatorname*{map}\nolimits_{x,y}%
z=z$), this becomes $\operatorname*{map}\nolimits_{x,y}\left(  \left(
\operatorname*{FV}v\right)  \setminus\left\{  z\right\}  \right)  =\left(
\operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}v\right)  \right)
\setminus\left\{  z\right\}  $. Now,%
\[
\operatorname*{FV}\left(  u\left\langle y/x\right\rangle \right)  =\left(
\operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}v\right)  \right)
\setminus\left\{  z\right\}  =\operatorname*{map}\nolimits_{x,y}\left(
\underbrace{\left(  \operatorname*{FV}v\right)  \setminus\left\{  z\right\}
}_{=\operatorname*{FV}u}\right)  =\operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right)  .
\]


Thus, $\operatorname*{FV}\left(  u\left\langle y / x\right\rangle \right)
=\operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV} u\right)  $ is
proven in every possible case and subcase. Lemma 1.C is proven.

\begin{quote}
\textbf{Lemma 1.D.} Let $x$ and $x^{\prime}$ be two variables, let $u$ and
$u^{\prime}$ be two terms in $L$, and let $y$ be a variable which does not
appear in any of the terms $u$ and $u^{\prime}$. Assume that
$\operatorname*{FV}\left(  u\left\langle y/x\right\rangle \right)
=\operatorname*{FV}\left(  u^{\prime}\left\langle y/x^{\prime}\right\rangle
\right)  $. Then, $\operatorname*{FV}\left(  \lambda xu\right)
=\operatorname*{FV}\left(  \lambda x^{\prime}u^{\prime}\right)  $.
\end{quote}

\textit{Proof of Lemma 1.D.} Lemma 1.C yields $\operatorname*{FV}\left(
u\left\langle y/x\right\rangle \right)  =\operatorname*{map}\nolimits_{x,y}%
\left(  \operatorname*{FV}u\right)  $ (where $\operatorname*{map}%
\nolimits_{x,y}$ is defined as in Lemma 1.C). But $y\notin\operatorname*{FV}u$
(because $y$ does not appear in $u$). Now we will prove that $\left(
\operatorname*{FV}u\right)  \setminus\left\{  x\right\}  =\left(
\operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}u\right)  \right)
\setminus\left\{  y\right\}  $.

In fact, let $z$ be an arbitrary element of $\left(  \operatorname*{FV}%
u\right)  \setminus\left\{  x\right\}  $. Then, $z\neq x$, but also
$z\in\operatorname*{FV}u$, so that $z\neq y$ (since $z\in\operatorname*{FV}u$
and $y\notin\operatorname*{FV}u$). Now, due to $z\neq x$, we have
$\operatorname*{map}\nolimits_{x,y}z=z$ (because $\operatorname*{map}%
\nolimits_{x,y}w=w$ for every variable $w\neq x$), and thus
$z=\operatorname*{map}\nolimits_{x,y}z\in\operatorname*{map}\nolimits_{x,y}%
\left(  \operatorname*{FV}u\right)  $ (since $z\in\operatorname*{FV}u$).
Together with $z\notin\left\{  y\right\}  $ (since $z\neq y$), this yields
$z\in\left(  \operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}%
u\right)  \right)  \setminus\left\{  y\right\}  $. Thus we have shown that
every $z\in\left(  \operatorname*{FV}u\right)  \setminus\left\{  x\right\}  $
satisfies $z\in\left(  \operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right)  \right)  \setminus\left\{  y\right\}  $. In other
words, $\left(  \operatorname*{FV}u\right)  \setminus\left\{  x\right\}
\subseteq\left(  \operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}%
u\right)  \right)  \setminus\left\{  y\right\}  $.

Now, let $z^{\prime}$ be an arbitrary element of $\left(  \operatorname*{map}%
\nolimits_{x,y}\left(  \operatorname*{FV}u\right)  \right)  \setminus\left\{
y\right\}  $. Then, $z^{\prime}\in\operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right)  $, so that there exists some $w^{\prime}%
\in\operatorname*{FV}u$ such that $z^{\prime}=\operatorname*{map}%
\nolimits_{x,y}w^{\prime}$. Consider this $w^{\prime}$. Clearly, $w^{\prime
}\neq x$ (since $w^{\prime}=x$ would yield $z^{\prime}=\operatorname*{map}%
\nolimits_{x,y}\underbrace{w^{\prime}}_{=x}=\operatorname*{map}\nolimits_{x,y}%
x=y$, contradicting $z^{\prime}\in\left(  \operatorname*{map}\nolimits_{x,y}%
\left(  \operatorname*{FV}u\right)  \right)  \setminus\left\{  y\right\}  $).
Thus, $\operatorname*{map}\nolimits_{x,y}w^{\prime}=w^{\prime}$ (since
$\operatorname*{map}\nolimits_{x,y}w=w$ for every variable $w\neq x$). Thus,
$z^{\prime}=\operatorname*{map}\nolimits_{x,y}w^{\prime}=w^{\prime}%
\in\operatorname*{FV}u$. Combined with $z^{\prime}\notin\left\{  x\right\}  $
(since $z^{\prime}=w^{\prime}\neq x$), this yields $z^{\prime}\in\left(
\operatorname*{FV}u\right)  \setminus\left\{  x\right\}  $. Thus we have shown
that every $z^{\prime}\in\left(  \operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right)  \right)  \setminus\left\{  y\right\}  $ satisfies
$z^{\prime}\in\left(  \operatorname*{FV}u\right)  \setminus\left\{  x\right\}
$. In other words, $\left(  \operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right)  \right)  \setminus\left\{  y\right\}
\subseteq\left(  \operatorname*{FV}u\right)  \setminus\left\{  x\right\}  $.
Combined with $\left(  \operatorname*{FV}u\right)  \setminus\left\{
x\right\}  \subseteq\left(  \operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right)  \right)  \setminus\left\{  y\right\}  $, this
yields $\left(  \operatorname*{FV}u\right)  \setminus\left\{  x\right\}
=\left(  \operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}u\right)
\right)  \setminus\left\{  y\right\}  $.

Thus,%
\[
\operatorname*{FV}\left(  \lambda xu\right)  =\left(  \operatorname*{FV}%
u\right)  \setminus\left\{  x\right\}  =\underbrace{\left(
\operatorname*{map}\nolimits_{x,y}\left(  \operatorname*{FV}u\right)  \right)
}_{=\operatorname*{FV}\left(  u\left\langle y/x\right\rangle \right)
}\setminus\left\{  y\right\}  =\left(  \operatorname*{FV}\left(  u\left\langle
y/x\right\rangle \right)  \right)  \diagdown\left\{  y\right\}  .
\]
Similarly, $\operatorname*{FV}\left(  \lambda x^{\prime}u^{\prime}\right)
=\left(  \operatorname*{FV}\left(  u^{\prime}\left\langle y/x^{\prime
}\right\rangle \right)  \right)  \setminus\left\{  y\right\}  $. Therefore,
$\operatorname*{FV}\left(  u\left\langle y/x\right\rangle \right)
=\operatorname*{FV}\left(  u^{\prime}\left\langle y/x^{\prime}\right\rangle
\right)  $ yields%
\[
\operatorname*{FV}\left(  \lambda xu\right)  =\underbrace{\left(
\operatorname*{FV}\left(  u\left\langle y/x\right\rangle \right)  \right)
}_{=\operatorname*{FV}\left(  u^{\prime}\left\langle y/x^{\prime}\right\rangle
\right)  }\setminus\left\{  y\right\}  =\left(  \operatorname*{FV}\left(
u^{\prime}\left\langle y/x^{\prime}\right\rangle \right)  \right)
\setminus\left\{  y\right\}  =\operatorname*{FV}\left(  \lambda x^{\prime
}u^{\prime}\right)  .
\]
Lemma 1.D is proven.

Lemma 1.D is used in the proof that $t$ and $t^{\prime}$ have the same free
variables if $t\equiv t^{\prime}$ (this fact is given without proof on page 12
of [1]).

\begin{quote}
\textbf{Lemma 1.E.} Let $u$ be a term in $L$, and $x$ be a variable. Then,
$u\left\langle x/x\right\rangle =u$.
\end{quote}

\textit{Proof of Lemma 1.E.} This is a trivial induction proof (induction on
$u$), so we omit it.

Lemma 1.E is used in the proof of Proposition 1.14 in [1] (in fact, it is the
reason why $u^{\prime}\left[  x^{\prime}/x^{\prime}\right]  =u^{\prime}$).

\begin{center}
\textbf{3. Equivalent definitions of }$\alpha$\textbf{-equivalence}
\end{center}

Not everybody defines the notion of $\alpha$-equivalence the same way as it is
done in [1]. In some other texts, $\alpha$-equivalence is defined in a
different way, which, instead of the substitution $\left\langle
t/x\right\rangle $ defined in [1], uses another notion of substitution:

\begin{quote}
\textbf{Definition.} For any term $t$ in $L$ and any variables $x_{1}$ and
$y_{1}$, we define the term $t\left\{  y_{1}/x_{1}\right\}  $ as the result of
the replacement of \textit{every} occurence of $x_{1}$ in $t$ by $y_{1}$
(where "every occurence" really means "every occurence", including bounded and
free occurences and occurences in abstractions). The definition is by
induction on $t$, as follows:

if $t=x_{1}$, then $t\left\{  y_{1}/x_{1}\right\}  =y_{1}$;

if $t$ is a variable $\neq x_{1}$, then $t\left\{  y_{1}/x_{1}\right\}  =t$;

if $t=\left(  u\right)  v$ for some terms $u$ and $v$, then $t\left\{
y_{1}/x_{1}\right\}  =\left(  u\left\{  y_{1}/x_{1}\right\}  \right)  \left(
v\left\{  y_{1}/x_{1}\right\}  \right)  $;

if $t=\lambda xu$ for some variable $x$ and some term $u$, then $t\left\{
y_{1}/x_{1}\right\}  =\lambda\left(  x\left\{  y_{1}/x_{1}\right\}  \right)
\left(  u\left\{  y_{1}/x_{1}\right\}  \right)  $.
\end{quote}

Intuitively, this $\left\{  y_{1}/x_{1}\right\}  $ substitution is a very
low-level kind of substitution, best understood as a blind find-replace
operation without regard to the meaning of the $x_{1}$'s which are being
replaced. Similarly one can define a substitution $\left\{  y_{1}%
/x_{1},...,y_{m}/x_{m}\right\}  $ for $m$ variables $x_{1},...,x_{m}$ and $m$
variables $y_{1},...,y_{m}$, but I will not use it.\footnote{Note that
$t\left\{  s/x\right\}  $ \textit{cannot} be defined if $s$ is just assumed to
be an arbitrary term (rather than a single variable).} Now here is the second
definition of $\alpha$-equivalence I am speaking about:

\begin{quote}
\textbf{Definition.} Let us define a relation $=^{\alpha}$ on terms in
$L$.\ \ \ \ \footnote{We denote this relation by $=^{\alpha}$, but later (in
Theorem 1.F) we will show that this relation is identical to the relation
$\equiv$ from [1].} Namely, we define $t=^{\alpha}t^{\prime}$ by induction on
the length of $t$ by the following clauses:

if $t$ is a variable, then $t=^{\alpha}t^{\prime}$ if and only if
$t=t^{\prime}$;

if $t=\left(  u\right)  v$ for some terms $u$ and $v$, then $t=^{\alpha
}t^{\prime}$ if and only if $t^{\prime}=\left(  u^{\prime}\right)  v^{\prime}$
for some terms $u^{\prime}$ and $v^{\prime}$ with $u=^{\alpha}u^{\prime}$ and
$v=^{\alpha}v^{\prime}$;

if $t=\lambda xu$ for some variable $x$ and some term $u$, then $t=^{\alpha
}t^{\prime}$ if and only if $t^{\prime}=\lambda x^{\prime}u^{\prime}$ for some
variable $x^{\prime}$ and some term $u^{\prime}$ such that all variables $y$
except a finite number satisfy $u\left\{  y/x\right\}  =^{\alpha}u^{\prime
}\left\{  y/x^{\prime}\right\}  $.
\end{quote}

We claim that the relation $=^{\alpha}$ defined by this definition is the
$\alpha$-equivalence defined in [1]; i. e., we claim that the following
theorem holds:

\begin{quote}
\textbf{Theorem 1.F.} The relations $\equiv$ and $=^{\alpha}$ are identical.
\end{quote}

We prove this using a lemma:

\begin{quote}
\textbf{Lemma 1.G.} Let $t$ be a term in $L$. Let $x$ and $y$ be two variables
such that $y$ does not occur in $t$. Then, $t\left\langle y/x\right\rangle
\equiv t\left\{  y/x\right\}  $.
\end{quote}

\textit{Proof of Lemma 1.G.} We prove this by induction over $t$:

If $t$ is a variable, then everything is clear because the definitions of
$t\left\langle y / x\right\rangle $ and $t\left\{  y / x\right\}  $ for $t$
being a variable are the same.

If $t=\left(  u\right)  v$ for some terms $u$ and $v$, then everything is
clear again because the definition of $t\left\langle y/x\right\rangle $ says%
\begin{align*}
t\left\langle y/x\right\rangle  &  =\underbrace{\left(  u\left\langle
y/x\right\rangle \right)  }_{\substack{\equiv u\left\{  y/x\right\}
\\\text{(by the induction}\\\text{assumption)}}}\underbrace{\left(
v\left\langle y/x\right\rangle \right)  }_{\substack{\equiv v\left\{
y/x\right\}  \\\text{(by the induction}\\\text{assumption)}}%
}\ \ \ \ \ \ \ \ \ \ \left(  \text{since }t=\left(  u\right)  v\right) \\
&  \equiv\left(  u\left\{  y/x\right\}  \right)  \left(  v\left\{
y/x\right\}  \right)  =t\left\{  y/x\right\} \\
&  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since the definition of }t\left\{  y/x\right\}  \text{ says}\\
\text{ }t\left\{  y/x\right\}  =\left(  u\left\{  y/x\right\}  \right)
\left(  v\left\{  y/x\right\}  \right)  \text{ (since }t=\left(  u\right)
v\text{)}%
\end{array}
\right)  .
\end{align*}


So it only remains to consider the case when $t=\lambda zu$ for some variable
$z$ and some term $u$. By the induction assumption, $u\left\langle y /
x\right\rangle \equiv u\left\{  y / x\right\}  $.

Two subcases are possible: the subcase $z\neq x$ and the subcase $z=x$.

First consider the subcase $z\neq x$. In this subcase, $t\left\langle
y/x\right\rangle =\lambda z\left(  u\left\langle y/x\right\rangle \right)
\equiv\lambda z\left(  u\left\{  y/x\right\}  \right)  $ (by Corollary 1.7,
since $u\left\langle y/x\right\rangle \equiv u\left\{  y/x\right\}  $) and
\newline$t\left\{  y/x\right\}  =\lambda\left(  z\left\{  y/x\right\}
\right)  \left(  u\left\{  y/x\right\}  \right)  =\lambda z\left(  u\left\{
y/x\right\}  \right)  $ (since $z\neq x$ and thus $z\left\{  y/x\right\}
=z$), so that $t\left\langle y/x\right\rangle \equiv\lambda z\left(  u\left\{
y/x\right\}  \right)  =t\left\{  y/x\right\}  $.

Now consider the subcase $z=x$. In this subcase, $t=\lambda zu=\lambda xu$, so
that $t\left\langle y/x\right\rangle =\lambda xu$, but on the other hand
$t=\lambda xu$ gives us $t\left\{  y/x\right\}  =\lambda\underbrace{\left(
x\left\{  y/x\right\}  \right)  }_{=y}\left(  u\left\{  y/x\right\}  \right)
=\lambda y\left(  u\left\{  y/x\right\}  \right)  \equiv\lambda y\left(
u\left\langle y/x\right\rangle \right)  $ (by Corollary 1.7, since $u\left\{
y/x\right\}  \equiv u\left\langle y/x\right\rangle $). Since $y$ does not
occur in $u$ (because $y$ does not occur in $t$), we have $\lambda
xu\equiv\lambda y\left(  u\left\langle y/x\right\rangle \right)  $ by Lemma
1.9, so that $t\left\langle y/x\right\rangle =\lambda xu\equiv\lambda y\left(
u\left\langle y/x\right\rangle \right)  \equiv t\left\{  y/x\right\}  $.

Hence, $t\left\langle y / x\right\rangle \equiv t\left\{  y / x\right\}  $ is
proved in every case and every subcase. Lemma 1.G is thus proven.

\begin{quote}
\textbf{Lemma 1.H.} Let $t$ and $t^{\prime}$ be two terms in $L$ such that
$t=^{\alpha}t^{\prime}$. Then, $t\equiv t^{\prime}$.
\end{quote}

\textit{Proof of Lemma 1.H.} We proceed by induction over the length of $t$.

There are three cases to consider: the case when $t$ is a variable; the case
when $t=\left(  u\right)  v$ for some terms $u$ and $v$; the case when
$t=\lambda xu$ for some variable $x$ and some term $u$.

In the case when $t$ is a variable, the relation $t=^{\alpha}t^{\prime}$
yields that $t^{\prime}$ is the same variable as $t$. Thus, $t\equiv
t^{\prime}$.

In the case when $t=\left(  u\right)  v$ for some terms $u$ and $v$, the
relation $t=^{\alpha}t^{\prime}$ yields that $t^{\prime}=\left(  u^{\prime
}\right)  v^{\prime}$ for some terms $u^{\prime}$ and $v^{\prime}$ with
$u=^{\alpha}u^{\prime}$ and $v=^{\alpha}v^{\prime}$. By the induction
assumption, $u=^{\alpha}u^{\prime}$ yields $u\equiv u^{\prime}$, and
$v=^{\alpha}v^{\prime}$ yields $v\equiv v^{\prime}$. Thus, $t^{\prime}=\left(
u^{\prime}\right)  v^{\prime}$ for some terms $u^{\prime}$ and $v^{\prime}$
with $u\equiv u^{\prime}$ and $v\equiv v^{\prime}$. This means that $t\equiv
t^{\prime}$.

Now let us consider the final remaining case: the case when $t=\lambda xu$ for
some variable $x$ and some term $u$. In this case, $t=^{\alpha}t^{\prime}$
means that $t^{\prime}=\lambda x^{\prime}u^{\prime}$ for some variable
$x^{\prime}$ and some term $u^{\prime}$ such that all variables $y$ except a
finite number satisfy $u\left\{  y/x\right\}  =^{\alpha}u^{\prime}\left\{
y/x^{\prime}\right\}  $. By the induction assumption, this yields that all
variables $y$ except a finite number satisfy $u\left\{  y/x\right\}  \equiv
u^{\prime}\left\{  y/x^{\prime}\right\}  $ (because the terms $u\left\{
y/x\right\}  $ and $u^{\prime}\left\{  y/x^{\prime}\right\}  $ are as long as
$u$ and $u^{\prime}$, respectively, and therefore shorter than $t$ and
$t^{\prime}$, respectively). Thus, all variables $y$ except a finite number
and except those which occur in $u$ or $u^{\prime}$ satisfy $u\left\langle
y/x\right\rangle \equiv u^{\prime}\left\langle y/x^{\prime}\right\rangle $
(because Lemma 1.G yields that these variables satisfy $u\left\langle
y/x\right\rangle \equiv u\left\{  y/x\right\}  $ and $u^{\prime}\left\langle
y/x^{\prime}\right\rangle \equiv u^{\prime}\left\{  y/x^{\prime}\right\}  $,
so that they satisfy $u\left\langle y/x\right\rangle \equiv u\left\{
y/x\right\}  \equiv u^{\prime}\left\{  y/x^{\prime}\right\}  \equiv u^{\prime
}\left\langle y/x^{\prime}\right\rangle $). But "all variables $y$ except a
finite number and except those which occur in $u$ or $u^{\prime}$ " can be
rewritten as "all variables $y$ except a finite number", because only finitely
many variables occur in $u$ or $u^{\prime}$. Thus, all variables $y$ except a
finite number satisfy $u\left\langle y/x\right\rangle \equiv u^{\prime
}\left\langle y/x^{\prime}\right\rangle $. Hence, $t\equiv t^{\prime}$ (by the
definition of $\equiv$).

Thus we have proven that $t\equiv t^{\prime}$ in all possible cases. The proof
of Lemma 1.H is complete.

\begin{quote}
\textbf{Lemma 1.I.} Let $t$ and $t^{\prime}$ be two terms in $L$ such that
$t\equiv t^{\prime}$. Then, $t=^{\alpha}t^{\prime}$.
\end{quote}

\textit{Proof of Lemma 1.I.} We proceed by induction over the length of $t$.

There are three cases to consider: the case when $t$ is a variable; the case
when $t=\left(  u\right)  v$ for some terms $u$ and $v$; the case when
$t=\lambda xu$ for some variable $x$ and some term $u$.

In the case when $t$ is a variable, the relation $t\equiv t^{\prime}$ yields
that $t^{\prime}$ is the same variable as $t$. Thus, $t=^{\alpha}t^{\prime}$.

In the case when $t=\left(  u\right)  v$ for some terms $u$ and $v$, the
relation $t\equiv t^{\prime}$ yields that $t^{\prime}=\left(  u^{\prime
}\right)  v^{\prime}$ for some terms $u^{\prime}$ and $v^{\prime}$ with
$u\equiv u^{\prime}$ and $v\equiv v^{\prime}$. By the induction assumption,
$u\equiv u^{\prime}$ yields $u=^{\alpha}u^{\prime}$, and $v\equiv v^{\prime}$
yields $v=^{\alpha}v^{\prime}$. Thus, $t^{\prime}=\left(  u^{\prime}\right)
v^{\prime}$ for some terms $u^{\prime}$ and $v^{\prime}$ with $u=^{\alpha
}u^{\prime}$ and $v=^{\alpha}v^{\prime}$. This means that $t=^{\alpha
}t^{\prime}$.

Now let us consider the final remaining case: the case when $t=\lambda xu$ for
some variable $x$ and some term $u$. In this case, $t\equiv t^{\prime}$ means
that $t^{\prime}=\lambda x^{\prime}u^{\prime}$ for some variable $x^{\prime}$
and some term $u^{\prime}$ such that all variables $y$ except a finite number
satisfy $u\left\langle y/x\right\rangle \equiv u^{\prime}\left\langle
y/x^{\prime}\right\rangle $. Thus, all variables $y$ except a finite number
and except those which occur in $u$ or $u^{\prime}$ satisfy $u\left\{
y/x\right\}  \equiv u^{\prime}\left\{  y/x^{\prime}\right\}  $ (because Lemma
1.G yields that these variables satisfy $u\left\langle y/x\right\rangle \equiv
u\left\{  y/x\right\}  $ and $u^{\prime}\left\langle y/x^{\prime}\right\rangle
\equiv u^{\prime}\left\{  y/x^{\prime}\right\}  $, so that they satisfy
$u\left\{  y/x\right\}  \equiv u\left\langle y/x\right\rangle \equiv
u^{\prime}\left\langle y/x^{\prime}\right\rangle \equiv u^{\prime}\left\{
y/x^{\prime}\right\}  $). But "all variables $y$ except a finite number and
except those which occur in $u$ or $u^{\prime}$ " can be rewritten as "all
variables $y$ except a finite number", because only finitely many variables
occur in $u$ or $u^{\prime}$. Thus, all variables $y$ except a finite number
satisfy $u\left\{  y/x\right\}  \equiv u^{\prime}\left\{  y/x^{\prime
}\right\}  $. By the induction assumption, this yields that all variables $y$
except a finite number satisfy $u\left\{  y/x\right\}  =^{\alpha}u^{\prime
}\left\{  y/x^{\prime}\right\}  $ (because the terms $u\left\{  y/x\right\}  $
and $u^{\prime}\left\{  y/x^{\prime}\right\}  $ are as long as $u$ and
$u^{\prime}$, respectively, and therefore shorter than $t$ and $t^{\prime}$,
respectively). Hence, $t=^{\alpha}t^{\prime}$ (by the definition of
$=^{\alpha}$).

Thus we have proven that $t=^{\alpha}t^{\prime}$ in all possible cases. The
proof of Lemma 1.I is complete.

\textit{Proof of Theorem 1.F.} Theorem 1.F follows directly from Lemma 1.H and
Lemma 1.I.

\begin{center}
\textbf{4. Some rules for substitution}
\end{center}

Now we are going to prove the following properties of the substitution defined
in Chapter 1 \S 2 of [1]:

\begin{quote}
\textbf{Lemma 1.J.} Any variable $x$ and any $s\in\Lambda$ satisfy $x\left[
s/x\right]  =s$.

\textbf{Lemma 1.K.} Any two distinct variables $x$ and $y$ and any
$s\in\Lambda$ satisfy $y\left[  s/x\right]  =y$.

\textbf{Lemma 1.L.} If $t_{1}\in\Lambda$, $t_{2}\in\Lambda$ and $s\in\Lambda$
are three equivalence classes and $x$ is a variable, then $\left(  t_{1}%
t_{2}\right)  \left[  s/x\right]  =\left(  t_{1}\left[  s/x\right]  \right)
\left(  t_{2}\left[  s/x\right]  \right)  $.

\textbf{Lemma 1.M.} If $x$ and $y$ are two distinct variables, and
$s\in\Lambda$ and $r\in\Lambda$ are two equivalence classes, then $\left(
\lambda yr\right)  \left[  s/x\right]  =\lambda y^{\prime}\left(  r\left[
y^{\prime}/y\right]  \left[  s/x\right]  \right)  $, where $y^{\prime}$ is any
variable which is not free in $x$, $s$ or $r$.

\textbf{Lemma 1.N.} If $x$ and $y$ are two distinct variables, and
$s\in\Lambda$ and $r\in\Lambda$ are two equivalence classes such that $y$ is
not a free variable in $s$, then $\left(  \lambda yr\right)  \left[
s/x\right]  =\lambda y\left(  r\left[  s/x\right]  \right)  $.

\textbf{Lemma 1.O.} If $x$ is a variable, and $s\in\Lambda$ and $r\in\Lambda$
are two equivalence classes, then $\left(  \lambda xr\right)  \left[
s/x\right]  =\lambda xr$.
\end{quote}

\textit{Proof of Lemma 1.J.} Let $\underline{s}$ be a representative of the
equivalence class $s$. Clearly, $x$ is a representative of $x$, and no bound
variable of $x$ is free in $\underline{s}$ (since $x$ has no bound variable).
Therefore, by the definition of substitution, $x\left[  s/x\right]  $ is the
equivalence class of $x\left\langle \underline{s}/x\right\rangle $. Since
$x\left\langle \underline{s}/x\right\rangle =\underline{s}$, this means that
$x\left[  s/x\right]  $ is the equivalence class of $\underline{s}$. In other
words, $x\left[  s/x\right]  =s$ (because $s$ is the equivalence class of
$\underline{s}$). This proves Lemma 1.J.

\textit{Proof of Lemma 1.K.} Let $\underline{s}$ be a representative of the
equivalence class $s$. Clearly, $y$ is a representative of $y$, and no bound
variable of $y$ is free in $\underline{s}$ (since $y$ has no bound variable).
Therefore, by the definition of substitution, $y\left[  s/x\right]  $ is the
equivalence class of $y\left\langle \underline{s}/x\right\rangle $. Since
$y\left\langle \underline{s}/x\right\rangle =y$, this means that $y\left[
s/x\right]  $ is the equivalence class of $y$. In other words, $y\left[
s/x\right]  =y$. This proves Lemma 1.K.

\textit{Proof of Lemma 1.L.} Let $\underline{s}$ be a representative of the
equivalence class $s$.

Let $\underline{t}_{1}$ be a representative of the equivalence class $t_{1}$
such that no bound variable of $\underline{t}_{1}$ is free in $s$%
.\ \ \ \ \footnote{Such a representative $\underline{t}_{1}$ exists due to
Lemma 1.10.} Let $\underline{t}_{2}$ be a representative of the equivalence
class $t_{2}$ such that no bound variable of $\underline{t}_{2}$ is free in
$s$.\ \ \ \ \footnote{Such a representative $\underline{t}_{2}$ exists due to
Lemma 1.10.} Then, clearly, no bound variable of $\underline{t}_{1}%
\underline{t}_{2}$ is free in $s$ (since $\operatorname*{BV}\left(
\underline{t}_{1}\underline{t}_{2}\right)  =\left(  \operatorname*{BV}%
\underline{t}_{1}\right)  \cup\left(  \operatorname*{BV}\underline{t}%
_{2}\right)  $), and we know that $\underline{t}_{1}\underline{t}_{2}$ is a
representative of the equivalence class $t_{1}t_{2}$. Thus, the definition of
$\left(  t_{1}t_{2}\right)  \left[  s/x\right]  $ says that $\left(
t_{1}t_{2}\right)  \left[  s/x\right]  $ is the equivalence class of $\left(
\underline{t}_{1}\underline{t}_{2}\right)  \left\langle \underline{s}%
/x\right\rangle $. On the other hand, the definition of $t_{1}\left[
s/x\right]  $ says that $t_{1}\left[  s/x\right]  $ is the equivalence class
of $\underline{t}_{1}\left\langle \underline{s}/x\right\rangle $ (since no
bound variable of $\underline{t}_{1}$ is free in $s$), and the definition of
$t_{2}\left[  s/x\right]  $ says that $t_{2}\left[  s/x\right]  $ is the
equivalence class of $\underline{t}_{2}\left\langle \underline{s}%
/x\right\rangle $ (since no bound variable of $\underline{t}_{2}$ is free in
$s$). Since we know that $\left(  \underline{t}_{1}\underline{t}_{2}\right)
\left\langle \underline{s}/x\right\rangle =\left(  \underline{t}%
_{1}\left\langle \underline{s}/x\right\rangle \right)  \left(  \underline{t}%
_{2}\left\langle \underline{s}/x\right\rangle \right)  $, we therefore
conclude that
\begin{align*}
\left(  t_{1}t_{2}\right)  \left[  s/x\right]   &  =\left(  \text{equivalence
class of }\underbrace{\left(  \underline{t}_{1}\underline{t}_{2}\right)
\left\langle \underline{s}/x\right\rangle }_{=\left(  \underline{t}%
_{1}\left\langle \underline{s}/x\right\rangle \right)  \left(  \underline{t}%
_{2}\left\langle \underline{s}/x\right\rangle \right)  }\right) \\
&  =\left(  \text{equivalence class of }\left(  \underline{t}_{1}\left\langle
\underline{s}/x\right\rangle \right)  \left(  \underline{t}_{2}\left\langle
\underline{s}/x\right\rangle \right)  \right) \\
&  =\underbrace{\left(  \text{equivalence class of }\underline{t}%
_{1}\left\langle \underline{s}/x\right\rangle \right)  }_{=t_{1}\left[
s/x\right]  }\underbrace{\left(  \text{equivalence class of }\underline{t}%
_{2}\left\langle \underline{s}/x\right\rangle \right)  }_{=t_{2}\left[
s/x\right]  }\\
&  =\left(  t_{1}\left[  s/x\right]  \right)  \left(  t_{2}\left[  s/x\right]
\right)  .
\end{align*}
Lemma 1.L is proven.

\textit{Proof of Lemma 1.N.} Let $\underline{s}$ be a representative of the
equivalence class $s$. Let $\underline{r}$ be a representative of the
equivalence class $r$ such that no bound variable of $\underline{r}$ is free
in $s$. \ \ \ \ \footnote{Such a representative $\underline{r}$ exists due to
Lemma 1.10.} Then, $\lambda y\underline{r}$ is a representative of $\lambda
yr$, and no bound variable of $\lambda y\underline{r}$ is free in $s$ (because
$\operatorname*{BV}\left(  \lambda y\underline{r}\right)  =\left\{  y\right\}
\cup\left(  \operatorname*{BV}\underline{r}\right)  $, but neither $y$ nor any
bound variable of $\underline{r}$ is free in $s$). Therefore, by the
definition of $\left(  \lambda yr\right)  \left[  s/x\right]  $, we know that
$\left(  \lambda yr\right)  \left[  s/x\right]  $ is the equivalence class of
$\left(  \lambda y\underline{r}\right)  \left\langle \underline{s}%
/x\right\rangle $. Since $\left(  \lambda y\underline{r}\right)  \left\langle
\underline{s}/x\right\rangle =\lambda y\left(  \underline{r}\left\langle
\underline{s}/x\right\rangle \right)  $ (because $x\neq y$), this rewrites as
follows: $\left(  \lambda yr\right)  \left[  s/x\right]  $ is the equivalence
class of $\lambda y\left(  \underline{r}\left\langle \underline{s}%
/x\right\rangle \right)  $. But since $r\left[  s/x\right]  $ is the
equivalence class of $\underline{r}\left\langle \underline{s}/x\right\rangle $
(by the definition of $r\left[  s/x\right]  $, since no bound variable of
$\underline{r}$ is free in $s$), the class $\lambda y\left(  r\left[
s/x\right]  \right)  $ is the equivalence class of $\lambda y\left(
\underline{r}\left\langle \underline{s}/x\right\rangle \right)  $. So now we
know that both $\left(  \lambda yr\right)  \left[  s/x\right]  $ and $\lambda
y\left(  r\left[  s/x\right]  \right)  $ are the equivalence class of $\lambda
y\left(  \underline{r}\left\langle \underline{s}/x\right\rangle \right)  $.
Thus, $\left(  \lambda yr\right)  \left[  s/x\right]  =\lambda y\left(
r\left[  s/x\right]  \right)  $. This proves Lemma 1.N.

\textit{Proof of Lemma 1.M.} Let $y^{\prime}$ be any variable which is not
free in $x$, $s$ or $r$. Then, $y^{\prime}$ is not free in $\lambda yr$
either. Proposition 1.14 (applied to $\lambda yr$, $y$, $r$ and $y^{\prime}$
instead of $t$, $x$, $u$ and $x^{\prime}$) yields $\lambda yr=\lambda
y^{\prime}\left(  r\left[  y^{\prime}/y\right]  \right)  $. Lemma 1.N (applied
to $y^{\prime}$ and $r\left[  y^{\prime}/y\right]  $ instead of $y$ and $r$)
yields $\left(  \lambda y^{\prime}\left(  r\left[  y^{\prime}/y\right]
\right)  \right)  \left[  s/x\right]  =\lambda y^{\prime}\left(  r\left[
y^{\prime}/y\right]  \left[  s/x\right]  \right)  $ (here we use $y^{\prime
}\neq x$, which is because $y^{\prime}$ is not free in $x$). Thus,
$\underbrace{\left(  \lambda yr\right)  }_{=\lambda y^{\prime}\left(  r\left[
y^{\prime}/y\right]  \right)  }\left[  s/x\right]  =\left(  \lambda y^{\prime
}\left(  r\left[  y^{\prime}/y\right]  \right)  \right)  \left[  s/x\right]
=\lambda y^{\prime}\left(  r\left[  y^{\prime}/y\right]  \left[  s/x\right]
\right)  $. This proves Lemma 1.M.

\textit{Proof of Lemma 1.O.} Let $\underline{s}$ be a representative of the
equivalence class $s$. Let $\underline{p}$ be a representative of the
equivalence class $\lambda xr$ such that no bound variable of $\underline{p}$
is free in $s$.\ \ \ \ \footnote{Such a representative $\underline{p}$ exists
due to Lemma 1.10.} Then, the definition of $\left(  \lambda xr\right)
\left[  s/x\right]  $ yields that $\left(  \lambda xr\right)  \left[
s/x\right]  $ is the equivalence class of $\underline{p}\left\langle
\underline{s}/x\right\rangle $. But $x$ is not a free variable in
$\underline{p}$ (because $x$ is not a free variable in $\lambda xr$), and
therefore $\underline{p}\left\langle \underline{s}/x\right\rangle
=\underline{p}$ (by Lemma 1.1 in [1]). Hence, $\left(  \lambda xr\right)
\left[  s/x\right]  $ is the equivalence class of $\underline{p}$ (since
$\left(  \lambda xr\right)  \left[  s/x\right]  $ is the equivalence class of
$\underline{p}\left\langle \underline{s}/x\right\rangle $). In other words,
$\left(  \lambda xr\right)  \left[  s/x\right]  =\lambda xr$ (since we know
that the equivalence class of $\underline{p}$ is $\lambda xr$). This proves
Lemma 1.O.

\begin{center}
\textbf{Appendix: Proof of Corollary 1.3 of [1], Chapter 1, \S 1}
\end{center}

Below is a writeup of the proof of Corollary 1.3 of [1]. I made this writeup
at a time when the proof given in [1] was wrong; now the proof in [1] was
corrected, so there is no use in this writeup anymore except for the little
bit of additional detail it gives.

\textit{Proof of Corollary 1.3:} WLOG assume that $x_{1},...,x_{u}$ are those
variables among the set $\left\{  x_{1},...,x_{m}\right\}  $ which don't occur
in $t$. Then, $x_{1},...,x_{u}$ are not free in $t$, so that Lemma 1.1 yields
$t\left\langle y_{1}/x_{1},...,y_{m}/x_{m}\right\rangle =t\left\langle
y_{u+1}/x_{u+1},...,y_{m}/x_{m}\right\rangle $. Now, the sets $\left\{
x_{u+1},...,x_{m}\right\}  $ and $\left\{  y_{1},...,y_{m}\right\}  $ have no
common elements (because every of the variables $x_{u+1},...,x_{m}$ occurs in
$t$, while none of the variables $y_{1},...,y_{m}$ does). The hypothesis of
Lemma 1.2 is satisfied (with $k=0$), because none of the $y_{i}$ is bound in
$t$. Thus,%
\[
t\left\langle y_{u+1}/x_{u+1},...,y_{m}/x_{m}\right\rangle \left\langle
t_{1}/y_{1},...,t_{m}/y_{m}\right\rangle =t\left\langle t_{u+1}/x_{u+1}%
,...,t_{m}/x_{m},t_{1}/y_{1},...,t_{m}/y_{m}\right\rangle .
\]
But $y_{1},...,y_{m}$ are not free in $t$, and thus Lemma 1.1 yields%
\[
t\left\langle t_{u+1}/x_{u+1},...,t_{m}/x_{m},t_{1}/y_{1},...,t_{m}%
/y_{m}\right\rangle =t\left\langle t_{u+1}/x_{u+1},...,t_{m}/x_{m}%
\right\rangle .
\]
Finally, $x_{1},...,x_{u}$ are not free in $t$, so that Lemma 1.1 yields
(again)%
\[
t\left\langle t_{u+1}/x_{u+1},...,t_{m}/x_{m}\right\rangle =t\left\langle
t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle .
\]


Altogether,%
\begin{align*}
&  \underbrace{t\left\langle y_{1}/x_{1},...,y_{m}/x_{m}\right\rangle
}_{=t\left\langle y_{u+1}/x_{u+1},...,y_{m}/x_{m}\right\rangle }\left\langle
t_{1}/y_{1},...,t_{m}/y_{m}\right\rangle \\
&  =t\left\langle y_{u+1}/x_{u+1},...,y_{m}/x_{m}\right\rangle \left\langle
t_{1}/y_{1},...,t_{m}/y_{m}\right\rangle =t\left\langle t_{u+1}/x_{u+1}%
,...,t_{m}/x_{m},t_{1}/y_{1},...,t_{m}/y_{m}\right\rangle \\
&  =t\left\langle t_{u+1}/x_{u+1},...,t_{m}/x_{m}\right\rangle =t\left\langle
t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle ,
\end{align*}
qed.

\begin{center}
\textbf{References}
\end{center}

[1] Jean-Louis Krivine, \textit{Lambda-calculus, types and models}, 22 January
2009, updated version of 5 June 2011.\newline%
\texttt{http://www.pps.jussieu.fr/\symbol{126}krivine/articles/Lambda.pdf}


\end{document}