diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 9247619..49f6aef 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -36,17 +36,17 @@ mutual
 
     ||| function type
     Pi  : (qty, qtm : Qty) -> (x : Name) ->
-          (a : Term d n) -> (b : Term d (S n)) -> Term d n
+          (arg : Term d n) -> (res : Term d (S n)) -> Term d n
     ||| function term
-    Lam : (x : Name) -> (t : Term d (S n)) -> Term d n
+    Lam : (x : Name) -> (body : Term d (S n)) -> Term d n
 
     ||| elimination
     E : (e : Elim d n) -> Term d n
 
     ||| term closure/suspended substitution
-    CloT  : (s : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
+    CloT  : (tm : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
     ||| dimension closure/suspended substitution
-    DCloT : (s : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
+    DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
 
   ||| first argument `d` is dimension scope size, second `n` is term scope size
   public export
@@ -57,15 +57,15 @@ mutual
     B : (i : Var n) -> Elim d n
 
     ||| term application
-    (:@) : (f : Elim d n) -> (s : Term d n) -> Elim d n
+    (:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
 
     ||| type-annotated term
-    (:#) : (s, a : Term d n) -> Elim d n
+    (:#) : (tm, ty : Term d n) -> Elim d n
 
     ||| term closure/suspended substitution
-    CloE  : (e : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
+    CloE  : (el : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
     ||| dimension closure/suspended substitution
-    DCloE : (e : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
+    DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
 
 %name Term s, t, r
 %name Elim e, f
@@ -323,8 +323,8 @@ parameters {auto _ : Alternative f}
   ||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)`
   export
   betaLam1 : Elim d n -> f (Elim d n)
-  betaLam1 ((Lam {t, _} :# Pi {a, b, _}) :@ s) =
-    pure $ (t :# b) // (s :# a ::: id)
+  betaLam1 ((Lam {body, _} :# Pi {arg, res, _}) :@ s) =
+    pure $ (body :# res) // (s :# arg ::: id)
   betaLam1 _ = empty
 
   ||| `(e ⦂ A) >>> e`    [if `e` is an elim]