diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index 773fb06..69e2a6f 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -7,6 +7,7 @@ import Quox.Name
 import Data.DPair
 import Data.Nat
 import Data.SnocList
+import Data.SnocVect
 import Data.Vect
 import Control.Monad.Identity
 
@@ -68,6 +69,21 @@ export %inline
 toList' : Telescope' a _ _ -> List a
 toList' = map snd . toList
 
+export
+fromSnocVect : SnocVect n a -> Context' a n
+fromSnocVect [<]       = [<]
+fromSnocVect (sx :< x) = fromSnocVect sx :< x
+
+
+public export
+tabulate : ((n : Nat) -> tm n) -> (n : Nat) -> Context tm n
+tabulate f 0     = [<]
+tabulate f (S k) = tabulate f k :< f k
+
+public export
+replicate : (n : Nat) -> a -> Context' a n
+replicate n x = tabulate (const x) n
+
 
 public export
 (.) : Telescope tm from mid -> Telescope tm mid to -> Telescope tm from to
@@ -81,6 +97,10 @@ export
   rewrite plusSuccRightSucc n to in
   (tel :< x) <>< xs
 
+export
+(++) : Telescope' a from to -> SnocVect n a -> Telescope' a from (n + to)
+tel ++ [<]       = tel
+tel ++ (sx :< x) = (tel ++ sx) :< x
 
 public export
 getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) ->
@@ -236,6 +256,12 @@ foldLazy : Monoid a => Telescope' (Lazy a) from to -> a
 foldLazy = foldMap force
 
 
+export %inline
+all, any : (forall n. tm n -> Bool) -> Telescope tm from to -> Bool
+all p = foldMap @{All} p
+any p = foldMap @{Any} p
+
+
 export %inline
 (forall n. Eq (tm n)) => Eq (Telescope tm from to) where
   (==) = foldLazy @{All} .: zipWithLazy (==)
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index fba3987..d66d9c9 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -368,7 +368,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
           ety <- computeElimType ctx e (noOr1 ne)
           compareType (extendTy zero eret.name ety ctx) eret.term fret.term
           (fst, snd) <- expectSigE defs ctx ety
-          let [x, y] = ebody.names
+          let [< x, y] = ebody.names
           Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
                         (substCasePairRet ety eret)
                         ebody.term fbody.term
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index ab8b00a..351ef62 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -4,8 +4,9 @@ module Quox.Parser.FromParser
 import Quox.Parser.Syntax
 import Quox.Parser.Parser
 import Quox.Typechecker
-import Data.List
 
+import Data.List
+import Data.SnocVect
 import public Control.Monad.Either
 import public Control.Monad.State
 import public Control.Monad.Reader
@@ -91,16 +92,16 @@ mutual
 
     Pi pi x s t =>
       Pi pi <$> fromPTermWith ds ns s
-            <*> fromPTermTScope ds ns [x] t
+            <*> fromPTermTScope ds ns [< x] t
 
     Lam x s =>
-      Lam <$> fromPTermTScope ds ns [x] s
+      Lam <$> fromPTermTScope ds ns [< x] s
 
     s :@ t =>
       map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t
 
     Sig x s t =>
-      Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [x] t
+      Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [< x] t
 
     Pair s t =>
       Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t
@@ -108,13 +109,13 @@ mutual
     Case pi pair (r, ret) (CasePair (x, y) body) =>
       map E $ Base.CasePair pi
         <$> fromPTermElim ds ns pair
-        <*> fromPTermTScope ds ns [r] ret
-        <*> fromPTermTScope ds ns [x, y] body
+        <*> fromPTermTScope ds ns [< r] ret
+        <*> fromPTermTScope ds ns [< x, y] body
 
     Case pi tag (r, ret) (CaseEnum arms) =>
       map E $ Base.CaseEnum pi
         <$> fromPTermElim ds ns tag
-        <*> fromPTermTScope ds ns [r] ret
+        <*> fromPTermTScope ds ns [< r] ret
         <*> assert_total fromPTermEnumArms ds ns arms
 
     Enum strs =>
@@ -127,12 +128,12 @@ mutual
     Tag str => pure $ Tag str
 
     Eq (i, ty) s t =>
-      Eq <$> fromPTermDScope ds ns [i] ty
+      Eq <$> fromPTermDScope ds ns [< i] ty
          <*> fromPTermWith ds ns s
          <*> fromPTermWith ds ns t
 
     DLam i s =>
-      DLam <$> fromPTermDScope ds ns [i] s
+      DLam <$> fromPTermDScope ds ns [< i] s
 
     s :% p =>
       map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
@@ -163,24 +164,26 @@ mutual
   private
   fromPTermTScope : {s : Nat} -> CanError m =>
                     Context' BName d -> Context' BName n ->
