diff --git a/src/plfa/part2/BigStep.lagda.md b/src/plfa/part2/BigStep.lagda.md
index 9cee24b5b..b5e2f0024 100644
--- a/src/plfa/part2/BigStep.lagda.md
+++ b/src/plfa/part2/BigStep.lagda.md
@@ -312,11 +312,11 @@ to consider.
   Using `δ ⊢ L ⇓ V` and `δ ≈ₑ τ`,
   the induction hypothesis gives us
   `subst τ L —↠ N` and `V ≈ N` for some `N`.
-  So we have shown that `subst σ x —↠ N` and `V ≈ N` for some `N`.
+  So we have shown that `subst σ (` x) —↠ N` and `V ≈ N` for some `N`.
 
 * Case `⇓-lam`.
   We immediately have `subst σ (ƛ N) —↠ subst σ (ƛ N)`
-  and `clos (subst σ (ƛ N)) γ ≈ subst σ (ƛ N)`.
+  and `clos (ƛ N) γ ≈ subst σ (ƛ N)`.
 
 * Case `⇓-app`.
   Using `γ ⊢ L ⇓ clos (ƛ N) δ` and `γ ≈ₑ σ`,