Bug in appendix Substitution

[wadler]

Section The σ algebra equations contains the equation

(sub-abs)   ⟪ σ ⟫ (ƛ N)    ≡ ƛ ⟪ σ ⟫ N

This is wrong, as is the subsequent discussion ("The equations sub-app and sub-abs says that substitution is a congruence for the lambda calculus. ") Later, the correct equation is stated and proved.

sub-abs : ∀{Γ Δ} {σ : Subst Γ Δ} {N : Γ , ★ ⊢ ★}
        → ⟪ σ ⟫ (ƛ N) ≡ ƛ ⟪ (` Z) • (σ ⨟ ↑) ⟫ N

[jsiek]

Thanks for noticing this! I've made a pull request to fix it.

[noughtmare]

It seems this issue can be closed.