diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 356c112..3817f82 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -113,6 +113,8 @@ data TypeLine a = MkTypeLine BaseName a
 
 export
 PrettyHL a => PrettyHL (TypeLine a) where
+  prettyM (MkTypeLine Unused ty) =
+    bracks <$> pretty0M ty
   prettyM (MkTypeLine i ty) =
     map bracks $ withPrec Outer $ prettyLams Nothing D [< i] ty
 
@@ -153,7 +155,7 @@ prettyCase' : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
 prettyCase' intro elim r ret arms = do
   elim  <- pretty0M elim
   ret   <- case r of
-    Unused => pretty0M ret
+    Unused => under T r $ pretty0M ret
     _      => prettyLams Nothing T [< r] ret
   arms  <- prettyArms T arms
   pure $ asep [intro <++> elim, returnD <++> ret, ofD <++> arms]
@@ -195,10 +197,8 @@ prettyBoxVal : PrettyHL a => Pretty.HasEnv m => a -> m (Doc HL)
 prettyBoxVal val = bracks <$> pretty0M val
 
 export
-prettyCompPat : Pretty.HasEnv m => Dim d -> DimConst -> BaseName -> m (Doc HL)
-prettyCompPat s e j = pure $
-  hsep [parens (hsep [!(pretty0M s), hl Syntax "=", !(pretty0M e)]),
-        !(pretty0M $ DV j)]
+prettyCompPat : Pretty.HasEnv m => DimConst -> BaseName -> m (Doc HL)
+prettyCompPat e j = hsep <$> sequence [pretty0M e, pretty0M $ DV j]
 
 export
 toNatLit : Term d n -> Maybe Nat
@@ -217,7 +217,7 @@ parameters (showSubsts : Bool)
   [TermSubst] PrettyHL (Term d n) using ElimSubst
   where
     prettyM (TYPE l) =
-      parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
+      pure $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
 
     prettyM (Pi qty s (S _ (N t))) = do
       dom <- pretty0M $ MkWithQty qty s
@@ -354,13 +354,14 @@ parameters (showSubsts : Bool)
 
     prettyM (Comp ty p q val r (S [< z] zero) (S [< o] one)) = do
       apps <- prettyApps' (L compD)
-        [(Nothing,  epretty ty),
+        [(Nothing,  epretty $ MkTypeLine Unused ty),
          (Just "@", epretty p),
          (Just "@", epretty q),
-         (Nothing,  epretty val)]
+         (Nothing,  epretty val),
+         (Just "@", epretty r)]
       arms <- prettyArms D
-        [([< z], !(prettyCompPat r Zero z), zero.term),
-         ([< o], !(prettyCompPat r One  o), one.term)]
+        [([< z], !(prettyCompPat Zero z), zero.term),
+         ([< o], !(prettyCompPat One  o), one.term)]
       pure $ apps <++> arms
 
     prettyM (TypeCase ty ret arms def) = do