diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index a5d06b1..36d9320 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -229,7 +229,6 @@ prettyDTApps dnames tnames f xs = do
 private
 record CaseArm opts d n where
   constructor MkCaseArm
-  {0 dinner, ninner : Nat}
   pat    : Doc opts
   dbinds : BTelescope d dinner -- 🍴
   tbinds : BTelescope n ninner
@@ -297,7 +296,7 @@ prettyCase_ : {opts : _} ->
               Doc opts -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) ->
               Eff Pretty (Doc opts)
 prettyCase_ dnames tnames intro head ret body = do
-  head   <- assert_total prettyElim dnames tnames head
+  head   <- withPrec Outer $ assert_total prettyElim dnames tnames head
   ret    <- prettyCaseRet dnames tnames ret
   bodys  <- prettyCaseBody dnames tnames body
   return <- returnD; of_ <- ofD
@@ -325,11 +324,6 @@ private
 LetExpr : Nat -> Nat -> Nat -> Type
 LetExpr d n n' = (Telescope (LetBinder d) n n', Term d n')
 
-private
-PrettyLetResult : LayoutOpts -> Nat -> Type
-PrettyLetResult opts d =
-  Exists $ \n => (BContext n, Term d n, SnocList (Doc opts))
-
 -- [todo] factor out this and the untyped version somehow
 export
 splitLet : Telescope (LetBinder d) n n' -> Term d n' -> Exists (LetExpr d n)
@@ -364,9 +358,10 @@ prettyLets dnames xs lets = snd <$> go lets where
     Nothing => do
       e <- withPrec Outer $ assert_total prettyElim dnames tnames e
       eq <- cstD; d <- askAt INDENT
+      inn <- inD
       pure $ ifMultiline
-        (hsep [hdr, eq, e])
-        (vsep [hdr, indent d $ hsep [eq, e]])
+        (hsep [hdr, eq, e, inn])
+        (vsep [hdr, indent d $ hsep [eq, e, inn]])
 
   go : forall b. Telescope (LetBinder d) a b ->
        Eff Pretty (BContext b, SnocList (Doc opts))
@@ -437,13 +432,10 @@ prettyDisp u = map Just $ hl Universe =<<
   ifUnicode (text $ superscript $ show u) (text $ "^" ++ show u)
 
 
-prettyTerm dnames tnames (TYPE l _) =
-  case !(askAt FLAVOR) of
-    Unicode => do
-      star  <- hl Syntax "★"
-      level <- hl Universe $ text $ superscript $ show l
-      pure $ hcat [star, level]
-    Ascii   => [|hl Syntax "Type" <++> hl Universe (text $ show l)|]
+prettyTerm dnames tnames (TYPE l _) = do
+  type  <- hl Syntax . text =<< ifUnicode "★" "Type"
+  level <- prettyDisp l
+  pure $ maybe type (type <+>) level
 
 prettyTerm dnames tnames (IOState _) =
   ioStateD
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index fe8322c..7a54387 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -391,5 +391,5 @@ export
 prettyWhnfContext : {opts : _} -> WhnfContext d n -> Eff Pretty (Doc opts)
 prettyWhnfContext ctx =
   let Val n = ctx.termLen in
-  separateTight !commaD <$>
-  prettyTContext' ctx.dnames (replicate n "_") ctx.tnames ctx.tctx
+  sepSingle . exceptLast (<+> comma) . toList <$>
+    prettyTContext' ctx.dnames (replicate n "_") ctx.tnames ctx.tctx