diff --git a/src/Quox/Ctx.idr b/src/Quox/Ctx.idr
deleted file mode 100644
index 56a2991..0000000
--- a/src/Quox/Ctx.idr
+++ /dev/null
@@ -1,98 +0,0 @@
-module Quox.Ctx
-
-import Data.Nat
-import Data.Fin
-import Data.SnocList
-import Data.DPair
-
-
-%default total
-
-public export
-data Ctx : Nat -> (Nat -> Type) -> Type where
-  Lin  : Ctx 0 f
-  (:<) : Ctx n f -> f n -> Ctx (S n) f
-
-%name Ctx ctx
-
-
-public export
-0 Ctx' : Nat -> Type -> Type
-Ctx' n a = Ctx n (\_ => a)
-
-
-public export
-toSList : Ctx n f -> SnocList (Exists f)
-toSList [<]        = [<]
-toSList (ctx :< x) = toSList ctx :< Evidence _ x
-
-public export
-toSList' : Ctx' n a -> SnocList a
-toSList' ctx = map (.snd) $ toSList ctx
-
-public export
-fromSList' : (xs : SnocList a) -> Ctx' (length xs) a
-fromSList' [<]       = [<]
-fromSList' (sx :< x) = fromSList' sx :< x
-
-
-public export
-0 Weaken : (Nat -> Type) -> Type
-Weaken f = forall n. (by : Nat) -> (1 x : f n) -> f (by + n)
-
-public export
-interface Weak f where weakN : Weaken f
-
-public export
-weak : Weak f => (1 x : f n) -> f (S n)
-weak = weakN 1
-
-
-public export
-lookBy : Weaken f -> Ctx n f -> (1 _ : Fin n) -> f n
-lookBy w = go 0 where
-  go : forall n. (by : Nat) -> Ctx n f -> (1 _ : Fin n) -> f (by + n)
-  go by (ctx :< x) (FZ {k})   =
-    rewrite sym $ plusSuccRightSucc by k in w (S by) x
-  go by (ctx :< x) (FS {k} i) =
-    rewrite sym $ plusSuccRightSucc by k in go (S by) ctx i
-
-public export
-look : Weak f => Ctx n f -> (1 _ : Fin n) -> f n
-look = lookBy weakN
-
-infixl 9 !!
-public export
-(!!) : Ctx' n a -> (1 _ : Fin n) -> a
-(!!) = lookBy (\_, x => x)
-
-
-public export
-map : (forall n. f n -> g n) -> (1 _ : Ctx n f) -> Ctx n g
-map f [<]        = [<]
-map f (ctx :< x) = map f ctx :< f x
-
-
-public export
-(forall n. Eq (f n)) => Eq (Ctx n f) where
-  [<]         == [<]         = True
-  (ctx1 :< x) == (ctx2 :< y) = ctx1 == ctx2 && x == y
-
-public export
-(forall n. Ord (f n)) => Ord (Ctx n f) where
-  compare [<]         [<]         = EQ
-  compare (ctx1 :< x) (ctx2 :< y) = compare ctx1 ctx2 <+> compare x y
-
-
-||| like `Exists` but only shows the second part
-private
-data ShowWrapper : (Nat -> Type) -> Type where
-  SW : f n -> ShowWrapper f
-
-private
-(forall n. Show (f n)) => Show (ShowWrapper f) where
-  showPrec d (SW x) = showPrec d x
-
-export
-(forall n. Show (f n)) => Show (Ctx n f) where
-  show = show . map (\x => SW {f} x.snd) . toSList
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 6be5fcd..91efaf9 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -1,6 +1,5 @@
 module Quox.Syntax.Term
 
-import public Quox.Ctx
 import public Quox.Syntax.Var
 import public Quox.Syntax.Shift
 import public Quox.Syntax.Subst