-                    Vect s BName ->
+                    SnocVect s BName ->
                     PTerm -> m (ScopeTermN s Three d n)
   fromPTermTScope ds ns xs t =
     if all isNothing xs then
       SN <$> fromPTermWith ds ns t
     else
-      SY (map (maybe Unused UN) xs) <$> fromPTermWith ds (ns <>< xs) t
+      SY (fromSnocVect $ map (maybe Unused UN) xs)
+        <$> fromPTermWith ds (ns ++ xs) t
 
   private
   fromPTermDScope : {s : Nat} -> CanError m =>
                     Context' BName d -> Context' BName n ->
-                    Vect s BName ->
+                    SnocVect s BName ->
                     PTerm -> m (DScopeTermN s Three d n)
   fromPTermDScope ds ns xs t =
     if all isNothing xs then
       SN <$> fromPTermWith ds ns t
     else
-      SY (map (maybe Unused UN) xs) <$> fromPTermWith (ds <>< xs) ns t
+      SY (fromSnocVect $ map (maybe Unused UN) xs)
+        <$> fromPTermWith (ds ++ xs) ns t
 
 
 export %inline
diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index aaf13dd..8d4f81b 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -121,14 +121,14 @@ mutual
     toPTermWith' ds ns s = case s of
       TYPE l =>
         TYPE l
-      Pi qty arg (S [x] res) =>
+      Pi qty arg (S [< x] res) =>
         Pi qty (Just $ show x)
           (toPTermWith ds ns arg)
           (toPTermWith ds (ns :< baseStr x) res.term)
-      Lam (S [x] body) =>
+      Lam (S [< x] body) =>
         Lam (Just $ show x) $
           toPTermWith ds (ns :< baseStr x) body.term
-      Sig fst (S [x] snd) =>
+      Sig fst (S [< x] snd) =>
         Sig (Just $ show x)
           (toPTermWith ds ns fst)
           (toPTermWith ds (ns :< baseStr x) snd.term)
@@ -138,10 +138,10 @@ mutual
         Enum $ SortedSet.toList cases
       Tag tag =>
         Tag tag
-      Eq (S [i] ty) l r =>
+      Eq (S [< i] ty) l r =>
         Eq (Just $ show i, toPTermWith (ds :< baseStr i) ns ty.term)
            (toPTermWith ds ns l) (toPTermWith ds ns r)
-      DLam (S [i] body) =>
+      DLam (S [< i] body) =>
         DLam (Just $ show i) $ toPTermWith (ds :< baseStr i) ns body.term
       E e =>
         toPTermWith ds ns e
@@ -165,12 +165,12 @@ mutual
         V $ MakePName [<] $ ns !!! i
       fun :@ arg =>
         toPTermWith ds ns fun :@ toPTermWith ds ns arg
-      CasePair qty pair (S [r] ret) (S [x, y] body) =>
+      CasePair qty pair (S [< r] ret) (S [< x, y] body) =>
         Case qty (toPTermWith ds ns pair)
              (Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term)
              (CasePair (Just $ show x, Just $ show y) $
                 toPTermWith ds (ns :< baseStr x :< baseStr y) body.term)
-      CaseEnum qty tag (S [r] ret) arms =>
+      CaseEnum qty tag (S [< r] ret) arms =>
         Case qty (toPTermWith ds ns tag)
              (Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term)
              (CaseEnum $ mapSnd (toPTermWith ds ns) <$> SortedMap.toList arms)
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 18434da..f3c43a4 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -6,6 +6,7 @@ import public Quox.Syntax.Subst
 import public Quox.Syntax.Qty
 import public Quox.Syntax.Dim
 import public Quox.Name
+import public Quox.Context
 -- import public Quox.OPE
 
 import Quox.Pretty
@@ -16,7 +17,6 @@ import Data.Maybe
 import Data.Nat
 import public Data.So
 import Data.String
-import Data.Vect
 import public Data.SortedMap
 import public Data.SortedSet
 
@@ -132,7 +132,7 @@ mutual
   public export
   record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
     constructor S
-    names : Vect s BaseName
+    names : NContext s
     body  : ScopedBody s f n
 
   public export
@@ -158,16 +158,16 @@ mutual
 ||| scope which ignores all its binders
 public export %inline
 SN : {s : Nat} -> f n -> Scoped s f n
-SN = S (replicate s "_") . N
+SN = S (replicate s Unused) . N
 
 ||| scope which uses its binders
 public export %inline
-SY : Vect s BaseName -> f (s + n) -> Scoped s f n
+SY : NContext s -> f (s + n) -> Scoped s f n
 SY ns = S ns . Y
 
 public export %inline
 name : Scoped 1 f n -> BaseName
-name (S [x] _) = x
+name (S [< x] _) = x
 
 public export %inline
 (.name) : Scoped 1 f n -> BaseName
