diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 316b2bb..afc8eef 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -134,6 +134,15 @@ public export %inline
 dweakT : (by : Nat) -> Term d n -> Term (by + d) n
 dweakT by t = t // shift by
 
+public export %inline
+dweakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s (by + d) n
+dweakS by t = t // shift by
+
+public export %inline
+dweakDS : {s : Nat} -> (by : Nat) ->
+          DScopeTermN s d n -> DScopeTermN s (by + d) n
+dweakDS by t = t // shift by
+
 public export %inline
 dweakE : (by : Nat) -> Elim d n -> Elim (by + d) n
 dweakE by t = t // shift by
@@ -143,6 +152,15 @@ public export %inline
 weakT : (by : Nat) -> Term d n -> Term d (by + n)
 weakT by t = t // shift by
 
+public export %inline
+weakS : {s : Nat} -> (by : Nat) -> ScopeTermN s d n -> ScopeTermN s d (by + n)
+weakS by t = t // shift by
+
+public export %inline
+weakDS : {s : Nat} -> (by : Nat) ->
+         DScopeTermN s d n -> DScopeTermN s d (by + n)
+weakDS by t = t // shift by
+
 public export %inline
 weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
 weakE by t = t // shift by
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index 671a06c..7b10046 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -26,6 +26,14 @@ CanShift (LocalVar d) where
   l // by = {type $= (// by), term $= map (// by)} l
 
 namespace LocalVar
+  export %inline
+  letVar : (type, term : Term d n) -> LocalVar d n
+  letVar type term = MkLocal {type, term = Just term}
+
+  export %inline
+  lamVar : (type : Term d n) -> LocalVar d n
+  lamVar type = MkLocal {type, term = Nothing}
+
   subD : DSubst d1 d2 -> LocalVar d1 n -> LocalVar d2 n
   subD th = {type $= (// th), term $= map (// th)}
 
@@ -135,7 +143,7 @@ namespace TyContext
 
   export %inline
   extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2
-  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, MkLocal s Nothing))
+  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s))
 
   export %inline
   extendTyLetN0 : CtxExtensionLet0 d n1 n2 -> TyContext d n1 -> TyContext d n2
@@ -148,7 +156,7 @@ namespace TyContext
   export %inline
   extendTyLet : Qty -> BindName -> Term d n -> Term d n ->
                 TyContext d n -> TyContext d (S n)
-  extendTyLet q x s e = extendTyLetN [< (q, x, MkLocal s (Just e))]
+  extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)]
 
   export %inline
   extendTy : Qty -> BindName -> Term d n -> TyContext d n -> TyContext d (S n)
@@ -239,7 +247,7 @@ namespace EqContext
 
   export %inline
   extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2
-  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, MkLocal s Nothing))
+  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s))
 
   export %inline
   extendTyLetN0 : CtxExtensionLet0 0 n1 n2 -> EqContext n1 -> EqContext n2
@@ -252,7 +260,7 @@ namespace EqContext
   export %inline
   extendTyLet : Qty -> BindName -> Term 0 n -> Term 0 n ->
                 EqContext n -> EqContext (S n)
-  extendTyLet q x s e = extendTyLetN [< (q, x, MkLocal s (Just e))]
+  extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)]
 
   export %inline
   extendTy : Qty -> BindName -> Term 0 n -> EqContext n -> EqContext (S n)
@@ -293,6 +301,25 @@ namespace WhnfContext
   empty : WhnfContext 0 0
   empty = MkWhnfContext [<] [<] [<]
 
+  export
+  extendTy' : BindName -> LocalVar d n -> WhnfContext d n -> WhnfContext d (S n)
+  extendTy' x var (MkWhnfContext {termLen, dnames, tnames, tctx}) =
+    MkWhnfContext {
+      dnames,
+      termLen = [|S termLen|],
+      tnames  = tnames :< x,
+      tctx    = tctx   :< var
+    }
+
+  export %inline
+  extendTy : BindName -> Term d n -> WhnfContext d n -> WhnfContext d (S n)
+  extendTy x ty ctx = extendTy' x (lamVar ty) ctx
+
+  export %inline
+  extendTyLet : BindName -> (type, term : Term d n) ->
+                WhnfContext d n -> WhnfContext d (S n)
+  extendTyLet x type term ctx = extendTy' x (letVar {type, term}) ctx
+
   export
   extendDimN : {s : Nat} -> BContext s -> WhnfContext d n ->
                WhnfContext (s + d) n
diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr
index f8c0e12..c97ed91 100644
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@@ -119,7 +119,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   eqCoe sty@(S [< j] ty) p q val r loc = do
     -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
     --   ⇝
