diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index a2cd868..9ffe7da 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -221,6 +221,11 @@ 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
+
 export %inline
 (forall n. PrettyHL (tm n)) => PrettyHL (Telescope tm from to) where
   prettyM tel = separate (hl Delim ";") <$> traverse prettyM (toList tel)