From 776f10940dd36ca975396a776a5cd2d03fd4a0e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Mon, 13 Jan 2020 10:45:46 +0100 Subject: [PATCH] Properties: fix the inductive hypothesis for lambda abstraction in the description of the proof of subst --- src/plfa/part2/Properties.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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.