diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index 0a923b3..91b3fcd 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -109,10 +109,17 @@ fromSnocVect [<]       = [<]
 fromSnocVect (sx :< x) = fromSnocVect sx :< x
 
 
+public export
+tabulateLT : (n : Nat) -> ((i : Nat) -> (0 p : i `LT` n) => tm i) ->
+             Context tm n
+tabulateLT 0     f = [<]
+tabulateLT (S k) f =
+  tabulateLT k (\i => f i @{lteSuccRight %search}) :< f k @{reflexive}
+
 public export
 tabulate : ((n : Nat) -> tm n) -> (n : Nat) -> Context tm n
-tabulate f 0     = [<]
-tabulate f (S k) = tabulate f k :< f k
+tabulate f n = tabulateLT n (\i => f i)
+-- [todo] fixup argument order lol
 
 public export
 replicate : (n : Nat) -> a -> Context' a n
@@ -182,6 +189,12 @@ export %hint
 succGT = LTESucc reflexive
 
 
+public export
+drop : (m : Nat) -> Context term (m + n) -> Context term n
+drop 0     ctx        = ctx
+drop (S m) (ctx :< _) = drop m ctx
+
+
 parameters {auto _ : Applicative f}
   export
   traverse : (forall n. tm1 n -> f (tm2 n)) ->
@@ -260,16 +273,17 @@ unzip3 (tel :< (x, y, z)) =
 
 
 public export
-lengthPrf : Telescope _ from to -> (len ** len + from = to)
-lengthPrf [<]        = (0 ** Refl)
+lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
+lengthPrf [<]        = Element 0 Refl
 lengthPrf (tel :< _) =
-  let len = lengthPrf tel in (S len.fst ** cong S len.snd)
+  let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
 
 export
-lengthPrf0 : Context _ to -> (len ** len = to)
+lengthPrf0 : Context _ to -> Singleton to
 lengthPrf0 ctx =
-  let len = lengthPrf ctx in
-  (len.fst ** rewrite sym $ plusZeroRightNeutral len.fst in len.snd)
+  let Element len prf = lengthPrf ctx in
+  rewrite sym prf `trans` plusZeroRightNeutral len in
+  [|len|]
 
 public export %inline
 length : Telescope {} -> Nat
@@ -288,6 +302,10 @@ foldl : {0 acc : Nat -> Type} ->
 foldl f z [<]        = z
 foldl f z (tel :< t) = f (foldl f z tel) (rewrite (lengthPrf tel).snd in t)
 
+export %inline
+foldl_ : (acc -> tm -> acc) -> acc -> Telescope' tm from to -> acc
+foldl_ f z tel = foldl f z tel
+
 export %inline
 foldMap : Monoid a => (forall n. tm n -> a) -> Telescope tm from to -> a
 foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index ea54e4f..82e7b22 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -4,6 +4,7 @@ import Quox.BoolExtra
 import public Quox.Typing
 import Data.Maybe
 import Quox.EffExtra
+import Quox.FreeVars
 
 %default total
 
@@ -673,9 +674,12 @@ parameters (loc : Loc) (ctx : TyContext d n)
     fromInner = lift . map fst . runState mode
 
     private
-    eachFace : Applicative f => (EqContext n -> DSubst d 0 -> f ()) -> f ()
-    eachFace act =
-      for_ (splits loc ctx.dctx) $ \th => act (makeEqContext ctx th) th
+    eachFace : Applicative f => FreeVars d ->
+               (EqContext n -> DSubst d 0 -> f ()) -> f ()
+    eachFace fvs act =
+      let Val d = ctx.dimLen in
+      for_ (splits loc ctx.dctx fvs) $ \th =>
+        act (makeEqContext ctx th) th
 
     private
     CompareAction : Nat -> Nat -> Type
@@ -683,18 +687,23 @@ parameters (loc : Loc) (ctx : TyContext d n)
       Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner ()
 
     private
-    runCompare : CompareAction d n -> Eff Equal ()
-    runCompare act = fromInner $ eachFace $ act !(askAt DEFS)
+    runCompare : FreeVars d -> CompareAction d n -> Eff Equal ()
+    runCompare fvs act = fromInner $ eachFace fvs $ act !(askAt DEFS)
+
+    private
+    fdvAll : HasFreeDVars t => List (t d n) -> FreeVars d
+    fdvAll ts =
+      let Val d = ctx.dimLen; Val n = ctx.termLen in foldMap fdv ts
 
     namespace Term
       export covering
       compare : (ty, s, t : Term d n) -> Eff Equal ()
