diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr
index 8d67c2b..24c7018 100644
--- a/lib/Quox/Syntax/Term/Tighten.idr
+++ b/lib/Quox/Syntax/Term/Tighten.idr
@@ -8,23 +8,11 @@ import Quox.No
 %default total
 
 
-export
-Tighten (Shift f) where
-  -- `OPE m n` is a spicy `m ≤ n`,
-  -- and `Shift f n` is a (different) spicy `f ≤ n`
-  -- so the value is `f ≤ m` (as a `Shift`), if that is the case
-  tighten _        SZ      = Nothing
-  tighten Id       by      = Just by
-  tighten (Drop p) (SS by) = tighten p by
-  tighten (Keep p) (SS by) = [|SS $ tighten p by|]
-
-
 export
 Tighten Dim where
   tighten p (K e loc) = pure $ K e loc
   tighten p (B i loc) = B <$> tighten p i <*> pure loc
 
-
 export
 tightenScope : (forall m, n. OPE m n -> f n -> Maybe (f m)) ->
                {s : Nat} -> OPE m n -> Scoped s f n -> Maybe (Scoped s f m)