diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 444b920..8a4d109 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -349,8 +349,8 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
         defs <- ask
         runReaderT {m} (MkCmpContext {mode}) $
           for_ (splits ctx.dctx) $ \th =>
-            compare0 defs (map (/// th) ctx.tctx)
-                     (ty /// th) (s /// th) (t /// th)
+            compare0 defs (map (// th) ctx.tctx)
+                     (ty // th) (s // th) (t // th)
 
       export covering
       compareType : (s, t : Term q d n) -> m ()
@@ -358,7 +358,7 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
         defs <- ask
         runReaderT {m} (MkCmpContext {mode}) $
           for_ (splits ctx.dctx) $ \th =>
-            compareType defs (map (/// th) ctx.tctx) (s /// th) (t /// th)
+            compareType defs (map (// th) ctx.tctx) (s // th) (t // th)
 
     namespace Elim
       ||| you don't have to pass the type in but the arguments must still be
@@ -369,7 +369,7 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
         defs <- ask
         runReaderT {m} (MkCmpContext {mode}) $
           for_ (splits ctx.dctx) $ \th =>
-            compare0 defs (map (/// th) ctx.tctx) (e /// th) (f /// th)
+            compare0 defs (map (// th) ctx.tctx) (e // th) (f // th)
 
   namespace Term
     export covering %inline
diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index 5aec6a2..9e53bf5 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -64,17 +64,17 @@ mutual
     pushSubstsWith th ph (TYPE l) =
       nclo $ TYPE l
     pushSubstsWith th ph (Pi qty x a body) =
-      nclo $ Pi qty x (subs a th ph) (subs body th ph)
+      nclo $ Pi qty x (a // th // ph) (body // th // ph)
     pushSubstsWith th ph (Lam x body) =
-      nclo $ Lam x $ subs body th ph
+      nclo $ Lam x $ body // th // ph
     pushSubstsWith th ph (Sig x a b) =
-      nclo $ Sig x (subs a th ph) (subs b th ph)
+      nclo $ Sig x (a // th // ph) (b // th // ph)
     pushSubstsWith th ph (Pair s t) =
-      nclo $ Pair (subs s th ph) (subs t th ph)
+      nclo $ Pair (s // th // ph) (t // th // ph)
     pushSubstsWith th ph (Eq i ty l r) =
-      nclo $ Eq i (subs ty th ph) (subs l th ph) (subs r th ph)
+      nclo $ Eq i (ty // th // ph) (l // th // ph) (r // th // ph)
     pushSubstsWith th ph (DLam i body) =
-      nclo $ DLam i $ subs body th ph
+      nclo $ DLam i $ body // th // ph
     pushSubstsWith th ph (E e) =
       let Element e nc = pushSubstsWith th ph e in nclo $ E e
     pushSubstsWith th ph (CloT s ps) =
@@ -92,13 +92,13 @@ mutual
         Left  yes => assert_total pushSubsts res
         Right no  => Element res no
     pushSubstsWith th ph (f :@ s) =
-      nclo $ subs f th ph :@ subs s th ph
+      nclo $ (f // th // ph) :@ (s // th // ph)
     pushSubstsWith th ph (CasePair pi p x r y z b) =
-      nclo $ CasePair pi (subs p th ph) x (subs r th ph) y z (subs b th ph)
+      nclo $ CasePair pi (p // th // ph) x (r // th // ph) y z (b // th // ph)
     pushSubstsWith th ph (f :% d) =
-      nclo $ subs f th ph :% (d // th)
+      nclo $ (f // th // ph) :% (d // th)
     pushSubstsWith th ph (s :# a) =
-      nclo $ subs s th ph :# subs a th ph
+      nclo $ (s // th // ph) :# (a // th // ph)
     pushSubstsWith th ph (CloE e ps) =
       pushSubstsWith th (comp th ps ph) e
     pushSubstsWith th ph (DCloE e ps) =
diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr
index ad3c97a..2349994 100644
--- a/lib/Quox/Syntax/Dim.idr
+++ b/lib/Quox/Syntax/Dim.idr
@@ -91,7 +91,7 @@ CanShift Dim where
   B i // by = B (i // by)
 
 export
-CanSubst Dim Dim where
+CanSubstSelf Dim where
   K e // _  = K e
   B i // th = th !! i
 
diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr
index 2fada8c..9a0fa9c 100644
--- a/lib/Quox/Syntax/Subst.idr
+++ b/lib/Quox/Syntax/Subst.idr
@@ -36,12 +36,8 @@ 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
-
-public export
-CanSubst1 : (Nat -> Type) -> Type
-CanSubst1 f = CanSubst f f
+interface FromVar term => CanSubstSelf term where
+  (//) : term from -> Lazy (Subst term from to) -> term to
 
 
 infixl 8 !!
@@ -53,7 +49,7 @@ public export
 
 
 public export
-CanSubst Var Var where
+CanSubstSelf Var where
   i    // Shift by   = shift by i
   VZ   // (t ::: th) = t
   VS i // (t ::: th) = i // th
@@ -66,7 +62,7 @@ shift by = Shift $ fromNat by
 
 infixl 9 .
 public export
-(.) : CanSubst1 f => Subst f from mid -> Subst f mid to -> Subst f from to
+(.) : CanSubstSelf f => Subst f from mid -> Subst f mid to -> Subst f from to
 Shift by      . Shift bz   = Shift $ by . bz
 Shift SZ      . ph         = ph
 Shift (SS by) . (t ::: th) = Shift by . th
@@ -83,12 +79,12 @@ map f (t ::: th) = f t ::: map f th
 
 
 public export %inline
-push : CanSubst1 f => Subst f from to -> Subst f (S from) (S to)
+push : CanSubstSelf f => Subst f from to -> Subst f (S from) (S to)
 push th = fromVar VZ ::: (th . shift 1)
 
 -- [fixme] a better way to do this?
 public export
-pushN : CanSubst1 f => (s : Nat) ->
+pushN : CanSubstSelf f => (s : Nat) ->
         Subst f from to -> Subst f (s + from) (s + to)
 pushN 0     th = th
 pushN (S s) th =
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index e7be95f..56cf5c8 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -5,62 +5,60 @@ import Data.Vect
 
 %default total
 
+namespace CanDSubst
+  public export
+  interface CanDSubst (0 tm : Nat -> Nat -> Type) where
+    (//) : tm dfrom n -> Lazy (DSubst dfrom dto) -> tm dto n
 
-infixl 8 ///
 mutual
-  namespace Term
-    ||| does the minimal reasonable work:
-    ||| - deletes the closure around an atomic constant like `TYPE`
-    ||| - deletes an identity substitution
-    ||| - composes (lazily) with an existing top-level dim-closure
-    ||| - otherwise, wraps in a new closure
-    export
-    (///) : Term q dfrom n -> DSubst dfrom dto -> Term q dto n
-    s          /// Shift SZ = s
-    TYPE l     /// _        = TYPE l
-    DCloT s ph /// th       = DCloT s $ ph . th
-    s          /// th       = DCloT s th
+  ||| does the minimal reasonable work:
+  ||| - deletes the closure around an atomic constant like `TYPE`
+  ||| - deletes an identity substitution
+  ||| - composes (lazily) with an existing top-level dim-closure
+  ||| - otherwise, wraps in a new closure
+  export
+  CanDSubst (Term q) where
+    s          // Shift SZ = s
+    TYPE l     // _        = TYPE l
+    DCloT s ph // th       = DCloT s $ ph . th
+    s          // th       = DCloT s th
 
-  namespace Elim
-    private
-    subDArgs : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
-    subDArgs (f :% d) th = subDArgs f th :% (d // th)
-    subDArgs e        th = DCloE e th
+  private
+  subDArgs : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
+  subDArgs (f :% d) th = subDArgs f th :% (d // th)
+  subDArgs e        th = DCloE e th
 
-    ||| does the minimal reasonable work:
-    ||| - deletes the closure around a term variable
-    ||| - deletes an identity substitution
-    ||| - composes (lazily) with an existing top-level dim-closure
-    ||| - immediately looks up bound variables in a
-    |||   top-level sequence of dimension applications
-    ||| - otherwise, wraps in a new closure
-    export
-    (///) : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
-    e          /// Shift SZ = e
-    F x        /// _        = F x
-    B i        /// _        = B i
-    f :% d     /// th       = subDArgs (f :% d) th
-    DCloE e ph /// th       = DCloE e $ ph . th
-    e          /// th       = DCloE e th
+  ||| does the minimal reasonable work:
+  ||| - deletes the closure around a term variable
+  ||| - deletes an identity substitution
+  ||| - composes (lazily) with an existing top-level dim-closure
+  ||| - immediately looks up bound variables in a
+  |||   top-level sequence of dimension applications
+  ||| - otherwise, wraps in a new closure
+  export
+  CanDSubst (Elim q) where
+    e          // Shift SZ = e
+    F x        // _        = F x
+    B i        // _        = B i
+    f :% d     // th       = subDArgs (f :% d) th
+    DCloE e ph // th       = DCloE e $ ph . th
+    e          // th       = DCloE e th
 
-  namespace ScopeTermN
-    export
-    (///) : ScopeTermN s q dfrom n -> DSubst dfrom dto -> ScopeTermN s q dto n
-    TUsed   body /// th = TUsed   $ body /// th
-    TUnused body /// th = TUnused $ body /// th
+  export
+  CanDSubst (ScopeTermN s q) where
+    TUsed   body // th = TUsed   $ body // th
+    TUnused body // th = TUnused $ body // th
 
-  namespace DScopeTermN
-    export
-    (///) : {s : Nat} ->
-            DScopeTermN s q dfrom n -> DSubst dfrom dto ->
-            DScopeTermN s q dto n
-    DUsed   body /// th = DUsed   $ body /// pushN s th
-    DUnused body /// th = DUnused $ body /// th
+  export
+  {s : Nat} -> CanDSubst (DScopeTermN s q) where
+    DUsed   body // th = DUsed   $ body // pushN s th
+    DUnused body // th = DUnused $ body // th
 
 
 export %inline FromVar (Elim q d) where fromVar = B
 export %inline FromVar (Term q d) where fromVar = E . fromVar
 
+
 ||| does the minimal reasonable work:
 ||| - deletes the closure around a *free* name
 ||| - deletes an identity substitution
@@ -68,7 +66,7 @@ export %inline FromVar (Term q d) where fromVar = E . fromVar
 ||| - immediately looks up a bound variable
 ||| - otherwise, wraps in a new closure
 export
-CanSubst (Elim q d) (Elim q d) where
+CanSubstSelf (Elim q d) where
   F x       // _  = F x
   B i       // th = th !! i
   CloE e ph // th = assert_total CloE e $ ph . th
@@ -76,6 +74,11 @@ CanSubst (Elim q d) (Elim q d) where
                          Shift SZ => e
                          th       => CloE e th
 
+namespace CanTSubst
+  public export
+  interface CanTSubst (0 tm : TermLike) where
+    (//) : tm q d from -> Lazy (TSubst q d from to) -> tm q d to
+
 ||| does the minimal reasonable work:
 ||| - deletes the closure around an atomic constant like `TYPE`
 ||| - deletes an identity substitution
@@ -83,7 +86,7 @@ CanSubst (Elim q d) (Elim q d) where
 ||| - goes inside `E` in case it is a simple variable or something
 ||| - otherwise, wraps in a new closure
 export
-CanSubst (Elim q d) (Term q d) where
+CanTSubst Term where
   TYPE l    // _  = TYPE l
   E e       // th = E $ e // th
   CloT s ph // th = CloT s $ ph . th
@@ -92,114 +95,45 @@ CanSubst (Elim q d) (Term q d) where
                          th       => CloT s th
 
 export %inline
-{s : Nat} -> CanSubst (Elim q d) (ScopeTermN s q d) where
+{s : Nat} -> CanTSubst (ScopeTermN s) where
   TUsed   body // th = TUsed   $ body // pushN s th
   TUnused body // th = TUnused $ body // th
 
 export %inline
-{s : Nat} -> CanSubst (Elim q d) (DScopeTermN s q d) where
-  DUsed   body // th = DUsed   $ body // map (/// shift s) th
+{s : Nat} -> CanTSubst (DScopeTermN s) where
+  DUsed   body // th = DUsed   $ body // map (// shift s) th
   DUnused body // th = DUnused $ body // th
 
-export %inline CanSubst Var (Term q d) where s // th = s // map (B {q, d}) th
-export %inline CanSubst Var (Elim q d) where e // th = e // map (B {q, d}) th
-
-export %inline
-{s : Nat} -> CanSubst Var (ScopeTermN s q d) where
-  b // th = b // map (B {q, d}) th
-
-export %inline
-{s : Nat} -> CanSubst Var (DScopeTermN s q d) where
-  b // th = b // map (B {q, d}) th
-
-
-infixl 8 //., ///
-mutual
-  namespace Term
-    ||| applies a term substitution with a less ambiguous type
-    export %inline
-    (//.) : Term q d from -> TSubst q d from to -> Term q d to
-    t //. th = t // th
-
-    ||| applies a term and dimension substitution
-    public export %inline
-    subs : Term q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
-           Term q dto to
-    subs s th ph = s /// th // ph
-
-  namespace Elim
-    ||| applies a term substitution with a less ambiguous type
-    export %inline
-    (//.) : Elim q d from -> TSubst q d from to -> Elim q d to
-    e //. th = e // th
-
-    ||| applies a term and dimension substitution
-    public export %inline
-    subs : Elim q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
-           Elim q dto to
-    subs e th ph = e /// th // ph
-
-  namespace ScopeTermN
-    ||| applies a term substitution with a less ambiguous type
-    export %inline
-    (//.) : {s : Nat} ->
-            ScopeTermN s q d from -> TSubst q d from to ->
-            ScopeTermN s q d to
-    body //. th = body // th
-
-    ||| applies a term and dimension substitution
-    public export %inline
-    subs : {s : Nat} ->
-           ScopeTermN s q dfrom from ->
-           DSubst dfrom dto -> TSubst q dto from to ->
-           ScopeTermN s q dto to
-    subs body th ph = body /// th // ph
-
-  namespace DScopeTermN
-    ||| applies a term substitution with a less ambiguous type
-    export %inline
-    (//.) : {s : Nat} -> DScopeTermN s q d from -> TSubst q d from to ->
-            DScopeTermN s q d to
-    body //. th = body // th
-
-    ||| applies a term and dimension substitution
-    public export %inline
-    subs : {s : Nat} ->
-           DScopeTermN s q dfrom from ->
-           DSubst dfrom dto -> TSubst q dto from to ->
-           DScopeTermN s q dto to
-    subs body th ph = body /// th // ph
-
-export %inline CanShift (Term q d) where s // by = s //. Shift by
-export %inline CanShift (Elim q d) where e // by = e //. Shift by
+export %inline CanShift (Term q d) where s // by = s // Shift by
+export %inline CanShift (Elim q d) where e // by = e // Shift by
 
 export %inline
 {s : Nat} -> CanShift (ScopeTermN s q d) where
-  b // by = b //. Shift by
+  b // by = b // Shift by
 
 
 export %inline
 comp : DSubst dfrom dto -> TSubst q dfrom from mid -> TSubst q dto mid to ->
        TSubst q dto from to
-comp th ps ph = map (/// th) ps . ph
+comp th ps ph = map (// th) ps . ph
 
 
 public export %inline
 dweakT : {by : Nat} -> Term q d n -> Term q (by + d) n
-dweakT t = t /// shift by
+dweakT t = t // shift by
 
 public export %inline
 dweakE : {by : Nat} -> Elim q d n -> Elim q (by + d) n
-dweakE t = t /// shift by
+dweakE t = t // shift by
 
 
 public export %inline
 weakT : {default 1 by : Nat} -> Term q d n -> Term q d (by + n)
-weakT t = t //. shift by
+weakT t = t // shift by
 
 public export %inline
 weakE : {default 1 by : Nat} -> Elim q d n -> Elim q d (by + n)
-weakE t = t //. shift by
+weakE t = t // shift by
 
 
 namespace ScopeTermN
@@ -226,7 +160,7 @@ sub1 t e = subN t [e]
 
 export %inline
 dsubN : DScopeTermN s q d n -> Vect s (Dim d) -> Term q d n
-dsubN (DUsed   body) ps = body /// fromVect ps
+dsubN (DUsed   body) ps = body // fromVect ps
 dsubN (DUnused body) _  = body
 
 export %inline
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 7de1e4c..89b40b0 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -38,7 +38,7 @@ record TyContext q d n where
 namespace TContext
   export %inline
   pushD : TContext q d n -> TContext q (S d) n
-  pushD tel = map (/// shift 1) tel
+  pushD tel = map (// shift 1) tel
 
 namespace TyContext
   public export %inline