Fix 77--82.

1 files changed, 5 insertions, 2 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 63cd7a7..b534040 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -4,13 +4,15 @@
 \section{System T}%
 \label{sec:systemt}
 
-System~T is a simply-typed lambda calculus. The types are naturals
+System~T is a simply-typed lambda calculus. Its types are naturals
 \nat{} and functions \(A \to B\). On top of the function abstraction and
 application operators, we have \zero{} and \suc{} for zero and
 successor, as well as \primreckw{}, the primitive
 recursor. \Cref{fig:syst-typing} shows the typing judgements, where
 \(\judgement{\Gamma}[T]{t}{A}\) means that \(t\) is System~T term of type
-\(A\) in context \(\Gamma\), and \cref{fig:syst-eq} the equational theory.
+\(A\) in context \(\Gamma\). \Cref{fig:syst-eq} gives the equational
+theory. We have beta- and eta-equality of functions and beta-reduction
+of natural numbers.
 
 \begin{figure}
   \[
@@ -54,6 +56,7 @@ recursor. \Cref{fig:syst-typing} shows the typing judgements, where
 \begin{figure}
   \begin{align*}
     (\lambda x. t)~u &= \sub{t}{x/u} \\
+    \lambda x. t~x &= t \qquad (x \notin t)\\
     \primrec{\zero}{u}{(x.v)} &= u \\
     \primrec{(\suc~t)}{u}{(x.v)} &= \sub{v}{x/\primrec{t}{u}{(x.v)}}
   \end{align*}