diff --git a/src/Quox/Ctx.idr b/src/Quox/Ctx.idr
new file mode 100644
index 0000000..56a2991
--- /dev/null
+++ b/src/Quox/Ctx.idr
@@ -0,0 +1,98 @@
+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/Name.idr b/src/Quox/Name.idr
index f8ed93f..c432667 100644
--- a/src/Quox/Name.idr
+++ b/src/Quox/Name.idr
@@ -9,7 +9,7 @@ public export
 data BaseName =
     UN String -- user-given name
 
-private BRepr : Type
+private 0 BRepr : Type
 BRepr = String
 
 private %inline brepr : BaseName -> BRepr
@@ -33,7 +33,7 @@ record Name where
   mods : SnocList String
   base : BaseName
 
-private Repr : Type
+private 0 Repr : Type
 Repr = (SnocList String, BRepr)
 
 private %inline repr : Name -> Repr
diff --git a/src/Quox/Pretty.idr b/src/Quox/Pretty.idr
index a9296ba..e44d334 100644
--- a/src/Quox/Pretty.idr
+++ b/src/Quox/Pretty.idr
@@ -26,7 +26,7 @@ data HL
   | Free
   | Syntax
 
-private HLRepr : Type
+private 0 HLRepr : Type
 HLRepr = Nat
 
 private %inline hlRepr : HL -> Nat
@@ -54,7 +54,7 @@ data PPrec
   | SApp -- substitution application
   | Arg
 
-private PrecRepr : Type
+private 0 PrecRepr : Type
 PrecRepr = Nat
 
 private %inline precRepr : PPrec -> PrecRepr
@@ -109,16 +109,16 @@ record PrettyEnv where
   ||| surrounding precedence level
   prec    : PPrec
 
-public export %inline HasEnv : (Type -> Type) -> Type
+public export %inline 0 HasEnv : (Type -> Type) -> Type
 HasEnv = MonadReader PrettyEnv
 
 export
 ifUnicode : HasEnv m => (uni, asc : Lazy a) -> m a
-ifUnicode uni asc = if (!ask).unicode then [|uni|] else [|asc|]
+ifUnicode uni asc = if unicode !ask then [|uni|] else [|asc|]
 
 export
 parensIfM : HasEnv m => PPrec -> Doc HL -> m (Doc HL)
-parensIfM d doc = pure $ parensIf ((!ask).prec > d) doc
+parensIfM d doc = pure $ parensIf (prec !ask > d) doc
 
 export
 withPrec : HasEnv m => PPrec -> m a -> m a
@@ -137,11 +137,11 @@ public export
 interface PrettyHL a where
   prettyM : HasEnv m => a -> m (Doc HL)
 
-export %inline
+public export %inline
 pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL)
 pretty0M = local {prec := Outer} . prettyM
 
-export %inline
+public export %inline
 pretty0 : PrettyHL a => {default True unicode : Bool} -> a -> Doc HL
 pretty0 x {unicode} =
   let env = MakePrettyEnv {dnames = [], tnames = [], unicode, prec = Outer} in
@@ -164,8 +164,9 @@ export PrettyHL Name     where prettyM = pure . pretty . toDots
 export
 prettyStr : PrettyHL a => {default True unicode : Bool} -> a -> String
 prettyStr {unicode} =
-  let layout = layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) in
-  renderString . layout . pretty0 {unicode}
+  renderString .
+  layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) .
+  pretty0 {unicode}
 
 
 export
diff --git a/src/Quox/Syntax/Dim.idr b/src/Quox/Syntax/Dim.idr
index e58e98d..cba8b2e 100644
--- a/src/Quox/Syntax/Dim.idr
+++ b/src/Quox/Syntax/Dim.idr
@@ -30,14 +30,14 @@ PrettyHL (Dim n) where
 
 
 public export
-DSubst : Nat -> Nat -> Type
+0 DSubst : Nat -> Nat -> Type
 DSubst = Subst Dim
 
 
 export %inline
 prettyDSubst : Pretty.HasEnv m => DSubst from to -> m (Doc HL)
 prettyDSubst th =
-  prettySubstM prettyM (!ask).dnames DVar
+  prettySubstM prettyM (dnames !ask) DVar
     !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
 
 
diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr
index 90c0783..4689d2d 100644
--- a/src/Quox/Syntax/Qty.idr
+++ b/src/Quox/Syntax/Qty.idr
@@ -6,14 +6,14 @@ import Data.Fin
 
 
 public export
-data Qty = Zero | One | Any
+data Qty = Zero | One | Many
 %name Qty.Qty pi, rh
 
 private Repr : Type
 Repr = Fin 3
 
 private %inline repr : Qty -> Repr
-repr pi = case pi of Zero => 0; One => 1; Any => 2
+repr pi = case pi of Zero => 0; One => 1; Many => 2
 
 export Eq  Qty where (==) = (==) `on` repr
 export Ord Qty where compare = compare `on` repr
@@ -25,7 +25,7 @@ PrettyHL Qty where
     case pi of
       Zero => ifUnicode "𝟬" "0"
       One  => ifUnicode "𝟭" "1"
-      Any  => ifUnicode "𝛚" "*"
+      Many => ifUnicode "𝛚" "*"
 
 export %inline
 prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL)
@@ -38,7 +38,7 @@ public export
 (+) : Qty -> Qty -> Qty
 Zero + rh   = rh
 pi   + Zero = pi
-_    + _    = Any
+_    + _    = Many
 
 public export
 (*) : Qty -> Qty -> Qty
@@ -46,9 +46,9 @@ Zero * _    = Zero
 _    * Zero = Zero
 One  * rh   = rh
 pi   * One  = pi
-Any  * Any  = Any
+Many * Many = Many
 
 infix 6 <=.
 public export
 (<=.) : Qty -> Qty -> Bool
-pi <=. rh = rh == Any || pi == rh
+pi <=. rh = rh == Many || pi == rh
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index 471f13f..dfee608 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -49,7 +49,7 @@ toEqv Refl {by = SZ}      = EqSZ
 toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl {by}
 
 
-export
+public export
 0 shiftDiff : (by : Shift from to) -> to = by.nat + from
 shiftDiff SZ      = Refl
 shiftDiff (SS by) = cong S $ shiftDiff by
diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index 34b5b34..497d6cc 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -38,7 +38,7 @@ interface FromVar env => CanSubst env term where
   (//) : term from -> Subst env from to -> term to
 
 public export
-CanSubst1 : (Nat -> Type) -> Type
+0 CanSubst1 : (Nat -> Type) -> Type
 CanSubst1 f = CanSubst f f
 
 
@@ -52,7 +52,7 @@ public export
 
 public export
 CanSubst Var Var where
-  i    // Shift by   = shift by i
+  i    // Shift by     = shift by i
   VZ   // (t ::: th) = t
   VS i // (t ::: th) = i // th
 
@@ -118,4 +118,4 @@ prettySubstM pr names bnd op cl th =
 ||| prints with [square brackets] and the `TVar` highlight for variables
 export
 PrettyHL (f to) => PrettyHL (Subst f from to) where
-  prettyM th = prettySubstM prettyM (!ask).tnames TVar "[" "]" th
+  prettyM th = prettySubstM prettyM (tnames !ask) TVar "[" "]" th
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 3c0c576..8a6ab99 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -1,5 +1,6 @@
 module Quox.Syntax.Term
 
+import public Quox.Ctx
 import public Quox.Syntax.Var
 import public Quox.Syntax.Shift
 import public Quox.Syntax.Subst
@@ -24,8 +25,8 @@ infixl 8 :#
 infixl 9 :@
 mutual
   public export
-  TSubst : Nat -> Nat -> Nat -> Type
-  TSubst d = Subst (\n => Elim d n)
+  0 TSubst : Nat -> Nat -> Nat -> Type
+  TSubst d = Subst (Elim d)
 
   ||| first argument `d` is dimension scope size, second `n` is term scope size
   public export
@@ -35,17 +36,17 @@ mutual
 
     ||| function type
     Pi  : (qty, qtm : Qty) -> (x : Name) ->
-          (arg : Term d n) -> (res : Term d (S n)) -> Term d n
+          (a : Term d n) -> (b : Term d (S n)) -> Term d n
     ||| function term
-    Lam : (x : Name) -> (body : Term d (S n)) -> Term d n
+    Lam : (x : Name) -> (t : Term d (S n)) -> Term d n
 
     ||| elimination
     E : (e : Elim d n) -> Term d n
 
     ||| term closure/suspended substitution
-    CloT  : (tm : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
+    CloT  : (s : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
     ||| dimension closure/suspended substitution
-    DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
+    DCloT : (s : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
 
   ||| first argument `d` is dimension scope size, second `n` is term scope size
   public export
@@ -56,15 +57,15 @@ mutual
     B : (i : Var n) -> Elim d n
 
     ||| term application
-    (:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
+    (:@) : (f : Elim d n) -> (s : Term d n) -> Elim d n
 
     ||| type-annotated term
-    (:#) : (tm, ty : Term d n) -> Elim d n
+    (:#) : (s, a : Term d n) -> Elim d n
 
     ||| term closure/suspended substitution
-    CloE  : (el : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
+    CloE  : (e : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
     ||| dimension closure/suspended substitution
-    DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
+    DCloE : (e : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
 
 %name Term s, t, r
 %name Elim e, f
@@ -166,7 +167,7 @@ mutual
 
   export covering
   prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
-  prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
+  prettyTSubst s = prettySubstM prettyM (tnames !ask) TVar "[" "]" s
 
   export covering
   prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
@@ -268,23 +269,19 @@ isCloT (E e)       = isCloE e
 isCloT _           = False
 
 ||| an elimination which is not a top level closure
-public export NotCloElim : Nat -> Nat -> Type
+public export 0 NotCloElim : Nat -> Nat -> Type
 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
+public export 0 NotCloTerm : Nat -> Nat -> Type
 NotCloTerm d n = Subset (Term d n) $ So . not . isCloT
 
 
 mutual
-  ||| if the input term has any top-level closures, push them under one layer of
-  ||| syntax
   export
   pushSubstsT : Term d n -> NotCloTerm d n
   pushSubstsT s = pushSubstsT' id id s
 
-  ||| if the input elimination has any top-level closures, push them under one
-  ||| layer of syntax
   export
   pushSubstsE : Elim d n -> NotCloElim d n
   pushSubstsE e = pushSubstsE' id id e
@@ -299,7 +296,7 @@ mutual
   pushSubstsT' th ph (Lam x t) =
     Element (Lam x $ subs t th $ push ph) Oh
   pushSubstsT' th ph (E e) =
-    let Element e prf = pushSubstsE' th ph e in Element (E e) prf
+    case pushSubstsE' th ph e of Element e' prf => Element (E e') prf
   pushSubstsT' th ph (CloT  s ps) =
     pushSubstsT' th (comp' th ps ph) s
   pushSubstsT' th ph (DCloT s ps) =
@@ -323,11 +320,11 @@ mutual
 
 
 parameters {auto _ : Alternative f}
-  ||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)]`
+  ||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)`
   export
   betaLam1 : Elim d n -> f (Elim d n)
-  betaLam1 ((Lam {body, _} :# Pi {arg, res, _}) :@ s) =
-    pure $ (body :# res) // (s :# arg ::: id)
+  betaLam1 ((Lam {t, _} :# Pi {a, b, _}) :@ s) =
+    pure $ (t :# b) // (s :# a ::: id)
   betaLam1 _ = empty
 
   ||| `(e ⦂ A) >>> e`    [if `e` is an elim]
@@ -336,10 +333,10 @@ parameters {auto _ : Alternative f}
   upsilon1 (E e :# _) = pure e
   upsilon1 _          = empty
 
-  export
+  public export
   step : Elim d n -> f (Elim d n)
   step e = betaLam1 e <|> upsilon1 e
 
-export
+public export
 step' : Elim d n -> Elim d n
 step' e = fromMaybe e $ step e
diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index ca5747b..513a057 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -68,7 +68,7 @@ public export %inline
 V : (i : Nat) -> {auto 0 p : i `LT` n} -> Var n
 V i {p} = fromNatWith i p
 
-export %inline
+public export %inline
 tryFromNat : Alternative f => (n : Nat) -> Nat -> f (Var n)
 tryFromNat n i =
   case i `isLT` n of
@@ -99,6 +99,14 @@ toFromNat 0     (LTESucc x) = Refl
 toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
 
 
+public export
+(.int) : Var n -> Integer
+i.int = natToInteger i.nat
+%builtin NaturalToInteger Var.(.int)
+
+public export Cast (Var n) Integer where cast i = i.int
+
+
 -- not using %transform like other things because weakSpec requires the proof
 -- to be relevant. but since only `LTESucc` is ever possible that seems
 -- to be a bug?