diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index 20875d1..6a058c7 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -37,25 +37,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