diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index a7c00eb..54e38b2 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -75,6 +75,11 @@ public export %inline
 (!!) : CanShift tm => Context tm len -> Var len -> tm len
 ctx !! i = getShift ctx i SZ
 
+infixl 8 !?
+public export %inline
+(!?) : Context' tm len -> Var len -> tm
+ctx !? i = (ctx !! i) @{Const}
+
 
 ||| a triangle of bindings. each type binding in a context counts the ues of
 ||| others in its type, and all of these together form a triangle.
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index 5e23ebe..75b7b7e 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -204,3 +204,7 @@ interface CanShift f where
   (//) : f from -> Shift from to -> f to
 
 export CanShift Var where i // by = shift by i
+
+namespace CanShift
+  export
+  [Const] CanShift (\_ => a) where x // _ = x