-      compare ty s t = runCompare $ \defs, ectx, th =>
+      compare ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th =>
         compare0 defs ectx (ty // th) (s // th) (t // th)
 
       export covering
       compareType : (s, t : Term d n) -> Eff Equal ()
-      compareType s t = runCompare $ \defs, ectx, th =>
+      compareType s t = runCompare (fdvAll [s, t]) $ \defs, ectx, th =>
         compareType defs ectx (s // th) (t // th)
 
     namespace Elim
@@ -702,7 +711,7 @@ parameters (loc : Loc) (ctx : TyContext d n)
       ||| of the same type!!
       export covering
       compare : (e, f : Elim d n) -> Eff Equal ()
-      compare e f = runCompare $ \defs, ectx, th =>
+      compare e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th =>
         ignore $ compare0 defs ectx (e // th) (f // th)
 
   namespace Term
diff --git a/lib/Quox/FreeVars.idr b/lib/Quox/FreeVars.idr
new file mode 100644
index 0000000..acff6ae
--- /dev/null
+++ b/lib/Quox/FreeVars.idr
@@ -0,0 +1,280 @@
+module Quox.FreeVars
+
+import Quox.Syntax.Term.Base
+import Data.Maybe
+import Data.Nat
+import Data.Singleton
+import Data.SortedSet
+
+
+public export
+record FreeVars n where
+  constructor FV
+  vars : Context' Bool n
+
+
+export %inline
+(||) : FreeVars n -> FreeVars n -> FreeVars n
+FV s || FV t = FV $ zipWith (\x, y => x || y) s t
+
+export %inline
+(&&) : FreeVars n -> FreeVars n -> FreeVars n
+FV s && FV t = FV $ zipWith (\x, y => x && y) s t
+
+export %inline Semigroup (FreeVars n) where (<+>) = (||)
+
+export %inline [AndS] Semigroup (FreeVars n) where (<+>) = (&&)
+
+export
+only : {n : Nat} -> Var n -> FreeVars n
+only i = FV $ only' i where
+  only' : {n' : Nat} -> Var n' -> Context' Bool n'
+  only' VZ     = replicate (pred n') False :< True
+  only' (VS i) = only' i :< False
+
+export %inline
+all : {n : Nat} -> FreeVars n
+all = FV $ replicate n True
+
+export %inline
+none : {n : Nat} -> FreeVars n
+none = FV $ replicate n False
+
+
+export %inline
+uncons : FreeVars (S n) -> (FreeVars n, Bool)
+uncons (FV (xs :< x)) = (FV xs, x)
+
+
+export %inline {n : Nat} -> Monoid (FreeVars n) where neutral = none
+export %inline [AndM] {n : Nat} -> Monoid (FreeVars n) where neutral = all
+
+
+private
+self : {n : Nat} -> Context' (FreeVars n) n
+self = tabulate (\i => FV $ tabulate (== i) n) n
+
+export
+shift : forall from, to. Shift from to -> FreeVars from -> FreeVars to
+shift by (FV xs) = FV $ shift' by xs where
+  shift' : Shift from' to' -> Context' Bool from' -> Context' Bool to'
+  shift' SZ      ctx = ctx
+  shift' (SS by) ctx = shift' by ctx :< False
+
+
+export
+fromSet : {n : Nat} -> SortedSet (Var n) -> FreeVars n
+fromSet vs = FV $ tabulateLT n $ \i => contains (V i) vs
+
+export
+toSet : {n : Nat} -> FreeVars n -> SortedSet (Var n)
+toSet (FV vs) =
+  foldl_ (\s, i => maybe s (\i => insert i s) i) empty $
+  zipWith (\i, b => guard b $> i) (tabulateLT n V) vs
+
+
+public export
+interface HasFreeVars (0 term : Nat -> Type) where
+  constructor HFV
+  fv : {n : Nat} -> term n -> FreeVars n
+
+public export
+interface HasFreeDVars (0 term : TermLike) where
+  constructor HFDV
+  fdv : {d, n : Nat} -> term d n -> FreeVars d
+
+export
+Fdv : (0 term : TermLike) -> {n : Nat} ->
+      HasFreeDVars term => HasFreeVars (\d => term d n)
+Fdv term @{HFDV fdv} = HFV fdv
+
+
+export
+fvEach : {n1, n2 : Nat} -> HasFreeVars env =>
+         Subst env n1 n2 -> Context' (Lazy (FreeVars n2)) n1
+fvEach (Shift by) = map (delay . shift by) self
+fvEach (t ::: th) = fvEach th :< fv t
+
+export
+fdvEach : {d, n1, n2 : Nat} -> HasFreeDVars env =>
+          Subst (env d) n1 n2 -> Context' (Lazy (FreeVars d)) n1
+fdvEach (Shift by) = replicate n1 none
+fdvEach (t ::: th) = fdvEach th :< fdv t
+
+
+export
+HasFreeVars Dim where
+  fv (K _ _) = none
+  fv (B i _) = only i
+
+
+export
+{s : Nat} -> HasFreeVars term => HasFreeVars (Scoped s term) where
+  fv (S _ (Y body)) = FV $ drop s (fv body).vars
+  fv (S _ (N body)) = fv body
+
+export
+implementation [DScope]
+  {s : Nat} -> HasFreeDVars term =>
+  HasFreeDVars (\d, n => Scoped s (\d' => term d' n) d)
+where
+  fdv (S _ (Y body)) = FV $ drop s (fdv body).vars
+  fdv (S _ (N body)) = fdv body
+
+export
+fvD : {0 term : TermLike} -> {n : Nat} -> (forall d. HasFreeVars (term d)) =>
+      Scoped s (\d => term d n) d -> FreeVars n
+fvD (S _ (Y body)) = fv body
+fvD (S _ (N body)) = fv body
+
+export
+fdvT : HasFreeDVars term => {s, d, n : Nat} -> Scoped s (term d) n -> FreeVars d
+fdvT (S _ (Y body)) = fdv body
+fdvT (S _ (N body)) = fdv body
+
+
+private
+guardM : Monoid a => Bool -> Lazy a -> a
+guardM b x = if b then x else neutral
+
+export
+implementation
+  (HasFreeVars term, HasFreeVars env) =>
+  HasFreeVars (WithSubst term env)
+where
+  fv (Sub term subst) =
+    let Val from = getFrom subst in
+    foldMap (uncurry guardM) $ zipWith (,) (fv term).vars (fvEach subst)
+
+export
+implementation [WithSubst]
+  ((forall d. HasFreeVars (term d)), HasFreeDVars term, HasFreeDVars env) =>
+  HasFreeDVars (\d => WithSubst (term d) (env d))
+where
+  fdv (Sub term subst) =
+    let Val from = getFrom subst in
+    fdv term <+>
+    foldMap (uncurry guardM) (zipWith (,) (fv term).vars (fdvEach subst))
+
+
+export HasFreeVars (Term d)
+export HasFreeVars (Elim d)
+
+export
+HasFreeVars (Term d) where
+  fv (TYPE  {})            = none
+  fv (Pi    {arg, res, _}) = fv arg <+> fv res
+  fv (Lam   {body, _})     = fv body
+  fv (Sig   {fst, snd, _}) = fv fst <+> fv snd
+  fv (Pair  {fst, snd, _}) = fv fst <+> fv snd
+  fv (Enum  {})            = none
+  fv (Tag   {})            = none
+  fv (Eq    {ty, l, r, _}) = fvD ty <+> fv l <+> fv r
+  fv (DLam  {body, _})     = fvD body
+  fv (Nat   {})            = none
+  fv (Zero  {})            = none
+  fv (Succ  {p, _})        = fv p
+  fv (BOX   {ty, _})       = fv ty
+  fv (Box   {val, _})      = fv val
+  fv (E     e)             = fv e
+  fv (CloT  s)             = fv s
+  fv (DCloT s)             = fv s.term
+
+export
+HasFreeVars (Elim d) where
+  fv (F {}) = none
+  fv (B i _) = only i
+  fv (App {fun, arg, _}) = fv fun <+> fv arg
+  fv (CasePair {pair, ret, body, _}) = fv pair <+> fv ret <+> fv body
+  fv (CaseEnum {tag, ret, arms, _}) =
+    fv tag <+> fv ret <+> foldMap fv (values arms)
+  fv (CaseNat {nat, ret, zero, succ, _}) =
+    fv nat <+> fv ret <+> fv zero <+> fv succ
+  fv (CaseBox {box, ret, body, _}) =
+    fv box <+> fv ret <+> fv body
+  fv (DApp {fun, _}) = fv fun
+  fv (Ann {tm, ty, _}) = fv tm <+> fv ty
+  fv (Coe {ty, val, _}) = fvD ty <+> fv val
+  fv (Comp {ty, val, zero, one, _}) =
+    fv ty <+> fv val <+> fvD zero <+> fvD one
+  fv (TypeCase {ty, ret, arms, def, _}) =
+    fv ty <+> fv ret <+> fv def <+> foldMap (\x => fv x.snd) (toList arms)
+  fv (CloE s) = fv s
+  fv (DCloE s) = fv s.term
+
+
+
+private
+expandDShift : {d1 : Nat} -> Shift d1 d2 -> Context' (Dim d2) d1
+expandDShift by = tabulateLT d1 (\i => BV i noLoc // by)
+
+private
+expandDSubst : {d1 : Nat} -> DSubst d1 d2 -> Context' (Dim d2) d1
+expandDSubst (Shift by) = expandDShift by
+expandDSubst (t ::: th) = expandDSubst th :< t
+
+
+private
+fdvSubst' : {d1, d2, n : Nat} -> HasFreeDVars term =>
+            term d1 n -> DSubst d1 d2 -> FreeVars d2
+fdvSubst' t th =
+  fold $ zipWith maybeOnly (fdv t).vars (expandDSubst th)
+where
+  maybeOnly : {d : Nat} -> Bool -> Dim d -> FreeVars d
+  maybeOnly True (B i _) = only i
+  maybeOnly _    _       = none
+
+private
+fdvSubst : {d, n : Nat} -> HasFreeDVars term =>
+           WithSubst (\d => term d n) Dim d -> FreeVars d
+fdvSubst (Sub t th) = let Val from = getFrom th in fdvSubst' t th
+
+
+export HasFreeDVars Term
+export HasFreeDVars Elim
+
+export
+HasFreeDVars Term where
+  fdv (TYPE  {})            = none
+  fdv (Pi    {arg, res, _}) = fdv arg <+> fdvT res
+  fdv (Lam   {body, _})     = fdvT body
+  fdv (Sig   {fst, snd, _}) = fdv fst <+> fdvT snd
+  fdv (Pair  {fst, snd, _}) = fdv fst <+> fdv snd
+  fdv (Enum  {})            = none
+  fdv (Tag   {})            = none
+  fdv (Eq    {ty, l, r, _}) = fdv @{DScope} ty <+> fdv l <+> fdv r
+  fdv (DLam  {body, _})     = fdv @{DScope} body
+  fdv (Nat   {})            = none
+  fdv (Zero  {})            = none
+  fdv (Succ  {p, _})        = fdv p
+  fdv (BOX   {ty, _})       = fdv ty
+  fdv (Box   {val, _})      = fdv val
+  fdv (E     e)             = fdv e
+  fdv (CloT  s)             = fdv s @{WithSubst}
+  fdv (DCloT s)             = fdvSubst s
+
+export
+HasFreeDVars Elim where
+  fdv (F {}) = none
+  fdv (B {}) = none
+  fdv (App {fun, arg, _}) = fdv fun <+> fdv arg
+  fdv (CasePair {pair, ret, body, _}) = fdv pair <+> fdvT ret <+> fdvT body
+  fdv (CaseEnum {tag, ret, arms, _}) =
+    fdv tag <+> fdvT ret <+> foldMap fdv (values arms)
+  fdv (CaseNat {nat, ret, zero, succ, _}) =
+    fdv nat <+> fdvT ret <+> fdv zero <+> fdvT succ
+  fdv (CaseBox {box, ret, body, _}) =
+    fdv box <+> fdvT ret <+> fdvT body
+  fdv (DApp {fun, arg, _}) =
+    fdv fun <+> fv arg
+  fdv (Ann {tm, ty, _}) =
+    fdv tm <+> fdv ty
+  fdv (Coe {ty, p, q, val, _}) =
+    fdv @{DScope} ty <+> fv p <+> fv q <+> fdv val
+  fdv (Comp {ty, p, q, val, r, zero, one, _}) =
+    fdv ty <+> fv p <+> fv q <+> fdv val <+>
+    fv r <+> fdv @{DScope} zero <+> fdv @{DScope} one
+  fdv (TypeCase {ty, ret, arms, def, _}) =
+    fdv ty <+> fdv ret <+> fdv def <+> foldMap (\x => fdvT x.snd) (toList arms)
+  fdv (CloE s) = fdv s @{WithSubst}
+  fdv (DCloE s) = fdvSubst s
diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index c8079d8..0ef0ddd 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -6,6 +6,7 @@ import public Quox.Syntax.Subst
 import public Quox.Context
 import Quox.Pretty
 import Quox.Name
+import Quox.FreeVars
 
 import Data.Maybe
 import Data.Nat
@@ -185,20 +186,28 @@ split1 e loc eqs = case setConst VZ e loc eqs of
   C (eqs :< _) => Just (eqs, K e loc ::: id)
 
 export %inline
-split : Loc -> DimEq' (S d) -> List (Split d)
-split loc eqs = toList (split1 Zero loc eqs) <+> toList (split1 One loc eqs)
+split1' : DimConst -> Loc -> DimEq' (S d) -> List (Split d)
+split1' e loc eqs = toList $ split1 e loc eqs
+
+export %inline
+split : Loc -> DimEq' (S d) -> Bool -> List (Split d)
+split loc eqs False = split1' Zero loc eqs
+split loc eqs True  = split1' Zero loc eqs <+> split1' One loc eqs
 
 export
-splits' : Loc -> DimEq' d -> List (DSubst d 0)
-splits' _   [<]          = [id]
-splits' loc eqs@(_ :< _) =
-  [th . ph | (eqs', th) <- split loc eqs, ph <- splits' loc eqs']
+splits' : Loc -> DimEq' d -> FreeVars d -> List (DSubst d 0)
+splits' _   [<]          _  = [id]
+splits' loc eqs@(_ :< _) us = do
+  let (us, u) = uncons us
+  (eqs', th) <- split loc eqs u
+  ph         <- splits' loc eqs' us
+  pure $ th . ph
 
 ||| the Loc is put into each of the DimConsts
 export %inline
-splits : Loc -> DimEq d -> List (DSubst d 0)
-splits _   ZeroIsOne = []
-splits loc (C eqs)   = splits' loc eqs
+splits : Loc -> DimEq d -> FreeVars d -> List (DSubst d 0)
+splits _   ZeroIsOne _   = []
+splits loc (C eqs)   fvs = splits' loc eqs fvs
 
 
 private
diff --git a/lib/Quox/Syntax/Shift.idr b/lib/Quox/Syntax/Shift.idr
index ecfe476..9e005b7 100644
--- a/lib/Quox/Syntax/Shift.idr
+++ b/lib/Quox/Syntax/Shift.idr
@@ -4,6 +4,8 @@ import public Quox.Syntax.Var
 
 import Data.Nat
 import Data.So
+import Data.Singleton
+import Syntax.PreorderReasoning
 
 %default total
 
@@ -146,6 +148,25 @@ weakViaNat s by =
 %transform "Shift.weak" Shift.weak = weakViaNat
 
 
+export
+getFrom : {to : Nat} -> Shift from to -> Singleton from
+getFrom SZ      = Val to
+getFrom (SS by) = getFrom by
+
+private
+0 getFromViaNatProof : (by : Shift from to) -> from = to `minus` by.nat
+getFromViaNatProof by = Calc $
+  |~ from
+  ~~ minus (by.nat + from) by.nat ..<(minusPlus {})
+  ~~ minus to by.nat              ..<(cong (flip minus by.nat) (shiftDiff by))
+
+private
+getFromViaNat : {to : Nat} -> Shift from to -> Singleton from
+getFromViaNat by = rewrite getFromViaNatProof by in Val _
+
+%transform "Shift.getFrom" Shift.getFrom = getFromViaNat
+
+
 public export
 shift : Shift from to -> Var from -> Var to
 shift SZ      i = i
@@ -178,11 +199,12 @@ by . SS bz = SS $ by . bz
 private
 0 compNatProof : (by : Shift from mid) -> (bz : Shift mid to) ->
                  to = by.nat + bz.nat + from
-compNatProof by bz =
-  trans (shiftDiff bz) $
-  trans (cong (bz.nat +) (shiftDiff by)) $
-  trans (plusAssociative bz.nat by.nat from) $
-  cong (+ from) (plusCommutative bz.nat by.nat)
+compNatProof by bz = Calc $
+  |~ to
+  ~~ bz.nat + mid             ...(shiftDiff {})
+  ~~ bz.nat + (by.nat + from) ...(cong (bz.nat +) (shiftDiff {}))
+  ~~ bz.nat + by.nat + from   ...(plusAssociative {})
+  ~~ by.nat + bz.nat + from   ...(cong (+ from) (plusCommutative {}))
 
 private %inline
 compViaNat' : (by : Shift from mid) -> (bz : Shift mid to) ->
diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr
index 976f7bb..e584d4b 100644
--- a/lib/Quox/Syntax/Subst.idr
+++ b/lib/Quox/Syntax/Subst.idr
@@ -7,6 +7,7 @@ import Quox.Name
 import Data.Nat
 import Data.List
 import Data.SnocVect
+import Data.Singleton
 import Derive.Prelude
 
 %default total
@@ -124,6 +125,12 @@ one : f n -> Subst f (S n) n
 one x = fromSnocVect [< x]
 
 
+export
+getFrom : {to : Nat} -> Subst _ from to -> Singleton from
+getFrom (Shift by) = getFrom by
+getFrom (t ::: th) = [|S $ getFrom th|]
+
+
 ||| whether two substitutions with the same codomain have the same shape
 ||| (the same number of terms and the same shift at the end). if so, they
 ||| also have the same domain
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index c1db5fe..15e5b1e 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -33,7 +33,7 @@ record TyContext d n where
   dctx   : DimEq d
   dnames : BContext d
   tctx   : TContext d n
-  tnames : BContext n
+  tnames : BContext n -- only used for printing
   qtys   : QContext n -- only used for printing
 %name TyContext ctx
 
@@ -46,7 +46,7 @@ record EqContext n where
   dassign : DimAssign dimLen -- only used for printing
   dnames  : BContext dimLen -- only used for printing
   tctx    : TContext 0 n
-  tnames  : BContext n
+  tnames  : BContext n -- only used for printing
   qtys    : QContext n -- only used for printing
 %name EqContext ctx
 
@@ -78,6 +78,10 @@ public export
 CtxExtension : Nat -> Nat -> Nat -> Type
 CtxExtension d = Telescope ((Qty, BindName,) . Term d)
 
+public export
+CtxExtension0 : Nat -> Nat -> Nat -> Type
+CtxExtension0 d = Telescope ((BindName,) . Term d)
+
 namespace TyContext
   public export %inline
   empty : TyContext 0 0
@@ -100,10 +104,18 @@ namespace TyContext
       qtys    = qtys . qs
     }
 
+  export %inline
+  extendTyN0 : CtxExtension0 d n1 n2 -> TyContext d n1 -> TyContext d n2
+  extendTyN0 xss = extendTyN (map (Zero,) xss)
+
   export %inline
   extendTy : Qty -> BindName -> Term d n -> TyContext d n -> TyContext d (S n)
   extendTy q x s = extendTyN [< (q, x, s)]
 
+  export %inline
+  extendTy0 : BindName -> Term d n -> TyContext d n -> TyContext d (S n)
+  extendTy0 = extendTy Zero
+
   export %inline
   extendDim : BindName -> TyContext d n -> TyContext (S d) n
   extendDim x (MkTyContext {dimLen, dctx, dnames, tctx, tnames, qtys}) =
@@ -158,7 +170,7 @@ makeEqContext' ctx th = MkEqContext {
 export
 makeEqContext : TyContext d n -> DSubst d 0 -> EqContext n
 makeEqContext ctx@(MkTyContext {dnames, _}) th =
-  let (d' ** Refl) = lengthPrf0 dnames in makeEqContext' ctx th
+  let Val d = lengthPrf0 dnames in makeEqContext' ctx th
 
 namespace EqContext
   public export %inline
@@ -183,10 +195,18 @@ namespace EqContext
       dassign, dnames
     }
 
+  export %inline
+  extendTyN0 : CtxExtension0 0 n1 n2 -> EqContext n1 -> EqContext n2
+  extendTyN0 xss = extendTyN (map (Zero,) xss)
+
   export %inline
   extendTy : Qty -> BindName -> Term 0 n -> EqContext n -> EqContext (S n)
   extendTy q x s = extendTyN [< (q, x, s)]
 
+  export %inline
+  extendTy0 : BindName -> Term 0 n -> EqContext n -> EqContext (S n)
+  extendTy0 = extendTy Zero
+
   export %inline
   extendDim : BindName -> DimConst -> EqContext n -> EqContext n
   extendDim x e (MkEqContext {dassign, dnames, tctx, tnames, qtys}) =
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index 6fd3882..41cc4cd 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -32,6 +32,7 @@ modules =
   Quox.Syntax.Term.Pretty,
   Quox.Syntax.Term.Subst,
   Quox.Syntax.Var,
+  Quox.FreeVars,
   Quox.Displace,
   Quox.Definition,
   Quox.Whnf.Interface,