-    -- comp [j ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›)
+    -- comp [j ⇒ A‹r/i›] @p @q ((eq ∷ (Eq [i ⇒ A] L R)‹p/j›) @r)
     --   @r { 0 j ⇒ L; 1 j ⇒ R }
     let ctx1 = extendDim j ctx
     Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
@@ -147,6 +147,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       (ST body.names $ body.term // (a' ::: shift 1)) loc
 
 
+-- new params block to call the above functions at different `n`
+parameters {auto _ : CanWhnf Term Interface.isRedexT}
+           {auto _ : CanWhnf Elim Interface.isRedexE}
+           (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
   ||| pushes a coercion inside a whnf-ed term
   export covering
   pushCoe : BindName ->
@@ -163,17 +167,22 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       IOState tyLoc =>
         whnf defs ctx sg $ Ann s (IOState tyLoc) loc
 
-      -- η expand it so that whnf for App can deal with it
+      -- η expand, then simplify the Coe/App in the body
       --
       -- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s)
       --   ⇝
       -- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖›
-      Pi {} =>
-        let inner = Coe (SY [< i] ty) p q s loc in
+      --   ⇝     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
+      -- (λ y ⇒ ⋯) ∷ (π.(x : A) → B)‹q/𝑖›   -- see `piCoe`
+      --
+      -- do the piCoe step here because otherwise equality checking keeps
+      -- doing the η forever
+      Pi {arg, res = S [< x] _, _} => do
+        let ctx' = extendTy x (arg // one p) ctx
+        body <- piCoe defs ctx' sg
+          (weakDS 1 $ SY [< i] ty) p q (weakT 1 s) (BVT 0 loc) loc
         whnf defs ctx sg $
-          Ann (LamY !(mnb "y" loc)
-                  (E $ App (weakE 1 inner) (BVT 0 loc) loc) loc)
-              (ty // one q) loc
+          Ann (LamY x (E body.fst) loc) (ty // one q) loc
 
       -- no η!!!
       -- push into a pair constructor, otherwise still stuck
@@ -199,17 +208,23 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       Enum cases tyLoc =>
         whnf defs ctx sg $ Ann s (Enum cases tyLoc) loc
 
-      -- η expand, same as for Π
+      -- η expand/simplify, same as for Π
       --
       -- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s)
       --   ⇝
       -- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›
-      Eq {} =>
-        let inner = Coe (SY [< i] ty) p q s loc in
+      --   ⇝     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
+      -- (δ 𝑘 ⇒ ⋯) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›   -- see `eqCoe`
+      --
+      -- do the eqCoe step here because otherwise equality checking keeps
+      -- doing the η forever
+      Eq {ty = S [< j] _, _} => do
+        let ctx' = extendDim j ctx
+        body <- eqCoe defs ctx' sg
+          (dweakDS 1 $ S [< i] $ Y ty) (weakD 1 p) (weakD 1 q)
+          (dweakT 1 s) (BV 0 loc) loc
         whnf defs ctx sg $
-          Ann (DLamY !(mnb "k" loc)
-                  (E $ DApp (dweakE 1 inner) (BV 0 loc) loc) loc)
-              (ty // one q) loc
+          Ann (DLamY i (E body.fst) loc) (ty // one q) loc
 
       -- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
       NAT tyLoc =>
@@ -219,22 +234,19 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       STRING tyLoc =>
         whnf defs ctx sg $ Ann s (STRING tyLoc) loc
 
-      -- η expand.... kinda
+      -- η expand/simplify
       --
-      -- (coe (𝑖 ⇒ [π. A]) @p @q s)
+      -- (coe (𝑖 ⇒ [π.A]) @p @q s)
       --   ⇝
-      -- [case1 s ∷ [π.A]‹p/𝑖› return A‹q/𝑖›
-      --  of {[x] ⇒ coe (𝑖 ⇒ A) @p @q x}] ∷ [π.A]‹q/𝑖›
+      -- [case coe (𝑖 ⇒ [π.A]) @p @q s return A‹q/𝑖› of {[x] ⇒ x}]
+      --   ⇝
+      -- [case1 s ∷ [π.A]‹p/𝑖› ⋯] ∷ [π.A]‹q/𝑖›   -- see `boxCoe`
       --
-      -- 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`
+      -- do the eqCoe step here because otherwise equality checking keeps
+      -- doing the η forever
       BOX qty inner tyLoc => do
-        let inner = CaseBox {
-              qty  = One,
-              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
-            }
-        whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc
+        body <- boxCoe defs ctx sg qty
+          (SY [< i] ty) p q s
+          (SN $ inner // one q)
+          (SY [< !(mnb "inner" loc)] (BVT 0 loc)) loc
+        whnf defs ctx sg $ Ann (Box (E body.fst) loc) (ty // one q) loc