diff --git a/src/Quox.idr b/src/Quox.idr
index 785cc8a..cd617fa 100644
--- a/src/Quox.idr
+++ b/src/Quox.idr
@@ -1,6 +1,6 @@
 module Quox
 
-import public Quox.Syntax
+import public Quox.Syntax.Term
 import public Quox.Pretty
 
 import Data.Nat
diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
deleted file mode 100644
index a3c81b0..0000000
--- a/src/Quox/Context.idr
+++ /dev/null
@@ -1,185 +0,0 @@
-module Quox.Context
-
-import Quox.Syntax.Shift
-import Quox.Pretty
-
-import Data.DPair
-import Data.Nat
-import Data.SnocList
-import Control.Monad.Identity
-
-%default total
-
-
-infixl 5 :<
-||| a sequence of bindings under an existing context. each successive element
-||| has one more bound variable, which correspond to all previous elements
-||| as well as the global context.
-public export
-data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where
-  Lin  : Telescope tm from from
-  (:<) : Telescope tm from to -> tm to -> Telescope tm from (S to)
-%name Telescope tel
-
-||| a global context is actually just a telescope over no existing bindings
-public export
-Context : (tm : Nat -> Type) -> (len : Nat) -> Type
-Context tm len = Telescope tm 0 len
-
-export
-toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
-toSnocList [<]        = [<]
-toSnocList (tel :< t) = toSnocList tel :< Evidence _ t
-
-private
-toList' : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
-toList' [<]        acc = acc
-toList' (tel :< t) acc = toList' tel (Evidence _ t :: acc)
-
-export %inline
-toList : Telescope tm _ _ -> List (Exists tm)
-toList tel = toList' tel []
-
-
-infixl 9 .
-public export
-(.) : Telescope tm from mid -> Telescope tm mid to -> Telescope tm from to
-tel1 . [<]         = tel1
-tel1 . (tel2 :< s) = (tel1 . tel2) :< s
-
-
-export
-getWith : CanShift tm => Context tm len -> Var len -> Shift len out -> tm out
-getWith (ctx :< t) VZ     th = t // drop1 th
-getWith (ctx :< t) (VS i) th = getWith ctx i (drop1 th)
-
-infixl 8 !!
-export %inline
-(!!) : CanShift tm => Context tm len -> Var len -> tm len
-ctx !! i = getWith ctx i SZ
-
-
-||| 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.
-public export
-Triangle : (tm : Nat -> Type) -> (len : Nat) -> Type
-Triangle = Context . Context
-
-
-export
-0 telescopeLTE : Telescope _ from to -> from `LTE` to
-telescopeLTE [<]        = reflexive {rel=LTE}
-telescopeLTE (tel :< _) = lteSuccRight $ telescopeLTE tel
-
-export
-(from `GT` to) => Uninhabited (Telescope _ from to) where
-  uninhabited tel = void $ LTEImpliesNotGT (telescopeLTE tel) %search
-
-export %hint
-0 succGT : S n `GT` n
-succGT = LTESucc $ reflexive {rel=LTE}
-
-export %inline
-absurd0 : (0 _ : Uninhabited a) => (0 _ : a) -> x
-absurd0 x = void $ absurd x
-
-
-parameters {auto _ : Applicative f}
-  export
-  traverse : (forall n. tm1 n -> f (tm2 n)) ->
-             Telescope tm1 from to -> f (Telescope tm2 from to)
-  traverse f [<]        = pure [<]
-  traverse f (tel :< x) = [|traverse f tel :< f x|]
-
-  infixl 3 `app`
-  ||| like `(<*>)` but with effects
-  export
-  app : Telescope (\n => tm1 n -> f (tm2 n)) from to ->
-        Telescope tm1 from to -> f (Telescope tm2 from to)
-  app [<]         [<]         = pure [<]
-  app (ftel :< f) (xtel :< x) = [|app ftel xtel :< f x|]
-  app [<]         (xtel :< _) = absurd0 xtel
-  app (ftel :< _) [<]         = absurd0 ftel
-
-  export %inline
-  sequence : Telescope (f . tm) from to -> f (Telescope tm from to)
-  sequence = traverse id
-
-export %inline
-map : (forall n. tm1 n -> tm2 n) ->
-      Telescope tm1 from to -> Telescope tm2 from to
-map f = runIdentity . traverse (pure . f)
-
-infixr 4 <$>
-export %inline
-(<$>) : (forall n. tm1 n -> tm2 n) ->
-        Telescope tm1 from to -> Telescope tm2 from to
-(<$>) = map
-
-infixl 3 <*>
-export %inline
-(<*>) : Telescope (\n => tm1 n -> tm2 n) from to ->
-        Telescope tm1 from to -> Telescope tm2 from to
-ftel <*> xtel = runIdentity $ (pure .) <$> ftel `app` xtel
--- ...but can't write pure without `from,to` being relevant,
--- so no idiom brackets ☹
-
-export %inline
-zipWith : (forall n. tm1 n -> tm2 n -> tm3 n) ->
-          Telescope tm1 from to -> Telescope tm2 from to ->
-          Telescope tm3 from to
-zipWith f tel1 tel2 = f <$> tel1 <*> tel2
-
-export %inline
-zipWith3 : (forall n. tm1 n -> tm2 n -> tm3 n -> tm4 n) ->
-           Telescope tm1 from to ->
-           Telescope tm2 from to ->
-           Telescope tm3 from to ->
-           Telescope tm4 from to
-zipWith3 f tel1 tel2 tel3 = f <$> tel1 <*> tel2 <*> tel3
-
-
-export
-lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
-lengthPrf [<]        = Element 0 Refl
-lengthPrf (tel :< _) =
-  let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
-
-public export %inline
-length : Telescope {} -> Nat
-length = fst . lengthPrf
-
-
-parameters {0 acc : Nat -> Type}
-  export
-  foldl : (forall m, n. acc m -> tm n -> acc (S m)) ->
-          acc 0 -> (tel : Telescope tm from to) -> acc (length tel)
-  foldl f z [<]        = z
-  foldl f z (tel :< t) = f (foldl f z tel) t
-
-parameters {auto _ : Monoid a}
-  export %inline
-  foldMap : (forall n. tm n -> a) -> Telescope tm from to -> a
-  foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
-
-  export %inline
-  fold : Telescope (\x => a) from to -> a
-  fold = foldMap id
-
-  ||| like `fold` but calculate the elements only when actually appending
-  export %inline
-  foldLazy : Telescope (\x => Lazy a) from to -> a
-  foldLazy = foldMap force
-
-
-export
-(forall n. Eq (tm n)) => Eq (Telescope tm from to) where
-  (==) = fold @{All} .: zipWith (==)
-
-export
-(forall n. Ord (tm n)) => Ord (Telescope tm from to) where
-  compare = foldLazy .: zipWith (delay .: compare)
-
-export
-(forall n. PrettyHL (tm n)) => PrettyHL (Telescope tm from to) where
-  prettyM tel = separate (hl Delim ";") <$> traverse prettyM (toList tel)
diff --git a/src/Quox/Eval.idr b/src/Quox/Eval.idr
deleted file mode 100644
index ba1e892..0000000
--- a/src/Quox/Eval.idr
+++ /dev/null
@@ -1,30 +0,0 @@
-module Quox.Eval
-
--- todo list:
--- - understand nbe and use it
--- - take a proof of well-typedness as an argument
-
-import Quox.Syntax
-
-import Data.DPair
-
-%default total
-
-
-public export Exists2 : (ty1 -> ty2 -> Type) -> Type
-Exists2 t = Exists (\a => Exists (\b => t a b))
-
-public export SomeTerm : Type
-SomeTerm = Exists2 Term
-
-public export SomeElim : Type
-SomeElim = Exists2 Elim
-
-public export SomeDim : Type
-SomeDim = Exists Dim
-
-private some : {0 t : ty -> Type} -> t a -> Exists t
-some t = Evidence ? t
-
-private some2 : {0 t : ty1 -> ty2 -> Type} -> t a b -> Exists2 t
-some2 t = some $ some t
diff --git a/src/Quox/Pretty.idr b/src/Quox/Pretty.idr
index d6178ef..a9296ba 100644
--- a/src/Quox/Pretty.idr
+++ b/src/Quox/Pretty.idr
@@ -87,35 +87,16 @@ hlF' : Functor f => HL -> f (Doc HL) -> f (Doc HL)
 hlF' = map . hl'
 
 