@@ -177,7 +177,7 @@ s.name = name s
 public export %inline
 Pi_ : (qty : q) -> (x : BaseName) ->
       (arg : Term q d n) -> (res : Term q d (S n)) -> Term q d n
-Pi_ {qty, x, arg, res} = Pi {qty, arg, res = S [x] $ Y res}
+Pi_ {qty, x, arg, res} = Pi {qty, arg, res = S [< x] $ Y res}
 
 ||| non dependent function type
 public export %inline
@@ -188,7 +188,7 @@ Arr {qty, arg, res} = Pi {qty, arg, res = SN res}
 public export %inline
 Sig_ : (x : BaseName) -> (fst : Term q d n) ->
        (snd : Term q d (S n)) -> Term q d n
-Sig_ {x, fst, snd} = Sig {fst, snd = S [x] $ Y snd}
+Sig_ {x, fst, snd} = Sig {fst, snd = S [< x] $ Y snd}
 
 ||| non dependent pair type
 public export %inline
@@ -199,7 +199,7 @@ And {fst, snd} = Sig {fst, snd = SN snd}
 public export %inline
 Eq_ : (i : BaseName) -> (ty : Term q (S d) n) ->
       (l, r : Term q d n) -> Term q d n
-Eq_ {i, ty, l, r} = Eq {ty = S [i] $ Y ty, l, r}
+Eq_ {i, ty, l, r} = Eq {ty = S [< i] $ Y ty, l, r}
 
 ||| non dependent equality type
 public export %inline
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index a0e8cc7..6cfd920 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -73,12 +73,13 @@ prettyArm sort xs pat body = do
 
 export
 prettyLams : PrettyHL a => Pretty.HasEnv m =>
-             Maybe (Doc HL) -> BinderSort -> List BaseName -> a -> m (Doc HL)
+             Maybe (Doc HL) -> BinderSort -> SnocList BaseName -> a ->
+             m (Doc HL)
 prettyLams lam sort names body = do
   let var = case sort of T => TVar; D => DVar
-  header <- sequence $ [hlF var $ prettyM x | x <- names]
+  header <- sequence $ [hlF var $ prettyM x | x <- toList names]
   let header = sep $ maybe header (:: header) lam
-  parensIfM Outer =<< prettyArm sort (cast names) header body
+  parensIfM Outer =<< prettyArm sort names header body
 
 export
 prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
@@ -110,7 +111,7 @@ prettyCase : PrettyHL a => PrettyHL b => PrettyHL c => PrettyHL q =>
              m (Doc HL)
 prettyCase pi elim r ret arms = do
   elim <- prettyQtyBinds [pi] elim
-  ret  <- prettyLams Nothing T [r] ret
+  ret  <- prettyLams Nothing T [< r] ret
   arms <- prettyArms arms
   pure $ asep [caseD <++> elim, returnD <++> ret, ofD <++> arms]
 
@@ -127,12 +128,12 @@ parameters (showSubsts : Bool)
   where
     prettyM (TYPE l) =
       parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
-    prettyM (Pi qty s (S [x] t)) =
+    prettyM (Pi qty s (S [< x] t)) =
       prettyBindType [qty] x s !arrowD t.term
     prettyM (Lam (S x t)) =
       let GotLams {names, body, _} = getLams' x t.term Refl in
