diff --git a/index.md b/index.md
index 1c3a8d29..08011abd 100644
--- a/index.md
+++ b/index.md
@@ -34,7 +34,7 @@ Comments on all matters---organisation, material we should add, material we shou
 (This part is not yet ready for review.)
 
   - [Lambda: Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/plta/Lambda.md %})
-  - [PandP: Progress and Preservation]({{ site.baseurl }}{% link out/plta/PandP.md %})
+  - [Properties: Progress and Preservation]({{ site.baseurl }}{% link out/plta/Properties.md %})
   - [DeBruijn: Inherently typed De Bruijn representation]({{ site.baseurl }}{% link out/plta/DeBruijn.md %})
   - [Extensions: Extensions to simply-typed lambda calculus]({{ site.baseurl }}{% link out/plta/Extensions.md %})
   - [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/plta/Inference.md %})
diff --git a/src/plta/Lambda.lagda b/src/plta/Lambda.lagda
index d2cca691..42b3151a 100644
--- a/src/plta/Lambda.lagda
+++ b/src/plta/Lambda.lagda
@@ -28,7 +28,7 @@ recursive function definitions.
 
 This chapter formalises the simply-typed lambda calculus, giving its
 syntax, small-step semantics, and typing rules.  The next chapter
-[PandP]({{ site.baseurl }}{% link out/plta/PandP.md %})
+[Properties]({{ site.baseurl }}{% link out/plta/Properties.md %})
 proves its main properties, including
 progress and preservation.  Following chapters will look at a number
 of variants of lambda calculus.
@@ -243,7 +243,7 @@ that are bound may become free.  Consider the following terms.
 
 We say that a term with no free variables is _closed_; otherwise it is
 _open_.  Of the three terms above, the first is closed and the other
-two are open.
+two are open.  We will focus on reduction of closed terms.
 
 Different occurrences of a variable may be bound and free.
 In the term
@@ -283,13 +283,6 @@ names, `x` and `x′`.
 
 ## Values
 
-<!--
-We only consider reduction of _closed_ terms,
-those that contain no free variables.  We consider
-a precise definition of free variables in Chapter
-[PandP]({{ site.baseurl }}{% link out/plta/PandP.md %}).
--->
-
 A _value_ is a term that corresponds to an answer.
 Thus, `` `suc `suc `suc `suc `zero` `` is a value,
 while `` plus · two · two `` is not.
diff --git a/src/plta/PandP.lagda b/src/plta/Properties.lagda
similarity index 99%
rename from src/plta/PandP.lagda
rename to src/plta/Properties.lagda
index 228d285d..84bdfa81 100644
--- a/src/plta/PandP.lagda
+++ b/src/plta/Properties.lagda
@@ -1,11 +1,11 @@
 ---
-title     : "PandP: Progress and Preservation"
+title     : "Properties: Progress and Preservation"
 layout    : page
-permalink : /PandP/
+permalink : /Properties/
 ---
 
 \begin{code}
-module plta.PandP where
+module plta.Properties where
 \end{code}
 
 [Parts of this chapter take their text from chapter _StlcProp_
diff --git a/src/plta/Statistics.lagda b/src/plta/Statistics.lagda
index 245f9c63..734e1e61 100644
--- a/src/plta/Statistics.lagda
+++ b/src/plta/Statistics.lagda
@@ -26,7 +26,7 @@ Total number of lines and number of lines of Agda code in each chapter
     Decidable                    566     170
 
     Lambda                      1114     345
-    LambdaProp                   827     450
+    Properties                   827     450
     DeBruijn                     477     351
     Extensions                   603     524
     Inference                    428     350