diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index 6035633..1c5451c 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -90,6 +90,11 @@ drop1 (Shift by) = Shift $ drop1 by
 drop1 (t ::: th) = th
 
 
+public export %inline
+one : f n -> Subst f (S n) n
+one x = x ::: id
+
+
 ||| `prettySubst pr names bnd op cl th` pretty-prints the substitution `th`,
 ||| with the following arguments:
 |||