From b2053ddc1aa849e563417422d6e6dc719ac028f8 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Mon, 20 May 2019 10:15:45 -0400 Subject: [PATCH] added a little text --- src/plfa/Substitution.lagda | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/plfa/Substitution.lagda b/src/plfa/Substitution.lagda index e04e3bee..8f99fc23 100644 --- a/src/plfa/Substitution.lagda +++ b/src/plfa/Substitution.lagda @@ -704,11 +704,14 @@ The proof is by induction on the term `M`. The last lemma needed to prove `sub-sub` states that the `exts` function distributes with sequencing. It is a corollary of -`commute-subst-rename`. We describe the proof below. +`commute-subst-rename` as described below. (It would have been nicer +to prove this directly by equational reasoning in the σ algebra, but +that would require the `sub-assoc` equation, whose proof depends on +`sub-sub`, which in turn depends on this lemma.) \begin{code} exts-seq : ∀{Γ Δ Δ′} {σ₁ : Subst Γ Δ} {σ₂ : Subst Δ Δ′} - → ∀ {A} → (exts σ₁ ⨟ exts σ₂) {A} ≡ exts (σ₁ ⨟ σ₂) + → ∀ {A} → (exts σ₁ ⨟ exts σ₂) {A} ≡ exts (σ₁ ⨟ σ₂) exts-seq = extensionality λ x → lemma {x = x} where lemma : ∀{Γ Δ Δ′}{A}{x : Γ , ★ ∋ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Δ′}