diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index 7bd96eb..5bfe956 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -73,8 +73,8 @@ tel1 . (tel2 :< s) = (tel1 . tel2) :< s
 public export
 getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) ->
                Shift len out -> Context tm len -> Var len -> tm out
-getShiftWith shft by (ctx :< t) VZ     = t `shft` drop1 by
-getShiftWith shft by (ctx :< t) (VS i) = getShiftWith shft (drop1 by) ctx i
+getShiftWith shft by (ctx :< t) VZ     = t `shft` ssDown by
+getShiftWith shft by (ctx :< t) (VS i) = getShiftWith shft (ssDown by) ctx i
 
 public export %inline
 getShift : CanShift tm => Shift len out -> Context tm len -> Var len -> tm out
diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index 3ac70ac..9bb0cac 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -149,7 +149,7 @@ private
 0 newGetShift : (d : Nat) -> (i : Var d) -> (by : Shift d d') ->
                 getShift' by (new' {d}) i = Nothing
 newGetShift (S d) VZ     by = Refl
-newGetShift (S d) (VS i) by = newGetShift d i (drop1 by)
+newGetShift (S d) (VS i) by = newGetShift d i (ssDown by)
 
 export
 0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' {d}) i = Nothing
diff --git a/lib/Quox/Syntax/Shift.idr b/lib/Quox/Syntax/Shift.idr
index 18dfb99..9face99 100644
--- a/lib/Quox/Syntax/Shift.idr
+++ b/lib/Quox/Syntax/Shift.idr
@@ -195,30 +195,6 @@ prettyShift bnd by =
 export PrettyHL (Shift from to) where prettyM = prettyShift TVar
 
 
-||| Drops the innermost variable from the input scope.
-public export
-drop1 : Shift (S from) to -> Shift from to
-drop1 SZ      = SS SZ
-drop1 (SS by) = SS (drop1 by)
-
-private
-drop1ViaNat : Shift (S from) to -> Shift from to
-drop1ViaNat by =
-  rewrite shiftDiff by in
-  rewrite sym $ plusSuccRightSucc by.nat from in
-  fromNat (S by.nat)
-
-private
-0 drop1ViaNatCorrect : (by : Shift (S from) to) -> drop1ViaNat by = drop1 by
-drop1ViaNatCorrect SZ = Refl
-drop1ViaNatCorrect (SS by) =
-  rewrite plusSuccRightSucc by.nat from in
-  rewrite sym $ shiftDiff by in
-  cong SS $ drop1ViaNatCorrect by
-
-%transform "Shift.drop1" drop1 by = drop1ViaNat by
-
-
 infixl 8 //
 public export
 interface CanShift f where
diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr
index 1c5451c..7b6e53f 100644
--- a/lib/Quox/Syntax/Subst.idr
+++ b/lib/Quox/Syntax/Subst.idr
@@ -86,7 +86,7 @@ push th = fromVar VZ ::: (th . shift 1)
 
 public export
 drop1 : Subst f (S from) to -> Subst f from to
-drop1 (Shift by) = Shift $ drop1 by
+drop1 (Shift by) = Shift $ ssDown by
 drop1 (t ::: th) = th