diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 6017846..a707495 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -90,8 +90,8 @@ mutual
 %name DScopeTerm body
 
 public export %inline
-Arr : Qty -> Term d n -> Term d n -> Term d n
-Arr pi a b = Pi {qty = pi, x = "_", arg = a, res = TUnused b}
+Arr : (qty : Qty) -> (arg, res : Term d n) -> Term d n
+Arr {qty, arg, res} = Pi {qty, x = "_", arg, res = TUnused res}
 
 ||| same as `F` but as a term
 public export %inline