-export %inline
+export
 parens : Doc HL -> Doc HL
 parens doc = hl Delim "(" <+> doc <+> hl Delim ")"
 
-export %inline
+export
 parensIf : Bool -> Doc HL -> Doc HL
 parensIf True  = parens
 parensIf False = id
 
 
-export
-separate' : Doc a -> List (Doc a) -> List (Doc a)
-separate' s []        = []
-separate' s [x]       = [x]
-separate' s (x :: xs) = x <+> s :: separate' s xs
-
-export %inline
-separate : Doc a -> List (Doc a) -> Doc a
-separate s = sep . separate' s
-
-export %inline
-hseparate : Doc a -> List (Doc a) -> Doc a
-hseparate s = hsep . separate' s
-
-export %inline
-vseparate : Doc a -> List (Doc a) -> Doc a
-vseparate s = vsep . separate' s
-
-
 public export
 record PrettyEnv where
   constructor MakePrettyEnv
@@ -131,21 +112,21 @@ record PrettyEnv where
 public export %inline HasEnv : (Type -> Type) -> Type
 HasEnv = MonadReader PrettyEnv
 
-export %inline
+export
 ifUnicode : HasEnv m => (uni, asc : Lazy a) -> m a
 ifUnicode uni asc = if (!ask).unicode then [|uni|] else [|asc|]
 
