diff --git a/beta.md b/beta.md
index ffc85294..877f840a 100644
--- a/beta.md
+++ b/beta.md
@@ -34,7 +34,7 @@ Pull requests are encouraged.
 
   - [Lambda]({{ site.baseurl }}/Lambda/): Introduction to Lambda Calculus
   - [Properties]({{ site.baseurl }}/Properties/): Progress and Preservation
-  - [DeBruijn]({{ site.baseurl }}/DeBruijn/): Inherently typed de Bruijn representation
+  - [DeBruijn]({{ site.baseurl }}/DeBruijn/): Intrinsically-typed de Bruijn representation
   - [More]({{ site.baseurl }}/More/): Additional constructs of simply-typed lambda calculus
   - [Bisimulation]({{ site.baseurl }}/Bisimulation/): Relating reductions systems
   - [Inference]({{ site.baseurl }}/Inference/): Bidirectional type inference
diff --git a/index.md b/index.md
index 758c649d..9f0f35f9 100644
--- a/index.md
+++ b/index.md
@@ -33,7 +33,7 @@ Pull requests are encouraged.
 
   - [Lambda]({{ site.baseurl }}/Lambda/): Introduction to Lambda Calculus
   - [Properties]({{ site.baseurl }}/Properties/): Progress and Preservation
-  - [DeBruijn]({{ site.baseurl }}/DeBruijn/): Inherently typed de Bruijn representation
+  - [DeBruijn]({{ site.baseurl }}/DeBruijn/): Intrinsically-typed de Bruijn representation
   - [More]({{ site.baseurl }}/More/): Additional constructs of simply-typed lambda calculus
   - [Bisimulation]({{ site.baseurl }}/Bisimulation/): Relating reductions systems
   - [Inference]({{ site.baseurl }}/Inference/): Bidirectional type inference
diff --git a/src/plfa/part3/Soundness.lagda.md b/src/plfa/part3/Soundness.lagda.md
index a1f788e7..e6a306ed 100644
--- a/src/plfa/part3/Soundness.lagda.md
+++ b/src/plfa/part3/Soundness.lagda.md
@@ -61,7 +61,7 @@ open import plfa.part3.Compositional using (lambda-inversion; var-inv)
 The proof of preservation in this section mixes techniques from
 previous chapters. Like the proof of preservation for the STLC, we are
 preserving a relation defined separately from the syntax, in contrast
-to the inherently typed terms. On the other hand, we are using de
+to the intrinsically-typed terms. On the other hand, we are using de
 Bruijn indices for variables.
 
 The outline of the proof remains the same in that we must prove lemmas