diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index 6717702..c93b20f 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -3,10 +3,12 @@ module Quox.Context
 import Quox.Syntax.Shift
 import Quox.Pretty
 import Quox.Name
+import Quox.NatExtra
+import Quox.PrettyValExtra
 
 import Data.DPair
 import Data.Nat
-import Data.Singleton
+import Quox.SingletonExtra
 import Data.SnocList
 import Data.SnocVect
 import Data.Vect
@@ -45,6 +47,10 @@ public export
 BContext : Nat -> Type
 BContext = Context' BindName
 
+public export
+BTelescope : Nat -> Nat -> Type
+BTelescope = Telescope' BindName
+
 
 public export
 unsnoc : Context tm (S n) -> (Context tm n, tm n)
@@ -123,6 +129,19 @@ replicate : (n : Nat) -> a -> Context' a n
 replicate n x = tabulateVar n $ const x
 
 
+public export
+replicateLTE : from `LTE'` to => a -> Telescope' a from to
+replicateLTE @{LTERefl}    x = [<]
+replicateLTE @{LTESuccR _} x = replicateLTE x :< x
+
+public export
+replicateTel : (from, to : Nat) -> a ->
+               Either (from `GT` to) (Telescope' a from to)
+replicateTel from to x = case isLTE' from to of
+  Yes lte  => Right $ replicateLTE x
+  No  nlte => Left  $ notLTEImpliesGT $ nlte . fromLTE
+
+
 public export
 (.) : Telescope tm from mid -> Telescope tm mid to -> Telescope tm from to
 tel1 . [<]         = tel1
@@ -275,12 +294,16 @@ lengthPrf [<]        = Element 0 Refl
 lengthPrf (tel :< _) =
   let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
 
-export
+public export
+lengthPrfSing : Telescope _ from to -> Singleton from -> Singleton to
+lengthPrfSing tel (Val from) =
+  let Element len prf = lengthPrf tel in
+  rewrite sym prf in
+  Val (len + from)
+
+public export
 lengthPrf0 : Context _ to -> Singleton to
-lengthPrf0 ctx =
-  let Element len prf = lengthPrf ctx in
-  rewrite sym prf `trans` plusZeroRightNeutral len in
-  [|len|]
+lengthPrf0 ctx = lengthPrfSing ctx (Val 0)
 
 public export %inline
 length : Telescope {} -> Nat
@@ -327,14 +350,30 @@ export %inline
 (forall n. Eq (tm n)) => Eq (Telescope tm from to) where
   (==) = foldLazy @{All} .: zipWithLazy (==)
 
+export %inline
+(forall n. DecEq (tm n)) => DecEq (Telescope tm from to) where
+  decEq [<] [<] = Yes Refl
+  decEq (xs :< x) (ys :< y) = do
+    let Yes Refl = decEq xs ys
+      | No n => No $ \case Refl => n Refl
+    let Yes Refl = decEq x y
+      | No n => No $ \case Refl => n Refl
+    Yes Refl
+  decEq [<]      (_ :< _) = No $ \case _ impossible
+  decEq (_ :< _) [<]      = No $ \case _ impossible
+
 export %inline
 (forall n. Ord (tm n)) => Ord (Telescope tm from to) where
   compare = foldLazy .: zipWithLazy compare
 
 export %inline
 (forall n. Show (tm n)) => Show (Telescope tm from to) where
-  showPrec d = showPrec d . toSnocList
-    where Show (Exists tm) where showPrec d t = showPrec d t.snd
+  showPrec d = showPrec d . toSnocList where
+    Show (Exists tm) where showPrec d t = showPrec d t.snd
+
+export %inline
+(forall n. PrettyVal (tm n)) => PrettyVal (Telescope tm from to) where
+  prettyVal xs = prettyVal $ toSnocList' $ map prettyVal xs
 
 
 parameters {opts : LayoutOpts} {0 tm : Nat -> Type}
@@ -361,5 +400,5 @@ parameters {opts : LayoutOpts} {0 tm : Nat -> Type}
 
 namespace BContext
   export
-  toNames : BContext n -> SnocList BaseName
+  toNames : BTelescope {} -> SnocList BaseName
   toNames = foldl (\xs, x => xs :< x.val) [<]
diff --git a/lib/Quox/NatExtra.idr b/lib/Quox/NatExtra.idr
index 714add1..79589a0 100644
--- a/lib/Quox/NatExtra.idr
+++ b/lib/Quox/NatExtra.idr
@@ -5,6 +5,7 @@ import Data.Nat.Division
 import Data.SnocList
 import Data.Vect
 import Data.String
+import Quox.Decidable
 
 %default total
 
@@ -14,26 +15,53 @@ data LTE' : Nat -> Nat -> Type where
   LTERefl  : LTE' n n
   LTESuccR : LTE' m n -> LTE' m (S n)
 %builtin Natural LTE'
+%name LTE' p, q
 
 public export %hint
 lteZero' : {n : Nat} -> LTE' 0 n
 lteZero' {n = 0}   = LTERefl
 lteZero' {n = S n} = LTESuccR lteZero'
+%transform "NatExtra.lteZero'" lteZero' {n} = believe_me n
 
 public export %hint
 lteSucc' : LTE' m n -> LTE' (S m) (S n)
 lteSucc' LTERefl      = LTERefl
 lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p
+%transform "NatExtra.lteSucc'" lteSucc' p = believe_me p
 
 public export
-fromLte : {n : Nat} -> LTE m n -> LTE' m n
-fromLte LTEZero     = lteZero'
-fromLte (LTESucc p) = lteSucc' $ fromLte p
+fromLTE : {n : Nat} -> LTE m n -> LTE' m n
+fromLTE LTEZero     = lteZero'
+fromLTE (LTESucc p) = lteSucc' $ fromLTE p
+-- %transform "NatExtra.fromLTE"
+--   fromLTE {n} p = believe_me (n `minus` believe_me p)
 
 public export
-toLte : {n : Nat} -> m `LTE'` n -> m `LTE` n
-toLte LTERefl      = reflexive
-toLte (LTESuccR p) = lteSuccRight (toLte p)
+toLTE : {m : Nat} -> m `LTE'` n -> m `LTE` n
+toLTE LTERefl      = reflexive
+toLTE (LTESuccR p) = lteSuccRight (toLTE p)
+-- %transform "NatExtra.toLTE" toLTE {m} p = believe_me m
+
+public export
+lteLTE' : {m, n : Nat} -> LTE m n <=> LTE' m n
+lteLTE' = MkEquivalence fromLTE toLTE
+
+public export
+isLTE' : (m, n : Nat) -> Dec (LTE' m n)
+isLTE' m n = map lteLTE' $ isLTE m n
+
+
+public export
+data LT' : Nat -> Nat -> Type where
+  LTZero : LT' 0 (S n)
+  LTSucc : LT' m n -> LT' (S m) (S n)
+%builtin Natural LT'
+%name LT' p, q
+
+public export
+Transitive Nat LT' where
+  transitive LTZero     (LTSucc q) = LTZero
+  transitive (LTSucc p) (LTSucc q) = LTSucc $ transitive p q
 
 
 private
diff --git a/lib/Quox/OPE.idr b/lib/Quox/OPE.idr
index 31203eb..a82d106 100644
--- a/lib/Quox/OPE.idr
+++ b/lib/Quox/OPE.idr
@@ -50,7 +50,7 @@ dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
 
 public export
 dropInner : {n : Nat} -> LTE m n -> OPE m n
-dropInner = dropInner' . fromLte
+dropInner = dropInner' . fromLTE
 
 public export
 dropInnerN : (m : Nat) -> OPE n (m + n)
diff --git a/lib/Quox/SingletonExtra.idr b/lib/Quox/SingletonExtra.idr
new file mode 100644
index 0000000..fac4bcf
--- /dev/null
+++ b/lib/Quox/SingletonExtra.idr
@@ -0,0 +1,11 @@
+module Quox.SingletonExtra
+
+import public Data.Singleton
+
+public export
+map : (f : a -> b) -> Singleton x -> Singleton (f x)
+map f x = [|f x|]
+
+public export
+(<$>) : (f : a -> b) -> Singleton x -> Singleton (f x)
+(<$>) = map