diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr
index 4b900bf..2e95742 100644
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@@ -218,19 +218,22 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       STRING tyLoc =>
         whnf defs ctx sg $ Ann s (STRING tyLoc) loc
 
-      -- η expand
+      -- η expand.... kinda
       --
       -- (coe (𝑖 ⇒ [π. A]) @p @q s)
       --   ⇝
-      -- [case1 coe (𝑖 ⇒ [π. A]) @p @q s return A‹q/𝑖› of {[x] ⇒ x}]
-      --   ∷ [π. A]‹q/𝑖›
-      BOX qty inner tyLoc =>
+      -- [case1 s ∷ [π.A]‹p/𝑖› return A‹q/𝑖›
+      --  of {[x] ⇒ coe (𝑖 ⇒ A) @p @q x}] ∷ [π.A]‹q/𝑖›
+      --
+      -- a literal η expansion of `e ⇝ [case e of {[x] ⇒ x}]` causes a loop in
+      -- the equality checker because whnf of `case e ⋯` requires whnf of `e`
+      BOX qty inner tyLoc => do
         let inner = CaseBox {
               qty  = One,
-              box  = Coe (SY [< i] ty) p q s loc,
-              ret  = SN $ ty // one q,
-              body = SY [< !(mnb "x" loc)] $ BVT 0 loc,
+              box  = Ann s (ty // one p) s.loc,
+              ret  = SN $ inner // one q,
+              body = SY [< !(mnb "x" loc)] $ E $
+                     Coe (ST [< i] $ weakT 1 inner) p q (BVT 0 s.loc) s.loc,
               loc
             }
-        in
         whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc