diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index 25f151b..a7c00eb 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -36,25 +36,25 @@ Context' a = Context (\_ => a)
 
 
 export
-toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
+toSnocList : Telescope {tm, _} -> SnocList (Exists tm)
 toSnocList [<]        = [<]
 toSnocList (tel :< t) = toSnocList tel :< Evidence _ t
 
 private
-toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
+toListAcc : Telescope {tm, _} -> List (Exists tm) -> List (Exists tm)
 toListAcc [<]        acc = acc
 toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc)
 
 export %inline
-toList : Telescope tm _ _ -> List (Exists tm)
+toList : Telescope {tm, _} -> List (Exists tm)
 toList tel = toListAcc tel []
 
 export %inline
-toSnocList' : Telescope' a _ _ -> SnocList a
+toSnocList' : Telescope' {a, _} -> SnocList a
 toSnocList' = map snd . toSnocList
 
 export %inline
-toList' : Telescope' a _ _ -> List a
+toList' : Telescope' {a, _} -> List a
 toList' = map snd . toList
 
 
@@ -65,15 +65,15 @@ tel1 . [<]         = tel1
 tel1 . (tel2 :< s) = (tel1 . tel2) :< s
 
 
-export
-getWith : CanShift tm => Context tm len -> Var len -> Shift len out -> tm out
-getWith (ctx :< t) VZ     th = t // drop1 th
-getWith (ctx :< t) (VS i) th = getWith ctx i (drop1 th)
+public export
+getShift : CanShift tm => Context tm len -> Var len -> Shift len out -> tm out
+getShift (ctx :< t) VZ     by = t // drop1 by
+getShift (ctx :< t) (VS i) by = getShift ctx i (drop1 by)
 
 infixl 8 !!
-export %inline
+public export %inline
 (!!) : CanShift tm => Context tm len -> Var len -> tm len
-ctx !! i = getWith ctx i SZ
+ctx !! i = getShift ctx i SZ
 
 
 ||| a triangle of bindings. each type binding in a context counts the ues of
@@ -173,36 +173,35 @@ zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
 
 
 export
-lengthPrf : Telescope _ from to -> Subset Nat $ \len => len + from = to
-lengthPrf [<]        = Element 0 Refl
-lengthPrf (tel :< _) = let len = lengthPrf tel in
-                       Element (S len.fst) (cong S len.snd)
+lengthPrf : Telescope _ from to -> (len : Nat ** len + from = to)
+lengthPrf [<]        = (0 ** Refl)
+lengthPrf (tel :< _) =
+  let len = lengthPrf tel in (S len.fst ** cong S len.snd)
 
 public export %inline
 length : Telescope {} -> Nat
 length = fst . lengthPrf
 
 
-parameters {0 acc : Nat -> Type}
-  export
-  foldl : (forall m, n. acc m -> tm n -> acc (S m)) ->
-          acc 0 -> (tel : Telescope tm from to) -> acc (length tel)
-  foldl f z [<]        = z
-  foldl f z (tel :< t) = f (foldl f z tel) t
+export
+foldl : {0 acc : Nat -> Type} ->
+        (f : forall n. acc n -> tm (n + from) -> acc (S n)) ->
+        (z : acc 0) -> (tel : Telescope tm from to) -> acc (length tel)
+foldl f z [<]        = z
+foldl f z (tel :< t) = f (foldl f z tel) (rewrite (lengthPrf tel).snd in t)
 
-parameters {auto _ : Monoid a}
-  export %inline
-  foldMap : (forall n. tm n -> a) -> Telescope tm from to -> a
-  foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
+export %inline
+foldMap : Monoid a => (forall n. tm n -> a) -> Telescope tm from to -> a
+foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
 
-  export %inline
-  fold : Telescope' a from to -> a
-  fold = foldMap id
+export %inline
+fold : Monoid a => Telescope' a from to -> a
+fold = foldMap id
 
-  ||| like `fold` but calculate the elements only when actually appending
-  export %inline
-  foldLazy : Telescope' (Lazy a) from to -> a
-  foldLazy = foldMap force
+||| like `fold` but calculate the elements only when actually appending
+export %inline
+foldLazy : Monoid a => Telescope' (Lazy a) from to -> a
+foldLazy = foldMap force
 
 
 export %inline