\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{} %TCIDATA{} %TCIDATA{BibliographyScheme=Manual} %BeginMSIPreambleData \providecommand{\U}{\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  (lemmata that are used in  without mention, due to their intuitive obviousness); \textbf{2)} show that the definition of $\alpha$-equivalence given in  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 . In particular, the sign $\equiv$ will stand for the $\alpha$-equivalence defined in . 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 } \end{center} Here come several facts silently used in some proofs in \S 1.2 of . 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 . 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 . (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 . (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 ). \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  (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 . 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 , 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 .} 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 ; 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 : \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 ). 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 , Chapter 1, \S 1} \end{center} Below is a writeup of the proof of Corollary 1.3 of . I made this writeup at a time when the proof given in  was wrong; now the proof in  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}  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}