diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md
index c6705f5b..072368a2 100644
--- a/src/plfa/part2/Properties.lagda.md
+++ b/src/plfa/part2/Properties.lagda.md
@@ -742,8 +742,8 @@ Now that naming is resolved, let's unpack the first three cases:
 
         ∅ ⊢ V ⦂ B
         Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C
-        ------------------------------------
-        Γ , x ⦂ A , y ⦂ B ⊢ N [ y := V ] ⦂ C
+        ----------------------------
+        Γ , x ⦂ A ⊢ N [ y := V ] ⦂ C
 
     The typing rule for abstractions then yields the required conclusion.