From a85b9d7ad841a4a1e860fa5e3dc8bc7734087b7c Mon Sep 17 00:00:00 2001
From: Thorsten Altenkirch <txa@cs.nott.ac.uk>
Date: Thu, 22 Jun 2023 17:25:38 +0200
Subject: [PATCH] minor

---
 fol-subst.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/fol-subst.agda b/fol-subst.agda
index cbd5ee1..6c0c2e1 100644
--- a/fol-subst.agda
+++ b/fol-subst.agda
@@ -36,7 +36,7 @@ comp ε us = ε
 comp (ts , u) us = (comp ts us) , (subst-t u us)
 
 {-
-t [ suc vs ] ≡ suc (t [vs ])
+t [ suc-subst vs ] ≡ suc (t [vs ])
 suc-subst ts ∘ (us , t) ≡ ts ∘ us
 
 t [ id ] ≡ t