diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index dc66a8b..65e5328 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -169,14 +169,14 @@ zipWith3Lazy : forall tm1, tm2, tm3, tm4.
                Telescope tm2 from to ->
                Telescope tm3 from to ->
                Telescope (\n => Lazy (tm4 n)) from to
-zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
+zipWith3Lazy f = zipWith3 (\x, y, z => delay $ f x y z)
 
 
 export
-lengthPrf : Telescope _ from to -> Subset Nat $ \len => len + from = to
+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)
+lengthPrf (tel :< _) =
+  let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
 
 public export %inline
 length : Telescope {} -> Nat
@@ -196,40 +196,40 @@ parameters {auto _ : Monoid a}
   foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
 
   export %inline
-  fold : Telescope' a from to -> a
+  fold : Telescope (\x => a) from to -> a
   fold = foldMap id
 
   ||| like `fold` but calculate the elements only when actually appending
   export %inline
-  foldLazy : Telescope' (Lazy a) from to -> a
+  foldLazy : Telescope (\x => Lazy a) from to -> a
   foldLazy = foldMap force
 
 
 export %inline
-and : Telescope' (Lazy Bool) _ _ -> Bool
+and : Telescope' (Lazy Bool) from to -> Bool
 and = force . fold @{All}
 
 export %inline
-all : (forall n. tm n -> Bool) -> Telescope tm _ _ -> Bool
+all : (forall n. f n -> Bool) -> Telescope f from to -> Bool
 all p = and . map (delay . p)
 
 export %inline
-all2 : (forall n. tm n -> tm2 n -> Bool) ->
-       Telescope tm from to -> Telescope tm2 from to -> Bool
+all2 : (forall n. f n -> g n -> Bool) ->
+       Telescope f from to -> Telescope g from to -> Bool
 all2 p = and .: zipWithLazy p
 
 
 export %inline
-or : Telescope' (Lazy Bool) _ _ -> Bool
+or : Telescope' (Lazy Bool) from to -> Bool
 or = force . fold @{Any}
 
 export %inline
-any : (forall n. tm n -> Bool) -> Telescope tm _ _ -> Bool
+any : (forall n. f n -> Bool) -> Telescope f from to -> Bool
 any p = or . map (delay . p)
 
 export %inline
-any2 : (forall n. tm1 n -> tm2 n -> Bool) ->
-       Telescope tm1 from to -> Telescope tm2 from to -> Bool
+any2 : (forall n. f n -> g n -> Bool) ->
+       Telescope f from to -> Telescope g from to -> Bool
 any2 p = or .: zipWithLazy p
 
 
diff --git a/src/Quox/Error.idr b/src/Quox/Error.idr
index bbe8b0f..a78cabb 100644
--- a/src/Quox/Error.idr
+++ b/src/Quox/Error.idr
@@ -1,7 +1,5 @@
 module Quox.Error
 
-import Data.List.Elem
-
 import Control.Monad.Identity
 import Control.Monad.Trans
 import Control.Monad.Reader
@@ -12,6 +10,20 @@ import Control.Monad.RWS
 %default total
 
 
+||| a proof that an element is in a list. unlike the standard library one, this
+||| is represented as a single number at runtime.
+public export
+data Elem : a -> List a -> Type where
+  Here  : x `Elem` (x :: xs)
+  There : x `Elem` xs -> x `Elem` (y :: xs)
+%builtin Natural Elem
+
+export
+Uninhabited (x `Elem` []) where
+  uninhabited Here      impossible
+  uninhabited (There _) impossible
+
+
 ||| a representation of a list's length. this is used in the `Ord` instance to
 ||| transform the `Ord` constraints into `Eq`s
 public export
@@ -28,8 +40,6 @@ record OneOf types where
   constructor One
   elem    : type `Elem` types
   1 value : type
--- this is basically the same as Data.OpenUnion, but using Elem instead of
--- AtIndex is much easier for some stuff here e.g. `get`
 
 export
 Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem
diff --git a/src/Quox/Eval.idr b/src/Quox/Eval.idr
index 0e3e878..e026814 100644
--- a/src/Quox/Eval.idr
+++ b/src/Quox/Eval.idr
@@ -15,6 +15,30 @@ import Data.SortedMap
 %default total
 
 
+public export Exists2 : (ty1 -> ty2 -> Type) -> Type
+Exists2 t = Exists (\a => Exists (\b => t a b))
+
+parameters {0 t : ty -> Type}
+  private %inline some : t a -> Exists t
+  some t = Evidence _ t
+
+parameters {0 t : ty1 -> ty2 -> Type}
+  private %inline some2 : t a b -> Exists2 t
+  some2 t = some $ some t
+
+||| A term of some unknown scope sizes.
+public export SomeTerm : Type
+SomeTerm = Exists2 Term
+
+||| An elimination of some unknown scope sizes.
+public export SomeElim : Type
+SomeElim = Exists2 Elim
+
+||| A dimension of some unknown scope size.
+public export SomeDim : Type
+SomeDim = Exists Dim
+
+
 public export
 record Global where
   constructor G
diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index 6035633..2658e0a 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -90,14 +90,16 @@ drop1 (Shift by) = Shift $ drop1 by
 drop1 (t ::: th) = th
 
 
-||| `prettySubst pr names bnd op cl th` pretty-prints the substitution `th`,
+||| `prettySubst pr bnd op cl unicode th` pretty-prints the substitution `th`,
 ||| with the following arguments:
 |||
 ||| * `th : Subst f from to`
-||| * `pr : f to -> m (Doc HL)` prints a single element
+||| * `pr : (unicode : Bool) -> f to -> m (Doc HL)` prints a single element
 ||| * `names : List Name` is a list of known bound var names
 ||| * `bnd : HL` is the highlight to use for bound variables being subsituted
 ||| * `op, cl : Doc HL` are the opening and closing brackets
+||| * `unicode : Bool` is whether to use unicode characters in the output
+|||   (also passed into `pr`)
 export
 prettySubstM : Pretty.HasEnv m =>
                (pr : f to -> m (Doc HL)) ->
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index b1441c5..d10d41d 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -368,27 +368,3 @@ parameters {auto _ : Alternative f}
 export
 step' : Elim d n -> Elim d n
 step' e = fromMaybe e $ step e
-
-
-public export Exists2 : (ty1 -> ty2 -> Type) -> Type
-Exists2 t = Exists (\a => Exists (\b => t a b))
-
-parameters {0 t : ty -> Type}
-  public export %inline some : t a -> Exists t
-  some t = Evidence _ t
-
-parameters {0 t : ty1 -> ty2 -> Type}
-  public export %inline some2 : t a b -> Exists2 t
-  some2 t = some $ some t
-
-||| A term of some unknown scope sizes.
-public export SomeTerm : Type
-SomeTerm = Exists2 Term
-
-||| An elimination of some unknown scope sizes.
-public export SomeElim : Type
-SomeElim = Exists2 Elim
-
-||| A dimension of some unknown scope size.
-public export SomeDim : Type
-SomeDim = Exists Dim