diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 0ff7b3b..994b570 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -133,7 +133,6 @@ data Term where
   ||| dimension closure/suspended substitution
   DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
 
-||| first argument `d` is dimension scope size, second `n` is term scope size
 public export
 data Elim where
   ||| free variable, possibly with a displacement (see @crude, or @mugen for a