From 724ec8542373d5891b2f96916efcbf9d4dec231a Mon Sep 17 00:00:00 2001
From: Jeremy Siek <jsiek@indiana.edu>
Date: Wed, 25 Mar 2020 15:42:33 -0400
Subject: [PATCH] substZero

---
 src/plfa/part2/More.lagda.md | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md
index b1137fee..e0e40bd9 100644
--- a/src/plfa/part2/More.lagda.md
+++ b/src/plfa/part2/More.lagda.md
@@ -785,16 +785,16 @@ subst σ (case× L M)    =  case× (subst σ L) (subst (exts (exts σ)) M)
 ## Single and double substitution
 
 ```
+substZero : ∀ {Γ}{A B} → Γ ⊢ A → Γ , A ∋ B → Γ ⊢ B
+substZero V Z      =  V
+substZero V (S x)  =  ` x
+
 _[_] : ∀ {Γ A B}
   → Γ , A ⊢ B
   → Γ ⊢ A
     ---------
   → Γ ⊢ B
-_[_] {Γ} {A} N V =  subst {Γ , A} {Γ} σ N
-  where
-  σ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B
-  σ Z      =  V
-  σ (S x)  =  ` x
+_[_] {Γ} {A} N V =  subst {Γ , A} {Γ} (substZero V) N
 
 _[_][_] : ∀ {Γ A B C}
   → Γ , A , B ⊢ C