diff --git a/src/plfa/part2/BigStep.lagda.md b/src/plfa/part2/BigStep.lagda.md
index 1db1a1fd..f438d258 100644
--- a/src/plfa/part2/BigStep.lagda.md
+++ b/src/plfa/part2/BigStep.lagda.md
@@ -24,7 +24,7 @@ after we have developed a denotational semantics for the lambda
 calculus, at which point the proof is an easy corollary of properties
 of the denotational semantics.
 
-We present the call-by-name strategy as a relation between an an input
+We present the call-by-name strategy as a relation between an input
 term and an output value. Such a relation is often called a _big-step
 semantics_, written `M ⇓ V`, as it relates the input term `M` directly
 to the final result `V`, in contrast to the small-step reduction
diff --git a/src/plfa/part2/Bisimulation.lagda.md b/src/plfa/part2/Bisimulation.lagda.md
index dfe23bc3..de161ea8 100644
--- a/src/plfa/part2/Bisimulation.lagda.md
+++ b/src/plfa/part2/Bisimulation.lagda.md
@@ -449,7 +449,7 @@ In its structure, it looks a little bit like a proof of progress:
               ~                         ~
               |                         |
               |                         |
-        (ƛ x ⇒ N†) · V† --- —→ --- N† [ x := V ]
+        (ƛ x ⇒ N†) · V† --- —→ --- N† [ x := V† ]
 
     Since simulation commutes with values and `V` is a value, `V†` is also a value.
     Since simulation commutes with substitution and `N ~ N†` and `V ~ V†`,