From 0f8be1980296ed52541c705f1338e77719920ca5 Mon Sep 17 00:00:00 2001 From: Altaria Date: Fri, 25 Jun 2021 11:22:18 +0100 Subject: [PATCH] fixed indentation for proper code display --- src/plfa/part2/Substitution.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part2/Substitution.lagda.md b/src/plfa/part2/Substitution.lagda.md index e5a25a12..9897931c 100644 --- a/src/plfa/part2/Substitution.lagda.md +++ b/src/plfa/part2/Substitution.lagda.md @@ -807,11 +807,11 @@ We proceed by induction on the term `M`. * If `M = ƛ N`, we first use the induction hypothesis to show that - ƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N) ≡ ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N + ƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N) ≡ ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N and then use the lemma `exts-seq` to show - ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N ≡ ƛ ⟪ exts ( σ₁ ⨟ σ₂) ⟫ N + ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N ≡ ƛ ⟪ exts ( σ₁ ⨟ σ₂) ⟫ N * If `M` is an application, we use the induction hypothesis for both subterms.