diff --git a/src/plfa/Bisimulation.lagda.md b/src/plfa/Bisimulation.lagda.md
index 11ab3ba4..23d242d9 100644
--- a/src/plfa/Bisimulation.lagda.md
+++ b/src/plfa/Bisimulation.lagda.md
@@ -232,7 +232,7 @@ where appropriate (in this case, only for the body of an abstraction).
 ## Simulation commutes with substitution
 
 The third technical result is that simulation commutes with substitution.
-It is more complex than substitution, because where we had one renaming map
+It is more complex than renaming, because where we had one renaming map
 `ρ` here we need two substitution maps, `σ` and `σ†`.
 
 The proof first requires we establish an analogue of extension.