From 61a8a4bbe40f67736fd3f5dead006d079d54391b Mon Sep 17 00:00:00 2001
From: Hillosanation <88579655+Hillosanation@users.noreply.github.com>
Date: Mon, 28 Sep 2026 17:48:00 +0800
Subject: [PATCH 1/2] fix typo

---
 src/plfa/part2/BigStep.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/plfa/part2/BigStep.lagda.md b/src/plfa/part2/BigStep.lagda.md
index 9cee24b5b..050b35794 100644
--- a/src/plfa/part2/BigStep.lagda.md
+++ b/src/plfa/part2/BigStep.lagda.md
@@ -312,7 +312,7 @@ 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)`

From 60e39fd9cd2ba8b67d4c6c89a38796233c90414c Mon Sep 17 00:00:00 2001
From: Hillosanation <88579655+Hillosanation@users.noreply.github.com>
Date: Mon, 28 Sep 2026 18:12:58 +0800
Subject: [PATCH 2/2] fix typo

---
 src/plfa/part2/BigStep.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/plfa/part2/BigStep.lagda.md b/src/plfa/part2/BigStep.lagda.md
index 050b35794..b5e2f0024 100644
--- a/src/plfa/part2/BigStep.lagda.md
+++ b/src/plfa/part2/BigStep.lagda.md
@@ -316,7 +316,7 @@ to consider.
 
 * 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 `γ ≈ₑ σ`,