From 33f0f6462446a90f89f1c4ef2e168d864f270648 Mon Sep 17 00:00:00 2001 From: Liang-Ting Chen Date: Wed, 20 May 2020 16:12:54 +0800 Subject: [PATCH] Fix cong-rename MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit M on the right hand side of ≡ should be M′ --- src/plfa/part2/Substitution.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Substitution.lagda.md b/src/plfa/part2/Substitution.lagda.md index b8c5e361..536adb4a 100644 --- a/src/plfa/part2/Substitution.lagda.md +++ b/src/plfa/part2/Substitution.lagda.md @@ -349,7 +349,7 @@ cong-ext{Γ}{Δ}{ρ}{ρ′}{B} rr {A} = extensionality λ x → lemma {x} cong-rename : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ}{B}{M M′ : Γ ⊢ B} → (∀{A} → ρ ≡ ρ′ {A}) → M ≡ M′ ------------------------------ - → rename ρ M ≡ rename ρ′ M + → rename ρ M ≡ rename ρ′ M′ cong-rename {M = ` x} rr refl = cong `_ (cong-app rr x) cong-rename {ρ = ρ} {ρ′ = ρ′} {M = ƛ N} rr refl = cong ƛ_ (cong-rename {ρ = ext ρ}{ρ′ = ext ρ′}{M = N} (cong-ext rr) refl)