From 0559135e4ee31dcc2b1a60f08e5b444932bdef92 Mon Sep 17 00:00:00 2001
From: Hillosanation <88579655+Hillosanation@users.noreply.github.com>
Date: Thu, 24 Sep 2026 21:12:45 +0800
Subject: [PATCH] Update Confluence.lagda.md

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

diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md
index 794c12ff7..24e61f36a 100644
--- a/src/plfa/part2/Confluence.lagda.md
+++ b/src/plfa/part2/Confluence.lagda.md
@@ -225,7 +225,7 @@ The proof is by induction on `M ⇛ N`.
 * Suppose `(ƛ N) · M  ⇛  N′ [ M′ ]` because `N ⇛ N′` and `M ⇛ M′`.
   By similar reasoning, we have
   `(ƛ N) · M —↠ (ƛ N′) · M′`
-  which we can following with the β reduction
+  which we can follow with the β reduction
   `(ƛ N′) · M′ —→ N′ [ M′ ]`.
 
 With this lemma in hand, we complete the proof that `M ⇛* N` implies