diff --git a/lib/Quox/Syntax/Term/Reduce.idr b/lib/Quox/Syntax/Term/Reduce.idr
index e1fac68..574407c 100644
--- a/lib/Quox/Syntax/Term/Reduce.idr
+++ b/lib/Quox/Syntax/Term/Reduce.idr
@@ -116,6 +116,7 @@ pushSubstsE' : Elim d n -> Elim d n
 pushSubstsE' e = (pushSubstsE e).fst
 
 
+{- [todo] remove these probably?
 mutual
   -- tightening a term/elim also causes substitutions to be pushed through.
   -- this is because otherwise a variable in an unused part of the subst
@@ -156,6 +157,7 @@ mutual
   Tighten (ScopeTerm d) where
     tighten p (TUsed   body) = TUsed   <$> tighten (Keep p) body
     tighten p (TUnused body) = TUnused <$> tighten p body
+-}
 
 
 public export %inline
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index a937fec..4840350 100644
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@@ -264,6 +264,7 @@ decEqFromBool i j =
 
 public export %inline DecEq (Var n) where decEq = varDecEq
 
+{- [todo] remove this probably?
 export
 Tighten Var where
   tighten Id       i      = pure i
@@ -271,3 +272,4 @@ Tighten Var where
   tighten (Drop q) (VS i) = tighten q i
   tighten (Keep q) VZ     = pure VZ
   tighten (Keep q) (VS i) = VS <$> tighten q i
+-}