diff --git a/Ix/IxVM/Kernel/DefEq.lean b/Ix/IxVM/Kernel/DefEq.lean
index c5dde3b6..2227a86c 100644
--- a/Ix/IxVM/Kernel/DefEq.lean
+++ b/Ix/IxVM/Kernel/DefEq.lean
@@ -39,6 +39,14 @@ def defEq := ⟦
   -- ============================================================================
   fn k_is_def_eq(a: KExpr, b: KExpr, types: List‹KExpr›,
                  top: List‹&KConstantInfo›, addrs: List‹Addr›) -> G {
+    -- When both sides are closed, the context can't affect the result;
+    -- collapse it so closed comparisons share a memo key across contexts.
+    -- `expr_lbr >= 0`, so the sum is 0 iff both sides are closed.
+    let lbr = expr_lbr(a) + expr_lbr(b);
+    let types = match lbr {
+      0 => store(ListNode.Nil),
+      _ => types,
+    };
     -- Tier 1: pointer equality short-circuit.
     match ptr_val(a) - ptr_val(b) {
       0 => 1,
diff --git a/Ix/IxVM/Kernel/Infer.lean b/Ix/IxVM/Kernel/Infer.lean
index 0aafb651..eac50ed8 100644
--- a/Ix/IxVM/Kernel/Infer.lean
+++ b/Ix/IxVM/Kernel/Infer.lean
@@ -54,6 +54,13 @@ def infer := ⟦
   -- ============================================================================
   fn k_infer(e: KExpr, types: List‹KExpr›,
              top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr {
+    -- Closed terms don't depend on the local context: collapse it so the
+    -- same closed subterm under different binder depths shares a memo key.
+    let lbr = expr_lbr(e);
+    let types = match lbr {
+      0 => store(ListNode.Nil),
+      _ => types,
+    };
     match load(e) {
       KExprNode.BVar(i) => types_lookup(types, i),
 
diff --git a/Ix/IxVM/Kernel/Whnf.lean b/Ix/IxVM/Kernel/Whnf.lean
index a80c5ddb..73ccb5f3 100644
--- a/Ix/IxVM/Kernel/Whnf.lean
+++ b/Ix/IxVM/Kernel/Whnf.lean
@@ -224,9 +224,17 @@ def whnf := ⟦
       KExprNode.Forall(_, _) => e,
       KExprNode.BVar(_) => e,
       _ =>
-        let pair = collect_spine(e);
-        match pair {
-          (head, spine) => whnf_with_spine(head, spine, types, top, addrs),
+        -- Closed-term context normalization: when `e` has no loose BVars,
+        -- whnf's result cannot depend on `types` (every spine major is
+        -- closed, so the `k_infer`/`is_prop_type` calls in the struct-iota
+        -- path never hit a BVar). Pass `Nil` so the same closed term whnf'd
+        -- under different contexts shares one memo key
+        -- `(head, spine, Nil, top, addrs)` -> cache hits. Open `e` keeps its
+        -- real context. Sound: a closed term reduces only to closed terms.
+        let (head, spine) = collect_spine(e);
+        match expr_lbr(e) {
+          0 => whnf_with_spine(head, spine, store(ListNode.Nil), top, addrs),
+          _ => whnf_with_spine(head, spine, types, top, addrs),
         },
     }
   }
diff --git a/Ix/IxVM/KernelTypes.lean b/Ix/IxVM/KernelTypes.lean
index 950a8f2c..3577bdbe 100644
--- a/Ix/IxVM/KernelTypes.lean
+++ b/Ix/IxVM/KernelTypes.lean
@@ -50,33 +50,6 @@ def kernelTypes := ⟦
 
   type KExpr = &KExprNode
 
-  -- ============================================================================
-  -- Values (NbE semantic domain)
-  -- ============================================================================
-
-  enum KValNode {
-    Srt(&KLevel),
-    Lit(KLiteral),
-    Lam(KVal, KExpr, KValEnv),
-    Pi(KVal, KExpr, KValEnv),
-    Ctor(G, List‹&KLevel›, G, List‹KVal›),
-    FVar(G, KVal, List‹KVal›),
-    Axiom(G, List‹&KLevel›, List‹KVal›),
-    Defn(G, List‹&KLevel›, List‹KVal›),
-    Thm(G, List‹&KLevel›, List‹KVal›),
-    Opaque(G, List‹&KLevel›, List‹KVal›),
-    Quot(G, List‹&KLevel›, List‹KVal›),
-    Induct(G, List‹&KLevel›, List‹KVal›),
-    Rec(G, List‹&KLevel›, List‹KVal›),
-    Proj(G, G, KVal, List‹KVal›),
-    Thunk(KExpr, KValEnv)
-  }
-
-  type KVal = &KValNode
-
-  -- Value environment (de Bruijn indexed, front = most recent binder)
-  type KValEnv = List‹KVal›
-
   -- ============================================================================
   -- Recursor Rule
   --