Fix cong-rename

M on the right hand side of ≡ should be M′
2020-05-20 16:12:54 +08:00 · 2020-05-20 16:12:54 +08:00 · 33f0f64624
commit 33f0f64624
parent 0a99b734ba
1 changed files with 1 additions and 1 deletions
--- 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)