-export %inline
+export
 parensIfM : HasEnv m => PPrec -> Doc HL -> m (Doc HL)
 parensIfM d doc = pure $ parensIf ((!ask).prec > d) doc
 
-export %inline
+export
 withPrec : HasEnv m => PPrec -> m a -> m a
 withPrec d = local {prec := d}
 
 public export data BinderSort = T | D
 
-export %inline
+export
 under : HasEnv m => BinderSort -> Name -> m a -> m a
 under s x = local $
   {prec := Outer} .
@@ -180,7 +161,7 @@ export PrettyHL BaseName where prettyM = pure . pretty . baseStr
 export PrettyHL Name     where prettyM = pure . pretty . toDots
 
 
-export %inline
+export
 prettyStr : PrettyHL a => {default True unicode : Bool} -> a -> String
 prettyStr {unicode} =
   let layout = layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) in
@@ -199,7 +180,7 @@ termHL Qty     = color BrightMagenta <+> bold
 termHL Free    = color BrightWhite
 termHL Syntax  = color BrightBlue
 
-export %inline
+export
 prettyTerm : {default True color, unicode : Bool} -> PrettyHL a => a -> IO Unit
 prettyTerm x {color, unicode} =
   let reann = if color then map termHL else unAnnotate in
diff --git a/src/Quox/Syntax.idr b/src/Quox/Syntax.idr
deleted file mode 100644
index 505f9b0..0000000
--- a/src/Quox/Syntax.idr
+++ /dev/null
@@ -1,9 +0,0 @@
-module Quox.Syntax
-
-import public Quox.Syntax.Dim
-import public Quox.Syntax.Qty
-import public Quox.Syntax.Shift
-import public Quox.Syntax.Subst
-import public Quox.Syntax.Term
-import public Quox.Syntax.Universe
-import public Quox.Syntax.Var
diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr
index 3cec218..90c0783 100644
--- a/src/Quox/Syntax/Qty.idr
+++ b/src/Quox/Syntax/Qty.idr
@@ -35,33 +35,20 @@ prettyQtyBinds =
 
 
 public export
-plus : Qty -> Qty -> Qty
-plus Zero rh   = rh
-plus pi   Zero = pi
-plus _    _    = Any
+(+) : Qty -> Qty -> Qty
+Zero + rh   = rh
+pi   + Zero = pi
+_    + _    = Any
 
 public export
-times : Qty -> Qty -> Qty
-times Zero _    = Zero
-times _    Zero = Zero
-times One  rh   = rh
-times pi   One  = pi
-times Any  Any  = Any
+(*) : Qty -> Qty -> Qty
+Zero * _    = Zero
+_    * Zero = Zero
+One  * rh   = rh
+pi   * One  = pi
+Any  * Any  = Any
 
 infix 6 <=.
 public export
-compat : Qty -> Qty -> Bool
-compat pi rh = rh == Any || pi == rh
-
-
-public export
-interface IsQty q where
-  zero, one : q
-  (+),  (*) : q -> q -> q
-  (<=.)     : q -> q -> Bool
-
-public export
-IsQty Qty where
-  zero  = Zero; one = One
-  (+)   = plus; (*) = times
-  (<=.) = compat
+(<=.) : Qty -> Qty -> Bool
+pi <=. rh = rh == Any || pi == rh
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index 5e23ebe..471f13f 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -172,35 +172,3 @@ prettyShift bnd by =
 
 ||| prints using the `TVar` highlight for variables
 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
-  (//) : f from -> Shift from to -> f to
-
-export CanShift Var where i // by = shift by i
diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index 47f0b8c..34b5b34 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -1,6 +1,6 @@
 module Quox.Syntax.Subst
 
-import public Quox.Syntax.Shift
+import Quox.Syntax.Shift
 import Quox.Syntax.Var
 import Quox.Name
 import Quox.Pretty
@@ -35,7 +35,7 @@ export Ord (f to) => Ord (Subst f from to) where compare = compare `on` repr
 infixl 8 //
 public export
 interface FromVar env => CanSubst env term where
-  (//) : term from -> Lazy (Subst env from to) -> term to
+  (//) : term from -> Subst env from to -> term to
 
 public export
 CanSubst1 : (Nat -> Type) -> Type
@@ -84,11 +84,6 @@ public export %inline
 push : CanSubst1 f => Subst f from to -> Subst f (S from) (S to)
 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 (t ::: th) = th
-
 
 ||| `prettySubst pr bnd op cl unicode th` pretty-prints the substitution `th`,
 ||| with the following arguments:
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 00a5836..3c0c576 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -187,12 +187,11 @@ export FromVar (Term d) where fromVar = E . fromVar
 ||| - otherwise, wraps in a new closure
 export
 CanSubst (Elim d) (Elim d) where
-  F x       // _  = F x
-  B i       // th = th !! i
-  CloE e ph // th = assert_total CloE e $ ph . th
-  e         // th = case force th of
-                         Shift SZ => e
-                         th       => CloE e th
+  F x       // _        = F x
+  B i       // th       = th !! i
+  CloE e ph // th       = CloE e $ assert_total $ ph . th
+  e         // Shift SZ = e
+  e         // th       = CloE e th
 
 ||| does the minimal reasonable work:
 ||| - deletes the closure around an atomic constant like `TYPE`
@@ -202,18 +201,11 @@ CanSubst (Elim d) (Elim d) where
 ||| - otherwise, wraps in a new closure
 export
 CanSubst (Elim d) (Term d) where
-  TYPE l    // _  = TYPE l
-  E e       // th = E $ e // th
-  CloT s ph // th = CloT s $ ph . th
-  s         // th = case force th of
-                         Shift SZ => s
-                         th       => CloT s th
-
-export CanSubst Var (Term d) where s // th = s // map (B {d}) th
-export CanSubst Var (Elim d) where e // th = e // map (B {d}) th
-
-export CanShift (Term d) where i // by = i // Shift by {env=(Elim d)}
-export CanShift (Elim d) where i // by = i // Shift by {env=(Elim d)}
+  TYPE l    // _        = TYPE l
+  E e       // th       = E $ e // th
+  CloT s ph // th       = CloT s $ ph . th
+  s         // Shift SZ = s
+  s         // th       = CloT s th
 
 
 infixl 8 ///
@@ -261,27 +253,27 @@ comp' th ps ph = map (/// th) ps . ph
 
 ||| true if an elimination has a closure or dimension closure at the top level
 public export %inline
-topCloE : Elim d n -> Bool
-topCloE (CloE  _ _) = True
-topCloE (DCloE _ _) = True
-topCloE _           = False
+isCloE : Elim d n -> Bool
+isCloE (CloE  _ _) = True
+isCloE (DCloE _ _) = True
+isCloE _           = False
 
 ||| true if a term has a closure or dimension closure at the top level,
 ||| or is `E` applied to such an elimination
 public export %inline
-topCloT : Term d n -> Bool
-topCloT (CloT  _ _) = True
-topCloT (DCloT _ _) = True
-topCloT (E e)       = topCloE e
-topCloT _           = False
+isCloT : Term d n -> Bool
+isCloT (CloT  _ _) = True
+isCloT (DCloT _ _) = True
+isCloT (E e)       = isCloE e
+isCloT _           = False
 
 ||| an elimination which is not a top level closure
 public export NotCloElim : Nat -> Nat -> Type
-NotCloElim d n = Subset (Elim d n) $ So . not . topCloE
+NotCloElim d n = Subset (Elim d n) $ So . not . isCloE
 
 ||| a term which is not a top level closure
 public export NotCloTerm : Nat -> Nat -> Type
-NotCloTerm d n = Subset (Term d n) $ So . not . topCloT
+NotCloTerm d n = Subset (Term d n) $ So . not . isCloT
 
 
 mutual