-      prettyLams (Just !lamD) T (toList names) body
-    prettyM (Sig s (S [x] t)) =
+      prettyLams (Just !lamD) T (toSnocList' names) body
+    prettyM (Sig s (S [< x] t)) =
       prettyBindType {q} [] x s !timesD t.term
     prettyM (Pair s t) =
       let GotPairs {init, last, _} = getPairs' [< s] t in
@@ -147,14 +148,14 @@ parameters (showSubsts : Bool)
       r  <- withPrec InEq $ prettyM r
       ty <- withPrec InEq $ prettyM ty
       parensIfM Eq $ asep [l <++> !eqndD, r <++> colonD, ty]
-    prettyM (Eq (S [i] (Y ty)) l r) = do
-      ty <- bracks <$> withPrec Outer (prettyLams Nothing D [i] ty)
+    prettyM (Eq (S [< i] (Y ty)) l r) = do
+      ty <- bracks <$> withPrec Outer (prettyLams Nothing D [< i] ty)
       l  <- withPrec Arg $ prettyM l
       r  <- withPrec Arg $ prettyM r
       parensIfM App $ eqD <++> asep [ty, l, r]
     prettyM (DLam (S i t)) =
       let GotDLams {names, body, _} = getDLams' i t.term Refl in
-      prettyLams (Just !dlamD) D (toList names) body
+      prettyLams (Just !dlamD) D (toSnocList' names) body
     prettyM (E e) = prettyM e
     prettyM (CloT s th) =
       if showSubsts then
@@ -179,10 +180,10 @@ parameters (showSubsts : Bool)
     prettyM (e :@ s) =
       let GotArgs {fun, args, _} = getArgs' e [s] in
       prettyApps Nothing fun args
-    prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do
+    prettyM (CasePair pi p (S [< r] ret) (S [< x, y] body)) = do
       pat <- parens . separate commaD <$> traverse (hlF TVar . prettyM) [x, y]
       prettyCase pi p r ret.term [([< x, y], pat, body.term)]
-    prettyM (CaseEnum pi t (S [r] ret) arms) =
+    prettyM (CaseEnum pi t (S [< r] ret) arms) =
       prettyCase pi t r ret.term
         [([<], prettyTag t, b) | (t, b) <- SortedMap.toList arms]
     prettyM (e :% d) =
diff --git a/lib/Quox/Syntax/Term/Split.idr b/lib/Quox/Syntax/Term/Split.idr
index dfe650e..8126c42 100644
--- a/lib/Quox/Syntax/Term/Split.idr
+++ b/lib/Quox/Syntax/Term/Split.idr
@@ -2,6 +2,7 @@ module Quox.Syntax.Term.Split
 
 import Quox.Syntax.Term.Base
 import Quox.Syntax.Term.Subst
+import Quox.Context
 
 import public Quox.No
 import public Data.Vect
@@ -130,25 +131,23 @@ getDArgs e = getDArgs' e []
 
 infixr 1 :\\
 public export
-absN : Vect m BaseName -> Term q d (m + n) -> Term q d n
-absN {m = 0}   []        s = s
-absN {m = S m} (x :: xs) s =
-  Lam $ S [x] $ Y $ absN xs $ rewrite sym $ plusSuccRightSucc m n in s
+absN : NContext m -> Term q d (m + n) -> Term q d n
+absN [<]       s = s
+absN (xs :< x) s = absN xs $ Lam $ SY [< x] s
 
 public export %inline
-(:\\) : Vect m BaseName -> Term q d (m + n) -> Term q d n
+(:\\) : NContext m -> Term q d (m + n) -> Term q d n
 (:\\) = absN
 
 
 infixr 1 :\\%
 public export
-dabsN : Vect m BaseName -> Term q (m + d) n -> Term q d n
-dabsN {m = 0}   []        s = s
-dabsN {m = S m} (x :: xs) s =
-  DLam $ S [x] $ Y $ dabsN xs $ rewrite sym $ plusSuccRightSucc m d in s
+dabsN : NContext m -> Term q (m + d) n -> Term q d n
+dabsN [<]       s = s
+dabsN (xs :< x) s = dabsN xs $ DLam $ SY [< x] s
 
 public export %inline
-(:\\%) : Vect m BaseName -> Term q (m + d) n -> Term q d n
+(:\\%) : NContext m -> Term q (m + d) n -> Term q d n
 (:\\%) = dabsN
 
 
@@ -156,7 +155,7 @@ public export
 record GetLams q d n where
   constructor GotLams
   {0 lams, rest : Nat}
-  names    : Vect lams BaseName
+  names    : NContext lams
   body     : Term q d rest
   0 eq     : lams + n = rest
   0 notLam : NotLam body
@@ -164,7 +163,7 @@ record GetLams q d n where
 mutual
   export %inline
   getLams' : forall lams, rest.
-             Vect lams BaseName -> Term q d rest -> (0 eq : lams + n = rest) ->
+             NContext lams -> Term q d rest -> (0 eq : lams + n = rest) ->
              GetLams q d n
   getLams' xs s0 eq =
     let Element s nc = pushSubsts s0 in
@@ -172,25 +171,25 @@ mutual
 
   private
   getLamsNc : forall lams, rest.
-              Vect lams BaseName ->
+              NContext lams ->
               (t : Term q d rest) -> (0 nc : NotClo t) =>
               (0 eq : lams + n = rest) ->
               GetLams q d n
   getLamsNc xs s Refl = case nchoose $ isLam s of
-    Left  y => let Lam (S [x] body) = s in
-               getLams' (x :: xs) (assert_smaller s body.term) Refl
+    Left  y => let Lam (S [< x] body) = s in
+               getLams' (xs :< x) (assert_smaller s body.term) Refl
     Right n => GotLams xs s Refl n
 
 export %inline
 getLams : Term q d n -> GetLams q d n
-getLams s = getLams' [] s Refl
+getLams s = getLams' [<] s Refl
 
 
 public export
 record GetDLams q d n where
   constructor GotDLams
   {0 lams, rest : Nat}
-  names     : Vect lams BaseName
+  names     : NContext lams
   body      : Term q rest n
   0 eq      : lams + d = rest
   0 notDLam : NotDLam body
@@ -198,7 +197,7 @@ record GetDLams q d n where
 mutual
   export %inline
   getDLams' : forall lams, rest.
-              Vect lams BaseName -> Term q rest n -> (0 eq : lams + d = rest) ->
+              NContext lams -> Term q rest n -> (0 eq : lams + d = rest) ->
               GetDLams q d n
   getDLams' xs s0 eq =
     let Element s nc = pushSubsts s0 in
@@ -206,18 +205,18 @@ mutual
 
   private
   getDLamsNc : forall lams, rest.
-               Vect lams BaseName ->
+               NContext lams ->
                (t : Term q rest n) -> (0 nc : NotClo t) =>
                (0 eq : lams + d = rest) ->
                GetDLams q d n
   getDLamsNc is s Refl = case nchoose $ isDLam s of
-    Left  y => let DLam (S [i] body) = s in
-               getDLams' (i :: is) (assert_smaller s body.term) Refl
+    Left  y => let DLam (S [< i] body) = s in
+               getDLams' (is :< i) (assert_smaller s body.term) Refl
     Right n => GotDLams is s Refl n
 
 export %inline
 getDLams : Term q d n -> GetDLams q d n
-getDLams s = getDLams' [] s Refl
+getDLams s = getDLams' [<] s Refl
 
 
 public export
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index b24d6b1..d9444cd 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -290,7 +290,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
     --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
     -- with ρ₁, ρ₂ ≤ πσ
-    let [x, y]  = body.names
+    let [< x, y]  = body.names
         pisg    = pi * sg.fst
         bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx
         bodyty  = substCasePairRet pairres.type ret
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index a339712..92a9185 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -16,7 +16,7 @@ defGlobals = fromList
    ("a'", mkPostulate Any $ FT "A"),
    ("b", mkPostulate Any $ FT "B"),
    ("f", mkPostulate Any $ Arr One (FT "A") (FT "A")),
-   ("id", mkDef Any (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0)),
+   ("id", mkDef Any (Arr One (FT "A") (FT "A")) ([< "x"] :\\ BVT 0)),
    ("eq-AB", mkPostulate Zero $ Eq0 (TYPE 0) (FT "A") (FT "B"))]
 
 parameters (label : String) (act : Lazy (M ()))
@@ -126,31 +126,31 @@ tests = "equality & subtyping" :- [
   "lambda" :- [
     testEq "λ x ⇒ [x] = λ x ⇒ [x]" $
       equalT empty (Arr One (FT "A") (FT "A"))
-        (["x"] :\\ BVT 0)
-        (["x"] :\\ BVT 0),
+        ([< "x"] :\\ BVT 0)
+        ([< "x"] :\\ BVT 0),
     testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $
       subT empty (Arr One (FT "A") (FT "A"))
-        (["x"] :\\ BVT 0)
-        (["x"] :\\ BVT 0),
+        ([< "x"] :\\ BVT 0)
+        ([< "x"] :\\ BVT 0),
     testEq "λ x ⇒ [x] = λ y ⇒ [y]" $
       equalT empty (Arr One (FT "A") (FT "A"))
-        (["x"] :\\ BVT 0)
-        (["y"] :\\ BVT 0),
+        ([< "x"] :\\ BVT 0)
+        ([< "y"] :\\ BVT 0),
     testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $
       equalT empty (Arr One (FT "A") (FT "A"))
-        (["x"] :\\ BVT 0)
-        (["y"] :\\ BVT 0),
+        ([< "x"] :\\ BVT 0)
+        ([< "y"] :\\ BVT 0),
     testNeq "λ x y ⇒ [x] ≠ λ x y ⇒ [y]" $
       equalT empty (Arr One (FT "A") $ Arr One (FT "A") (FT "A"))
-        (["x", "y"] :\\ BVT 1)
-        (["x", "y"] :\\ BVT 0),
+        ([< "x", "y"] :\\ BVT 1)
+        ([< "x", "y"] :\\ BVT 0),
     testEq "λ x ⇒ [a] = λ x ⇒ [a]  (Y vs N)" $
       equalT empty (Arr Zero (FT "B") (FT "A"))
-        (Lam $ SY ["x"] $ FT "a")
-        (Lam $ SN       $ FT "a"),
+        (Lam $ SY [< "x"] $ FT "a")
+        (Lam $ SN         $ FT "a"),
     testEq "λ x ⇒ [f [x]] = [f]  (η)" $
       equalT empty (Arr One (FT "A") (FT "A"))
-        (["x"] :\\ E (F "f" :@ BVT 0))
+        ([< "x"] :\\ E (F "f" :@ BVT 0))
         (FT "f")
   ],
 
@@ -168,7 +168,7 @@ tests = "equality & subtyping" :- [
 
   "equalities and uip" :-
   let refl : Term q d n -> Term q d n -> Elim q d n
-      refl a x = (DLam $ S ["_"] $ N x) :# (Eq0 a x x)
+      refl a x = (DLam $ S [< "_"] $ N x) :# (Eq0 a x x)
   in
   [
     note #""refl [A] x" is an abbreviation for "(δ i ⇒ x) ∷ (x ≡ x : A)""#,
@@ -217,7 +217,7 @@ tests = "equality & subtyping" :- [
            {globals = defGlobals `mergeLeft` fromList
               [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
       let ty : forall n. Term Three 0 n :=
-            Sig (FT "E") $ S ["_"] $ N $ FT "E" in
+            Sig (FT "E") $ S [< "_"] $ N $ FT "E" in
       equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
         (BV 0) (BV 1),
 
@@ -250,12 +250,12 @@ tests = "equality & subtyping" :- [
         (FT "b"),
     testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A  (N)" $
       equalT empty (Arr Zero (FT "B") (FT "A"))
-        (CloT (Lam $ S ["y"] $ N $ BVT 0) (F "a" ::: id))
-        (Lam $ S ["y"] $ N $ FT "a"),
+        (CloT (Lam $ S [< "y"] $ N $ BVT 0) (F "a" ::: id))
+        (Lam $ S [< "y"] $ N $ FT "a"),
     testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A  (Y)" $
       equalT empty (Arr Zero (FT "B") (FT "A"))
-        (CloT (["y"] :\\ BVT 1) (F "a" ::: id))
-        (["y"] :\\ FT "a")
+        (CloT ([< "y"] :\\ BVT 1) (F "a" ::: id))
+        ([< "y"] :\\ FT "a")
   ],
 
   "term d-closure" :- [
@@ -267,8 +267,8 @@ tests = "equality & subtyping" :- [
       equalTD 1
         (extendDim "𝑗" empty)
         (Eq0 (FT "A") (FT "a") (FT "a"))
-        (DCloT (["i"] :\\% FT "a") (K Zero ::: id))
-        (["i"] :\\% FT "a"),
+        (DCloT ([< "i"] :\\% FT "a") (K Zero ::: id))
+        ([< "i"] :\\% FT "a"),
     note "it is hard to think of well-typed terms with big dctxs"
   ],
 
@@ -334,20 +334,20 @@ tests = "equality & subtyping" :- [
       subE empty (F "f" :@ FT "a") (F "f" :@ FT "a"),
     testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = ([a ∷ A] ∷ A)  (β)" $
       equalE empty
-        (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
+        ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
         (E (FT "a" :# FT "A") :# FT "A"),
     testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = a  (βυ)" $
       equalE empty
-        (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
+        ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
         (F "a"),
     testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] = (λ y ⇒ [f [y]] ∷ ⋯) [a]  (β↘↙)" $
       let a = FT "A"; a2a = (Arr One a a) in
       equalE empty
-        (((["g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f")
-        (((["y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"),
+        ((([< "g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f")
+        ((([< "y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"),
     testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
       subE empty
-        (((["x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a")
+        ((([< "x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a")
         (F "a"),
     note "id : A ⊸ A ≔ λ x ⇒ [x]",
     testEq "id [a] = a" $ equalE empty (F "id" :@ FT "a") (F "a"),
@@ -407,13 +407,13 @@ tests = "equality & subtyping" :- [
   "annotation" :- [
     testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $
       equalE empty
-        ((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
+        (([< "x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
         (FT "f" :# Arr One (FT "A") (FT "A")),
     testEq "[f] ∷ A ⊸ A = f" $
       equalE empty (FT "f" :# Arr One (FT "A") (FT "A")) (F "f"),
     testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = f" $
       equalE empty
-        ((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
+        (([< "x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
         (F "f")
   ],
 
diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr
index 1faa0ee..211cf26 100644
--- a/tests/Tests/FromPTerm.idr
+++ b/tests/Tests/FromPTerm.idr
@@ -83,12 +83,14 @@ tests = "PTerm → Term" :- [
     parsesAs term fromPTerm' "x" $ BVT 2,
     parseFails term fromPTerm' "𝑖",
     parsesAs term fromPTerm' "f" $ FT "f",
-    parsesAs term fromPTerm' "λ w ⇒ w" $ ["w"] :\\ BVT 0,
-    parsesAs term fromPTerm' "λ w ⇒ x" $ ["w"] :\\ BVT 3,
-    parsesAs term fromPTerm' "λ x ⇒ x" $ ["x"] :\\ BVT 0,
+    parsesAs term fromPTerm' "λ w ⇒ w" $ [< "w"] :\\ BVT 0,
+    parsesAs term fromPTerm' "λ w ⇒ x" $ [< "w"] :\\ BVT 3,
+    parsesAs term fromPTerm' "λ x ⇒ x" $ [< "x"] :\\ BVT 0,
     parsesAs term fromPTerm' "λ a b ⇒ f a b" $
-      ["a", "b"] :\\ E (F "f" :@@ [BVT 1, BVT 0]),
+      [< "a", "b"] :\\ E (F "f" :@@ [BVT 1, BVT 0]),
     parsesAs term fromPTerm' "f @𝑖" $
       E $ F "f" :% BV 1
-  ]
+  ],
+
+  todo "everything else"
 ]
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index ab63f98..ade9237 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -29,9 +29,9 @@ tests = "whnf" :- [
     testNoStep "[A] ⊸ [B]" $
       Arr One (FT "A") (FT "B"),
     testNoStep "(x: [A]) ⊸ [B [x]]" $
-      Pi One (FT "A") (S ["x"] $ Y $ E $ F "B" :@ BVT 0),
+      Pi One (FT "A") (S [< "x"] $ Y $ E $ F "B" :@ BVT 0),
     testNoStep "λx. [x]" $
-      Lam $ S ["x"] $ Y $ BVT 0,
+      Lam $ S [< "x"] $ Y $ BVT 0,
     testNoStep "[f [a]]" $
       E $ F "f" :@ FT "a"
   ],
@@ -51,7 +51,7 @@ tests = "whnf" :- [
       (E (TYPE 1 :# TYPE 3))
       (TYPE 1),
     testWhnf "(λx. [x] ∷ [A] ⊸ [A]) [a]"
-      (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
+      ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
       (F "a")
   ],
 
@@ -87,28 +87,28 @@ tests = "whnf" :- [
 
   "term closure" :- [
     testWhnf "(λy. x){a/x}"
-      (CloT (Lam $ S ["y"] $ N $ BVT 0) (F "a" ::: id))
-      (Lam $ S ["y"] $ N $ FT "a"),
+      (CloT (Lam $ S [< "y"] $ N $ BVT 0) (F "a" ::: id))
+      (Lam $ S [< "y"] $ N $ FT "a"),
     testWhnf "(λy. y){a/x}"
-      (CloT (["y"] :\\ BVT 0) (F "a" ::: id))
-      (["y"] :\\ BVT 0)
+      (CloT ([< "y"] :\\ BVT 0) (F "a" ::: id))
+      ([< "y"] :\\ BVT 0)
   ],
 
   "looking inside […]" :- [
     testWhnf "[(λx. x ∷ A ⊸ A) [a]]"
-      (E $ ((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
+      (E $ (([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
       (FT "a")
   ],
 
   "nested redex" :- [
     note "whnf only looks at top level redexes",
     testNoStep "λy. [(λx. [x] ∷ [A] ⊸ [A]) [y]]" $
-      ["y"] :\\ E (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0),
+      [< "y"] :\\ E ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0),
     testNoStep "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $
       F "a" :@
-      E (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"),
+      E ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"),
     testNoStep "λx. [y [x]]{x/x,a/y}" {n = 1} $
-      ["x"] :\\ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id),
+      [< "x"] :\\ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id),
     testNoStep "f ([y [x]]{x/x,a/y})" {n = 1} $
       F "f" :@ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id)
   ]
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 14f1d81..52b1909 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -41,7 +41,7 @@ reflTy =
   Eq0 (BVT 1) (BVT 0) (BVT 0)
 
 reflDef : IsQty q => Term q d n
-reflDef = ["A","x"] :\\ ["i"] :\\% BVT 0
+reflDef = [< "A","x"] :\\ [< "i"] :\\% BVT 0
 
 
 fstTy : Term Three d n
@@ -52,8 +52,8 @@ fstTy =
 
 fstDef : Term Three d n
 fstDef =
-  (["A","B","p"] :\\
-    E (CasePair Any (BV 0) (SN $ BVT 2) (SY ["x","y"] $ BVT 1)))
+  ([< "A","B","p"] :\\
+    E (CasePair Any (BV 0) (SN $ BVT 2) (SY [< "x","y"] $ BVT 1)))
 
 sndTy : Term Three d n
 sndTy =
@@ -64,10 +64,10 @@ sndTy =
 
 sndDef : Term Three d n
 sndDef =
-  (["A","B","p"] :\\
+  ([< "A","B","p"] :\\
     E (CasePair Any (BV 0)
-        (SY ["p"] $ E $ BV 2 :@ E (F "fst" :@@ [BVT 3, BVT 2, BVT 0]))
-        (SY ["x","y"] $ BVT 0)))
+        (SY [< "p"] $ E $ BV 2 :@ E (F "fst" :@@ [BVT 3, BVT 2, BVT 0]))
+        (SY [< "x","y"] $ BVT 0)))
 
 
 defGlobals : Definitions Three
@@ -270,18 +270,18 @@ tests = "typechecker" :- [
   "lambda" :- [
     note "linear & unrestricted identity",
     testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $
-      check_ empty sone (["x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")),
+      check_ empty sone ([< "x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")),
     testTC "1 · (λ x ⇒ x) ⇐ A → A" $
-      check_ empty sone (["x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")),
+      check_ empty sone ([< "x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")),
     note "(fail) zero binding used relevantly",
     testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $
-      check_ empty sone (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
+      check_ empty sone ([< "x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
     note "(but ok in overall erased context)",
     testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
-      check_ empty szero (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
+      check_ empty szero ([< "x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
     testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯  # (type of refl)" $
       check_ empty sone
-        (["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
+        ([< "A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
         reflTy,
     testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯  # (def. and type of refl)" $
       check_ empty sone reflDef reflTy
@@ -295,7 +295,7 @@ tests = "typechecker" :- [
         (Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any],
     testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
       check_ empty sone
-        (Pair (FT "a") (["i"] :\\% FT "a"))
+        (Pair (FT "a") ([< "i"] :\\% FT "a"))
         (Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a"))
   ],
 
@@ -303,36 +303,36 @@ tests = "typechecker" :- [
     testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $
       inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) sone
         (CasePair One (BV 0) (SN $ FT "B")
-          (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
+          (SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
         (FT "B") [< One],
     testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $
       inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) sone
         (CasePair Any (BV 0) (SN $ FT "B")
-          (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
+          (SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
         (FT "B") [< Any],
     testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $
       inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) szero
         (CasePair Any (BV 0) (SN $ FT "B")
-          (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
+          (SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
         (FT "B") [< Zero],
     testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $
       infer_ (ctx [< ("x", FT "A" `And` FT "A")]) sone
         (CasePair Zero (BV 0) (SN $ FT "B")
-          (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])),
+          (SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])),
     testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $
       inferAsQ (ctx [< ("x", FT "A" `And` FT "B")]) sone
         (CasePair Any (BV 0) (SN $ FT "A")
-          (SY ["l", "r"] $ BVT 1))
+          (SY [< "l", "r"] $ BVT 1))
         (FT "A") [< Any],
     testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $
       inferAsQ (ctx [< ("x", FT "A" `And` FT "B")]) szero
         (CasePair One (BV 0) (SN $ FT "A")
-          (SY ["l", "r"] $ BVT 1))
+          (SY [< "l", "r"] $ BVT 1))
         (FT "A") [< Zero],
     testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $
       infer_ (ctx [< ("x", FT "A" `And` FT "B")]) sone
         (CasePair One (BV 0) (SN $ FT "A")
-          (SY ["l", "r"] $ BVT 1)),
+          (SY [< "l", "r"] $ BVT 1)),
     note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A",
     note "    ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)",
     testTC "0 · ‹type of fst› ⇐ ★₂" $
@@ -347,9 +347,9 @@ tests = "typechecker" :- [
       check_ empty sone sndDef sndTy,
     testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $
       inferAs empty szero
-        (F "snd" :@@ [TYPE 0, ["x"] :\\ BVT 0])
+        (F "snd" :@@ [TYPE 0, [< "x"] :\\ BVT 0])
         (Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $
-                (E $ F "fst" :@@ [TYPE 0, ["x"] :\\ BVT 0, BVT 0]))
+                (E $ F "fst" :@@ [TYPE 0, [< "x"] :\\ BVT 0, BVT 0]))
   ],
 
   "enums" :- [
@@ -369,13 +369,13 @@ tests = "typechecker" :- [
         (Eq0 (FT "A") (FT "a") (FT "a")),
     testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
       check_ empty szero
-        (["p","q"] :\\ ["i"] :\\% BVT 1)
+        ([< "p","q"] :\\ [< "i"] :\\% BVT 1)
         (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
          Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
          Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
     testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
       check_ empty szero
-        (["p","q"] :\\ ["i"] :\\% BVT 0)
+        ([< "p","q"] :\\ [< "i"] :\\% BVT 0)
         (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
          Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
          Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0))
@@ -388,7 +388,7 @@ tests = "typechecker" :- [
     note "  ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
     testTC "cong" $
       check_ empty sone
-        (["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
+        ([< "x", "y", "xy"] :\\ [< "i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
         (Pi_ Zero "x"  (FT "A") $
          Pi_ Zero "y"  (FT "A") $
          Pi_ One  "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $
@@ -401,7 +401,7 @@ tests = "typechecker" :- [
     note "  ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
     testTC "funext" $
       check_ empty sone
-        (["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
+        ([< "eq"] :\\ [< "i"] :\\% [< "x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
         (Pi_ One "eq"
           (Pi_ One "x" (FT "A")
             (Eq0 (E $ F "P" :@ BVT 0)