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