diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc
index ea51414..1e42c46 100644
--- a/docs/status/PROOF-STATUS.adoc
+++ b/docs/status/PROOF-STATUS.adoc
@@ -12,7 +12,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees.
 
 // Machine-readable ground-truth markers — checked by scripts/check-proof-status.sh.
 // Do not edit by hand without changing the MANIFEST accordingly.
-// gate:lean4 gated=15 quarantined=0
+// gate:lean4 gated=20 quarantined=0
 
 == Summary
 
@@ -99,7 +99,7 @@ every theorem depends on nothing outside Lean's three-axiom trusted base
 | ID | Target
 
 | ET-14 | *TEA erasure — the headline open problem. Never cite as proven.*
-| ET-1..3 (η) | η-laws / η-long normal forms extension of MECH-1
+| ET-1..3 (η) | η-laws / η-long normal forms extension of MECH-1 — **PARTIAL**: η-long forms `NfE`/`SpE` (neutrals at `★` only), `DefEqE` (β+η) with `defEq_to_defEqE`, `DecidableEq` for `NfE`/`SpE`, and a cast/exchange toolkit are landed and axiom-clean. **Still open: the η-long normalizer `nfE` (blocked on an `adjWkv` weakening-exchange lemma), soundness, completeness, `defEqE_iff_nfE`, `decDefEqE`, and the anti-vacuity example.** See issue #32
 | ET-1..3 (NAT) | type-level ℕ + recursor via NbE (stretch; research-adjacent)
 | ET-6, ET-7 | Structural Gate soundness + refusal characterization
 | ET-8, ET-9 | Polarity Gate blame accounting + no-laundering
diff --git a/verification/proofs/lean4/MANIFEST b/verification/proofs/lean4/MANIFEST
index d2f2a9d..e655a0e 100644
--- a/verification/proofs/lean4/MANIFEST
+++ b/verification/proofs/lean4/MANIFEST
@@ -16,3 +16,8 @@ verification/proofs/lean4|Systemet/L1/SubstLemmas.lean|gated|MECH-1: ET-2 commut
 verification/proofs/lean4|Systemet/L1/Soundness.lean|gated|MECH-1: ET-2 soundness (DefEq t (embNf (nf t)))
 verification/proofs/lean4|Systemet/L1/Completeness.lean|gated|MECH-1: ET-2 completeness + defEq_iff_nf
 verification/proofs/lean4|Systemet/L1/Decidable.lean|gated|MECH-1: ET-2 decEqNf/decDefEq (decidability of conversion)
+verification/proofs/lean4|Systemet/L1/EtaNormal.lean|gated|MECH-1 eta: eta-long normal forms NfE/SpE (neutrals only at star)
+verification/proofs/lean4|Systemet/L1/EtaConversion.lean|gated|MECH-1 eta: DefEqE (beta+eta) + defEq_to_defEqE embedding
+verification/proofs/lean4|Systemet/L1/EtaSubstLemmas.lean|gated|MECH-1 eta: cast/exchange toolkit for NfE/SpE
+verification/proofs/lean4|Systemet/L1/EtaHsub.lean|gated|MECH-1 eta: hereditary substitution on eta-long forms
+verification/proofs/lean4|Systemet/L1/EtaDecEq.lean|gated|MECH-1 eta: DecidableEq for NfE/SpE
diff --git a/verification/proofs/lean4/Systemet.lean b/verification/proofs/lean4/Systemet.lean
index b3bc33d..a20b75b 100644
--- a/verification/proofs/lean4/Systemet.lean
+++ b/verification/proofs/lean4/Systemet.lean
@@ -11,3 +11,8 @@ import Systemet.L1.SubstLemmas
 import Systemet.L1.Soundness
 import Systemet.L1.Completeness
 import Systemet.L1.Decidable
+import Systemet.L1.EtaNormal
+import Systemet.L1.EtaConversion
+import Systemet.L1.EtaSubstLemmas
+import Systemet.L1.EtaHsub
+import Systemet.L1.EtaDecEq
diff --git a/verification/proofs/lean4/Systemet/Audit.lean b/verification/proofs/lean4/Systemet/Audit.lean
index 21830b7..fc917bd 100644
--- a/verification/proofs/lean4/Systemet/Audit.lean
+++ b/verification/proofs/lean4/Systemet/Audit.lean
@@ -36,3 +36,7 @@ not in a status document. Update the PROOF-STATUS ledger when adding lines.
 #print axioms Systemet.L1.defEq_iff_nf
 #print axioms Systemet.L1.decEqNf
 #print axioms Systemet.L1.decDefEq
+
+-- MECH-1 (L1) eta extension: PARTIAL (goals 1,3 and DecidableEq only)
+#print axioms Systemet.L1.spEKindLe
+#print axioms Systemet.L1.defEq_to_defEqE
diff --git a/verification/proofs/lean4/Systemet/L1/EtaConversion.lean b/verification/proofs/lean4/Systemet/L1/EtaConversion.lean
new file mode 100644
index 0000000..2c327dd
--- /dev/null
+++ b/verification/proofs/lean4/Systemet/L1/EtaConversion.lean
@@ -0,0 +1,46 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+import Systemet.L1.EtaHsub
+import Systemet.L1.Conversion
+/-!
+# L1 βη-conversion (ET-η: the extended primitive relation)
+
+`DefEqE` is `DefEq` plus the η-rule: a term `t` at kind `k₁ ⇒ k₂` is
+convertible with `λ. (↑t) a₀` — its η-expansion, where `↑` is weakening by
+the fresh slot (`wkTy .vz`) and `a₀` is the fresh variable (`.var .vz`).
+The rules are otherwise verbatim `DefEq`, so `DefEqE` is again the least
+congruent equivalence containing β — now also containing η.
+
+`defEq_to_defEqE` embeds the β-theory: η strictly extends it.
+-/
+
+namespace Systemet.L1
+
+/-- Declarative βη-conversion: the least congruent equivalence containing
+    β and η. -/
+inductive DefEqE : {Γ : Ctx} → {k : Kind} → Ty Γ k → Ty Γ k → Prop where
+  | refl      : DefEqE t t
+  | symm      : DefEqE t u → DefEqE u t
+  | trans     : DefEqE t u → DefEqE u v → DefEqE t v
+  | beta      : (b : Ty (k₁ :: Γ) k₂) → (u : Ty Γ k₁) →
+                DefEqE (.app (.lam b) u) (subst0 b u)
+  | eta       : (t : Ty Γ (.arr k₁ k₂)) →
+                DefEqE t (.lam (.app (wkTy .vz t) (.var .vz)))
+  | arrowCong : DefEqE a a' → DefEqE b b' → DefEqE (.arrow a b) (.arrow a' b')
+  | lamCong   : DefEqE b b' → DefEqE (.lam b) (.lam b')
+  | appCong   : DefEqE f f' → DefEqE a a' → DefEqE (.app f a) (.app f' a')
+
+/-- β-conversion embeds into βη-conversion: η strictly extends β. -/
+theorem defEq_to_defEqE {Γ : Ctx} {k : Kind} {t u : Ty Γ k} :
+    DefEq t u → DefEqE t u := by
+  intro h
+  induction h with
+  | refl => exact .refl
+  | symm _ ih => exact ih.symm
+  | trans _ _ ih₁ ih₂ => exact ih₁.trans ih₂
+  | beta b u => exact .beta b u
+  | arrowCong _ _ ih₁ ih₂ => exact ih₁.arrowCong ih₂
+  | lamCong _ ih => exact ih.lamCong
+  | appCong _ _ ih₁ ih₂ => exact ih₁.appCong ih₂
+
+end Systemet.L1
diff --git a/verification/proofs/lean4/Systemet/L1/EtaDecEq.lean b/verification/proofs/lean4/Systemet/L1/EtaDecEq.lean
new file mode 100644
index 0000000..39fe89b
--- /dev/null
+++ b/verification/proofs/lean4/Systemet/L1/EtaDecEq.lean
@@ -0,0 +1,77 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+import Systemet.L1.EtaNormal
+/-!
+# L1 decidable equality of η-long normal forms
+
+Hand-rolled decidable equality for the mutual pair `NfE`/`SpE` — as with
+`Nf`/`Sp`, `deriving DecidableEq` cannot handle the mutual inductives, and
+`.ne`/`.cons` hide a head/argument kind that must be compared first (with
+`Kind`'s decidable equality) before the pieces can be compared
+componentwise.
+-/
+
+namespace Systemet.L1
+
+mutual
+  /-- Decidable equality on η-long normal forms. -/
+  def decEqNfE : {Γ : Ctx} → {k : Kind} → (m n : NfE Γ k) → Decidable (m = n)
+    | _, _, .lam b₁, .lam b₂ =>
+      match decEqNfE b₁ b₂ with
+      | .isTrue h => .isTrue (by rw [h])
+      | .isFalse h => .isFalse fun e => h (by injection e)
+    | _, _, .base n₁, .base n₂ =>
+      match Nat.decEq n₁ n₂ with
+      | .isTrue h => .isTrue (by rw [h])
+      | .isFalse h => .isFalse fun e => h (by injection e)
+    | _, _, .base _, .arrow _ _ => .isFalse fun e => by injection e
+    | _, _, .base _, .ne _ _ => .isFalse fun e => by injection e
+    | _, _, .arrow _ _, .base _ => .isFalse fun e => by injection e
+    | _, _, .arrow a₁ b₁, .arrow a₂ b₂ =>
+      match decEqNfE a₁ a₂ with
+      | .isFalse h₁ => .isFalse fun e => h₁ (by injection e)
+      | .isTrue h₁ =>
+        match decEqNfE b₁ b₂ with
+        | .isTrue h₂ => .isTrue (by rw [h₁, h₂])
+        | .isFalse h₂ => .isFalse fun e => h₂ (by injection e)
+    | _, _, .arrow _ _, .ne _ _ => .isFalse fun e => by injection e
+    | _, _, .ne _ _, .base _ => .isFalse fun e => by injection e
+    | _, _, .ne _ _, .arrow _ _ => .isFalse fun e => by injection e
+    | _, _, .ne (k := c₁) y₁ sp₁, .ne (k := c₂) y₂ sp₂ =>
+      if hc : c₁ = c₂ then by
+        subst hc
+        exact
+          if hy : y₁ = y₂ then
+            match decEqSpE sp₁ sp₂ with
+            | .isTrue hs => .isTrue (by rw [hy, hs])
+            | .isFalse hs => .isFalse fun e => hs (by injection e)
+          else .isFalse fun e => hy (by injection e)
+      else .isFalse fun e => hc (by injection e)
+  termination_by _ _ m _ => nfESize m
+  decreasing_by all_goals (simp only [nfESize]; omega)
+
+  /-- Decidable equality on spines of η-long forms. -/
+  def decEqSpE : {Γ : Ctx} → {a j : Kind} → (s t : SpE Γ a j) → Decidable (s = t)
+    | _, _, _, .nil, .nil => .isTrue rfl
+    | _, _, _, .nil, .cons _ _ => .isFalse fun e => by injection e
+    | _, _, _, .cons _ _, .nil => .isFalse fun e => by injection e
+    | _, _, _, .cons (b := b₁) sp₁ v₁, .cons (b := b₂) sp₂ v₂ =>
+      if hb : b₁ = b₂ then by
+        subst hb
+        exact
+          match decEqSpE sp₁ sp₂ with
+          | .isFalse h₁ => .isFalse fun e => h₁ (by injection e)
+          | .isTrue h₁ =>
+            match decEqNfE v₁ v₂ with
+            | .isTrue h₂ => .isTrue (by rw [h₁, h₂])
+            | .isFalse h₂ => .isFalse fun e => h₂ (by injection e)
+      else .isFalse fun e => hb (by injection e)
+  termination_by _ _ _ s _ => spESize s
+  decreasing_by all_goals (simp only [spESize]; omega)
+end
+
+instance : DecidableEq (NfE Γ k) := decEqNfE
+
+instance : DecidableEq (SpE Γ a j) := decEqSpE
+
+end Systemet.L1
diff --git a/verification/proofs/lean4/Systemet/L1/EtaHsub.lean b/verification/proofs/lean4/Systemet/L1/EtaHsub.lean
new file mode 100644
index 0000000..87b95d9
--- /dev/null
+++ b/verification/proofs/lean4/Systemet/L1/EtaHsub.lean
@@ -0,0 +1,104 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+import Systemet.L1.EtaNormal
+/-!
+# L1 hereditary substitution on η-long forms and the η-long normalizer
+
+The Keller–Altenkirch hereditary substitution, verbatim in structure from
+`Hsub.lean` but on η-long forms. Totality is by the same
+`(kindSize, tag, size)` lexicographic measure. The η-restriction *shrinks*
+the definition: a normal form at an arrow kind is always a `lam`, so
+`nappE` and the `cons` case of `appSpE` have a single, exhaustive clause —
+the neutral branch of β-application is impossible by typing.
+
+`nfE` normalizes every `Ty` in one structural pass; variables are
+η-expanded on the way in (`etaVarE`), which is exactly what makes the
+result η-long. The embeddings `embNfE`/`embSpE` read η-long forms back as
+terms.
+-/
+
+namespace Systemet.L1
+
+mutual
+  /-- Hereditary substitution on η-long normal forms. -/
+  def substNfE : {Γ : Ctx} → {j : Kind} → NfE Γ j → (x : Var Γ k) → NfE (rem x) k → NfE (rem x) j
+    | _, _, .lam b,     x, u => .lam (substNfE b (.vs x) (wkNfE .vz u))
+    | _, _, .base n,    _, _ => .base n
+    | _, _, .arrow a b, x, u => .arrow (substNfE a x u) (substNfE b x u)
+    | _, _, .ne y sp,   x, u =>
+      match eqv x y with
+      | .same      => appSpE u (substSpE sp x u)
+      | .diff _ y' => .ne y' (substSpE sp x u)
+  termination_by _ _ t _ _ => (kindSize k, 1, nfESize t)
+  decreasing_by
+    all_goals simp only [nfESize]
+    all_goals first
+      | (apply Prod.Lex.right; apply Prod.Lex.right; omega)
+      | (apply Prod.Lex.right; apply Prod.Lex.left; omega)
+      | (apply Prod.Lex.left
+         have h := spEKindLe sp
+         simp only [kindSize] at h ⊢
+         omega)
+
+  /-- Hereditary substitution on spines of η-long forms. -/
+  def substSpE : {Γ : Ctx} → {a j : Kind} → SpE Γ a j → (x : Var Γ k) → NfE (rem x) k → SpE (rem x) a j
+    | _, _, _, .nil,       _, _ => .nil
+    | _, _, _, .cons sp v, x, u => .cons (substSpE sp x u) (substNfE v x u)
+  termination_by _ _ _ sp _ _ => (kindSize k, 1, spESize sp)
+  decreasing_by
+    all_goals simp only [spESize]
+    all_goals first
+      | (apply Prod.Lex.right; apply Prod.Lex.right; omega)
+      | (apply Prod.Lex.right; apply Prod.Lex.left; omega)
+
+  /-- Fold an η-long form through a spine, β-reducing at each step. The
+      intermediate form is at an arrow kind, hence a `lam` — the single
+      clause is exhaustive. -/
+  def appSpE : {Γ : Ctx} → {a j : Kind} → NfE Γ a → SpE Γ a j → NfE Γ j
+    | _, _, _, u, .nil => u
+    | _, _, _, u, .cons sp v =>
+      match appSpE u sp with
+      | .lam t => substNfE t .vz v
+  termination_by _ a _ _ sp => (kindSize a, 0, spESize sp)
+  decreasing_by
+    all_goals simp only [spESize]
+    all_goals first
+      | (apply Prod.Lex.right; apply Prod.Lex.right; omega)
+      | (apply Prod.Lex.left
+         have h := spEKindLe sp
+         simp only [kindSize] at h ⊢
+         omega)
+end
+
+/-- Single β-application of η-long forms: the function is always a `lam`. -/
+def nappE : NfE Γ (.arr a b) → NfE Γ a → NfE Γ b
+  | .lam t, v => substNfE t .vz v
+
+/-- The η-long normalizer: one structural pass, η-expanding variables. -/
+def nfE : {Γ : Ctx} → {k : Kind} → Ty Γ k → NfE Γ k
+  | _, _, .var x     => etaVarE x
+  | _, _, .base n    => .base n
+  | _, _, .arrow a b => .arrow (nfE a) (nfE b)
+  | _, _, .lam b     => .lam (nfE b)
+  | _, _, .app f a   => nappE (nfE f) (nfE a)
+termination_by structural _ _ t => t
+
+mutual
+  /-- Embed an η-long normal form back into raw terms. -/
+  def embNfE : {Γ : Ctx} → {k : Kind} → NfE Γ k → Ty Γ k
+    | _, _, .lam b     => .lam (embNfE b)
+    | _, _, .base n    => .base n
+    | _, _, .arrow a b => .arrow (embNfE a) (embNfE b)
+    | _, _, .ne x sp   => embSpE (.var x) sp
+  termination_by _ _ t => nfESize t
+  decreasing_by all_goals (simp only [nfESize]; first | exact Nat.lt_succ_self _ | omega)
+
+  /-- Embed a spine, folding applications around a head term. -/
+  def embSpE : {Γ : Ctx} → {a j : Kind} → Ty Γ a → SpE Γ a j → Ty Γ j
+    | _, _, _, t, .nil       => t
+    | _, _, _, t, .cons sp v => .app (embSpE t sp) (embNfE v)
+  termination_by _ _ _ _ sp => spESize sp
+  decreasing_by all_goals (simp only [spESize]; omega)
+end
+
+end Systemet.L1
diff --git a/verification/proofs/lean4/Systemet/L1/EtaNormal.lean b/verification/proofs/lean4/Systemet/L1/EtaNormal.lean
new file mode 100644
index 0000000..9149ea1
--- /dev/null
+++ b/verification/proofs/lean4/Systemet/L1/EtaNormal.lean
@@ -0,0 +1,86 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+import Systemet.L1.Normal
+/-!
+# L1 η-long normal forms (ET-η, extending MECH-1)
+
+η-long normal forms `NfE` and neutral spines `SpE`, after Keller–Altenkirch
+("Hereditary Substitutions for Simple Types", MSFP 2010), whose development
+is natively η-long: a neutral `ne x sp` is a normal form **only at the base
+kind `★`**, so every η-long form at kind `k₁ ⇒ k₂` is a `lam`.
+
+`etaNe` is η-expansion of a neutral (a head variable applied through a
+spine) by *structural recursion on the result kind*: at `★` the neutral is
+already normal; at `b ⇒ c` we go under a binder, weaken the spine, append
+the η-expanded fresh variable, and recurse at `c` (the fresh variable is
+itself expanded at the strictly smaller kind `b`).
+-/
+
+namespace Systemet.L1
+
+mutual
+  /-- η-long β-normal forms: neutrals are admitted **only at `★`**. -/
+  inductive NfE : Ctx → Kind → Type where
+    | lam   : NfE (k₁ :: Γ) k₂ → NfE Γ (.arr k₁ k₂)
+    | base  : Nat → NfE Γ .star
+    | arrow : NfE Γ .star → NfE Γ .star → NfE Γ .star
+    | ne    : Var Γ k → SpE Γ k .star → NfE Γ .star
+
+  /-- Spines of η-long forms, left-nested (`cons sp v` appends the *last*
+      argument), exactly as `Sp`. -/
+  inductive SpE : Ctx → Kind → Kind → Type where
+    | nil  : SpE Γ k k
+    | cons : SpE Γ a (.arr b c) → NfE Γ b → SpE Γ a c
+end
+
+mutual
+  /-- Index-independent size of an η-long form (termination measure). -/
+  def nfESize : {Γ : Ctx} → {k : Kind} → NfE Γ k → Nat
+    | _, _, .lam b     => nfESize b + 1
+    | _, _, .base _    => 1
+    | _, _, .arrow a b => nfESize a + nfESize b + 1
+    | _, _, .ne _ sp   => spESize sp + 1
+
+  /-- Index-independent size of a spine (termination measure). -/
+  def spESize : {Γ : Ctx} → {a j : Kind} → SpE Γ a j → Nat
+    | _, _, _, .nil       => 0
+    | _, _, _, .cons sp v => spESize sp + nfESize v + 1
+end
+
+/-- The end kind of a spine is no larger than its head kind. -/
+theorem spEKindLe : {Γ : Ctx} → {a j : Kind} → SpE Γ a j → kindSize j ≤ kindSize a
+  | _, _, _, .nil => Nat.le_refl _
+  | _, _, _, .cons sp _ =>
+    Nat.le_trans (by simp [kindSize]; omega) (spEKindLe sp)
+
+mutual
+  /-- Weakening of η-long forms along one skipped slot. -/
+  def wkNfE : {Γ : Ctx} → (x : Var Γ k) → NfE (rem x) j → NfE Γ j
+    | _, x, .lam b     => .lam (wkNfE (.vs x) b)
+    | _, _, .base n    => .base n
+    | _, x, .arrow a b => .arrow (wkNfE x a) (wkNfE x b)
+    | _, x, .ne y sp   => .ne (wkv x y) (wkSpE x sp)
+  termination_by _ _ t => nfESize t
+  decreasing_by all_goals (simp only [nfESize]; first | exact Nat.lt_succ_self _ | omega)
+
+  /-- Weakening of spines along one skipped slot. -/
+  def wkSpE : {Γ : Ctx} → (x : Var Γ k) → SpE (rem x) a j → SpE Γ a j
+    | _, _, .nil       => .nil
+    | _, x, .cons sp v => .cons (wkSpE x sp) (wkNfE x v)
+  termination_by _ _ sp => spESize sp
+  decreasing_by all_goals (simp only [spESize]; omega)
+end
+
+/-- η-expansion of a neutral, by structural recursion on the result kind:
+    at `★` keep the neutral; at `b ⇒ c` bind a fresh variable of kind `b`,
+    weaken, append the η-expanded fresh variable, and recurse at `c`. -/
+def etaNe : (j : Kind) → {Γ : Ctx} → {a : Kind} → Var Γ a → SpE Γ a j → NfE Γ j
+  | .star, _, _, x, sp => .ne x sp
+  | .arr b c, _, _, x, sp =>
+    .lam (etaNe c (.vs x) (.cons (wkSpE .vz sp) (etaNe b .vz .nil)))
+termination_by structural j => j
+
+/-- η-expansion of a variable: the η-long normal form of `.var x`. -/
+abbrev etaVarE {Γ : Ctx} {a : Kind} (x : Var Γ a) : NfE Γ a := etaNe a x .nil
+
+end Systemet.L1
diff --git a/verification/proofs/lean4/Systemet/L1/EtaSubstLemmas.lean b/verification/proofs/lean4/Systemet/L1/EtaSubstLemmas.lean
new file mode 100644
index 0000000..d30c1b6
--- /dev/null
+++ b/verification/proofs/lean4/Systemet/L1/EtaSubstLemmas.lean
@@ -0,0 +1,368 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+import Systemet.L1.EtaHsub
+import Systemet.L1.SubstLemmas
+/-!
+# L1 substitution-commutation toolkit for η-long forms
+
+The Keller–Altenkirch commutation-lemma base of `SubstLemmas.lean`, ported
+to `NfE`/`SpE`. The variable-level laws (`eqv_refl`, `eqv_wkv`, `swp`,
+`remSwap`, `wkv_wkv`, the `castV` kit and the lexicographic-descent
+helpers) are *reused* from `SubstLemmas.lean` — they mention only `Var`.
+What is ported here: the `castNfE`/`castSpE` transport kit, the spine
+computation laws, commutation of the embeddings with weakening, the
+cancellation law, the exchange of weakenings, and the
+weakening/substitution exchange. The η-restriction only shrinks proofs:
+`appSpE`'s intermediate forms at arrow kinds are always `lam`s, so every
+neutral-function branch of the β-fold disappears.
+-/
+
+namespace Systemet.L1
+
+/-! ## Spine application unrolling -/
+
+/-- `appSpE` peels its last argument through `nappE`. -/
+theorem appSpE_cons (u : NfE Γ a) (sp : SpE Γ a (.arr b c)) (v : NfE Γ b) :
+    appSpE u (.cons sp v) = nappE (appSpE u sp) v := by
+  cases h : appSpE u sp with
+  | lam t => simp [appSpE, nappE, h]
+
+/-- `substNfE` at the substituted head: hand off to the spine fold. -/
+theorem substNfE_ne_self (x : Var Γ k) (sp : SpE Γ k .star) (u : NfE (rem x) k) :
+    substNfE (.ne x sp) x u = appSpE u (substSpE sp x u) := by
+  simp [substNfE, eqv_refl]
+
+/-- `substNfE` at a missed head: keep the neutral. -/
+theorem substNfE_ne_wkv (x : Var Γ k) (y : Var (rem x) c) (sp : SpE Γ c .star)
+    (u : NfE (rem x) k) :
+    substNfE (.ne (wkv x y) sp) x u = .ne y (substSpE sp x u) := by
+  simp [substNfE, eqv_wkv]
+
+/-! ## Embedding commutes with weakening -/
+
+mutual
+  /-- Embedding a weakened η-long form is weakening the embedding. -/
+  theorem embNfE_wkNfE : {Γ : Ctx} → {c j : Kind} → (x : Var Γ c) → (t : NfE (rem x) j) →
+      embNfE (wkNfE x t) = wkTy x (embNfE t)
+    | _, _, _, x, .lam (k₁ := k₁) b => by
+      simp only [wkNfE, embNfE, wkTy]
+      exact congrArg Ty.lam (embNfE_wkNfE (Var.vs (k' := k₁) x) b)
+    | _, _, _, _, .base n => by simp [wkNfE, embNfE, wkTy]
+    | _, _, _, x, .arrow a b => by
+      simp [wkNfE, embNfE, wkTy, embNfE_wkNfE x a, embNfE_wkNfE x b]
+    | _, _, _, x, .ne y sp => by
+      have h := embSpE_wkSpE x (.var y) sp
+      simp only [wkTy] at h
+      simp [wkNfE, embNfE, h]
+  termination_by _ _ _ _ t => nfESize t
+  decreasing_by all_goals (simp only [nfESize]; first | exact Nat.lt_succ_self _ | omega)
+
+  /-- Spine form of `embNfE_wkNfE`. -/
+  theorem embSpE_wkSpE : {Γ : Ctx} → {c a j : Kind} → (x : Var Γ c) → (h : Ty (rem x) a) →
+      (sp : SpE (rem x) a j) → embSpE (wkTy x h) (wkSpE x sp) = wkTy x (embSpE h sp)
+    | _, _, _, _, _, _, .nil => by simp [wkSpE, embSpE]
+    | _, _, _, _, x, h, .cons sp v => by
+      simp [wkSpE, embSpE, wkTy, embSpE_wkSpE x h sp, embNfE_wkNfE x v]
+  termination_by _ _ _ _ _ _ sp => spESize sp
+  decreasing_by all_goals (simp only [spESize]; omega)
+end
+
+/-! ## Cancellation: substituting a freshly weakened form -/
+
+mutual
+  /-- Substituting at a slot the form was just weakened past is the identity. -/
+  theorem substNfE_wkNfE_cancel : {Γ : Ctx} → {k j : Kind} → (x : Var Γ k) →
+      (t : NfE (rem x) j) → (u : NfE (rem x) k) → substNfE (wkNfE x t) x u = t
+    | _, _, _, x, .lam (k₁ := k₁) b, u => by
+      simp only [wkNfE, substNfE]
+      exact congrArg NfE.lam
+        (substNfE_wkNfE_cancel (Var.vs (k' := k₁) x) b (wkNfE .vz u))
+    | _, _, _, _, .base n, _ => by simp [wkNfE, substNfE]
+    | _, _, _, x, .arrow a b, u => by
+      simp [wkNfE, substNfE, substNfE_wkNfE_cancel x a u, substNfE_wkNfE_cancel x b u]
+    | _, _, _, x, .ne y sp, u => by
+      simp [wkNfE, substNfE_ne_wkv, substSpE_wkSpE_cancel x sp u]
+  termination_by _ _ _ _ t _ => nfESize t
+  decreasing_by all_goals (simp only [nfESize]; first | exact Nat.lt_succ_self _ | omega)
+
+  /-- Spine form of `substNfE_wkNfE_cancel`. -/
+  theorem substSpE_wkSpE_cancel : {Γ : Ctx} → {k a j : Kind} → (x : Var Γ k) →
+      (sp : SpE (rem x) a j) → (u : NfE (rem x) k) → substSpE (wkSpE x sp) x u = sp
+    | _, _, _, _, _, .nil, _ => by simp [wkSpE, substSpE]
+    | _, _, _, _, x, .cons sp v, u => by
+      simp [wkSpE, substSpE, substSpE_wkSpE_cancel x sp u, substNfE_wkNfE_cancel x v u]
+  termination_by _ _ _ _ _ sp _ => spESize sp
+  decreasing_by all_goals (simp only [spESize]; omega)
+end
+
+/-! ## Context-cast toolkit for η-long forms -/
+
+/-- Transport an η-long form along a context equality. -/
+def castNfE (h : Δ = Δ') (t : NfE Δ j) : NfE Δ' j := h ▸ t
+
+/-- Transport a spine along a context equality. -/
+def castSpE (h : Δ = Δ') (s : SpE Δ a j) : SpE Δ' a j := h ▸ s
+
+theorem castNfE_diag (e : Δ = Δ) (t : NfE Δ j) : castNfE e t = t := rfl
+
+theorem castSpE_diag (e : Δ = Δ) (s : SpE Δ a j) : castSpE e s = s := rfl
+
+theorem castNfE_lam (h : Δ = Δ') (b : NfE (k₁ :: Δ) k₂) :
+    castNfE h (.lam b) = .lam (castNfE (congrArg (k₁ :: ·) h) b) := by
+  subst h; rfl
+
+theorem castNfE_base (h : Δ = Δ') (n : Nat) :
+    castNfE h (.base n) = .base n := by
+  subst h; rfl
+
+theorem castNfE_arrow (h : Δ = Δ') (a b : NfE Δ .star) :
+    castNfE h (.arrow a b) = .arrow (castNfE h a) (castNfE h b) := by
+  subst h; rfl
+
+theorem castNfE_ne (h : Δ = Δ') (y : Var Δ c) (sp : SpE Δ c .star) :
+    castNfE h (.ne y sp) = .ne (castV h y) (castSpE h sp) := by
+  subst h; rfl
+
+theorem castSpE_nil (h : Δ = Δ') :
+    castSpE h (.nil (Γ := Δ) (k := a)) = .nil := by
+  subst h; rfl
+
+theorem castSpE_cons (h : Δ = Δ') (sp : SpE Δ a (.arr b c)) (v : NfE Δ b) :
+    castSpE h (.cons sp v) = .cons (castSpE h sp) (castNfE h v) := by
+  subst h; rfl
+
+theorem castNfE_appSpE (h : Δ = Δ') (F : NfE Δ a) (SP : SpE Δ a j) :
+    castNfE h (appSpE F SP) = appSpE (castNfE h F) (castSpE h SP) := by
+  subst h; rfl
+
+theorem castNfE_castNfE (e : Δ = Δ') (e' : Δ' = Δ'') (t : NfE Δ j) :
+    castNfE e' (castNfE e t) = castNfE (e.trans e') t := by
+  subst e; subst e'; rfl
+
+/-- Transporting past a fresh top slot commutes with weakening at `vz`. -/
+theorem castNfE_wkNfE_vz (h : Δ = Δ') (e : (c :: Δ : Ctx) = c :: Δ') (t : NfE Δ j) :
+    castNfE e (wkNfE (.vz (k := c) (Γ := Δ)) t) = wkNfE .vz (castNfE h t) := by
+  subst h; rfl
+
+/-- Spine form of `castNfE_wkNfE_vz`. -/
+theorem castSpE_wkSpE_vz (h : Δ = Δ') (e : (c :: Δ : Ctx) = c :: Δ') (sp : SpE Δ a j) :
+    castSpE e (wkSpE (.vz (k := c) (Γ := Δ)) sp) = wkSpE .vz (castSpE h sp) := by
+  subst h; rfl
+
+theorem castNfE_symm_cancel (e : Δ = Δ') (t : NfE Δ' j) :
+    castNfE e (castNfE e.symm t) = t := by
+  subst e; rfl
+
+theorem castSpE_symm_cancel (e : Δ = Δ') (sp : SpE Δ' a j) :
+    castSpE e (castSpE e.symm sp) = sp := by
+  subst e; rfl
+
+/-- η-expansion transports along a context equality. -/
+theorem castNfE_etaNe (h : Δ = Δ') (j : Kind) (x : Var Δ a) (sp : SpE Δ a j) :
+    castNfE h (etaNe j x sp) = etaNe j (castV h x) (castSpE h sp) := by
+  subst h; rfl
+
+/-! ## Exchange of weakenings -/
+
+mutual
+  /-- Exchange of weakenings on η-long forms. -/
+  theorem wkNfE_wkNfE : {Γ : Ctx} → {k c j : Kind} → (x : Var Γ k) →
+      (y : Var (rem x) c) → (t : NfE (rem y) j) →
+      wkNfE x (wkNfE y t) =
+        wkNfE (wkv x y) (wkNfE (swp x y) (castNfE (remSwap x y).symm t))
+    | _, _, _, _, x, y, .lam (k₁ := k₁) b => by
+      rw [castNfE_lam]
+      simp only [wkNfE]
+      exact congrArg NfE.lam
+        (wkNfE_wkNfE (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y) b)
+    | _, _, _, _, x, y, .base n => by
+      rw [castNfE_base]
+      simp [wkNfE]
+    | _, _, _, _, x, y, .arrow a b => by
+      rw [castNfE_arrow]
+      simp only [wkNfE]
+      rw [wkNfE_wkNfE x y a, wkNfE_wkNfE x y b]
+    | _, _, _, _, x, y, .ne z sp => by
+      rw [castNfE_ne]
+      simp only [wkNfE]
+      rw [wkv_wkv x y z, wkSpE_wkSpE x y sp]
+  termination_by _ _ _ _ _ _ t => nfESize t
+  decreasing_by all_goals (simp only [nfESize]; first | exact Nat.lt_succ_self _ | omega)
+
+  /-- Exchange of weakenings on spines. -/
+  theorem wkSpE_wkSpE : {Γ : Ctx} → {k c a j : Kind} → (x : Var Γ k) →
+      (y : Var (rem x) c) → (sp : SpE (rem y) a j) →
+      wkSpE x (wkSpE y sp) =
+        wkSpE (wkv x y) (wkSpE (swp x y) (castSpE (remSwap x y).symm sp))
+    | _, _, _, _, _, x, y, .nil => by
+      rw [castSpE_nil]
+      simp [wkSpE]
+    | _, _, _, _, _, x, y, .cons sp v => by
+      rw [castSpE_cons]
+      simp only [wkSpE]
+      rw [wkSpE_wkSpE x y sp, wkNfE_wkNfE x y v]
+  termination_by _ _ _ _ _ _ _ sp => spESize sp
+  decreasing_by all_goals (simp only [spESize]; omega)
+end
+
+/-- `substNfE` at the other slot of an exchange pair: the head misses, and
+    the surviving position is `swp x y`. -/
+theorem substNfE_ne_wkv' (x : Var Γ k) (y : Var (rem x) b) (sp : SpE Γ k .star)
+    (W : NfE (rem (wkv x y)) b) :
+    substNfE (.ne x sp) (wkv x y) W = .ne (swp x y) (substSpE sp (wkv x y) W) := by
+  rw [show (NfE.ne x sp : NfE Γ .star) = .ne (wkv (wkv x y) (swp x y)) sp from by
+    rw [wkv_swp]]
+  exact substNfE_ne_wkv (wkv x y) (swp x y) sp W
+
+/-! ## Weakening / substitution exchange -/
+
+mutual
+  /-- Weakening exchanges with hereditary substitution: substituting the
+      other slot of an exchange pair into a weakened η-long form. -/
+  theorem substNfE_wkNfE : {Γ : Ctx} → {k b j : Kind} → (x : Var Γ k) →
+      (y : Var (rem x) b) → (s : NfE (rem x) j) → (v : NfE (rem y) b) →
+      (W : NfE (rem (wkv x y)) b) →
+      W = wkNfE (swp x y) (castNfE (remSwap x y).symm v) →
+      substNfE (wkNfE x s) (wkv x y) W
+        = wkNfE (swp x y) (castNfE (remSwap x y).symm (substNfE s y v))
+    | _, _, _, _, x, y, .lam (k₁ := k₁) s₀, v, W, hW => by
+      subst hW
+      have h1 := substNfE_wkNfE (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y) s₀
+        (wkNfE (Var.vz (k := k₁) (Γ := rem y)) v)
+        (wkNfE (.vz (k := k₁) (Γ := rem (wkv x y)))
+          (wkNfE (swp x y) (castNfE (remSwap x y).symm v)))
+        ((wkNfE_wkNfE (Var.vz (k := k₁) (Γ := rem (wkv x y))) (swp x y)
+            (castNfE (remSwap x y).symm v)).trans
+          (congrArg (wkNfE (swp (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y)))
+            (castNfE_wkNfE_vz (remSwap x y).symm
+              (remSwap (Var.vs (k' := k₁) x)
+                (Var.vs (k' := k₁) y)).symm v)).symm)
+      simp only [wkNfE, substNfE]
+      rw [castNfE_lam]
+      simp only [wkNfE]
+      exact congrArg NfE.lam h1
+    | _, _, _, _, x, y, .base n, v, W, hW => by
+      subst hW
+      simp only [wkNfE, substNfE]
+      rw [castNfE_base]
+      simp [wkNfE]
+    | _, _, _, _, x, y, .arrow a₀ b₀, v, W, hW => by
+      subst hW
+      simp only [wkNfE, substNfE]
+      rw [castNfE_arrow]
+      simp only [wkNfE]
+      rw [substNfE_wkNfE x y a₀ v _ rfl, substNfE_wkNfE x y b₀ v _ rfl]
+    | _, _, _, _, x, y, .ne (k := c) z sp, v, W, hW =>
+      match c, z, sp, eqv y z with
+      | _, _, sp, .same => by
+        subst hW
+        simp only [wkNfE]
+        rw [substNfE_ne_self, substNfE_ne_self,
+          substSpE_wkSpE x y sp v _ rfl,
+          ← wkNfE_appSpE (swp x y) (castNfE (remSwap x y).symm v)
+            (castSpE (remSwap x y).symm (substSpE sp y v)),
+          ← castNfE_appSpE (remSwap x y).symm v (substSpE sp y v)]
+      | _, _, sp, .diff _ z' => by
+        subst hW
+        simp only [wkNfE]
+        rw [wkv_wkv x y z', substNfE_ne_wkv, substNfE_ne_wkv,
+          castNfE_ne (remSwap x y).symm z' (substSpE sp y v)]
+        simp only [wkNfE]
+        rw [substSpE_wkSpE x y sp v _ rfl]
+  termination_by _ _ b _ _ _ s _ _ _ => (kindSize b, 1, nfESize s)
+  decreasing_by
+    all_goals simp only [nfESize]
+    all_goals first
+      | (apply Prod.Lex.right; apply Prod.Lex.right;
+         first | omega | exact Nat.lt_succ_self _)
+      | (apply Prod.Lex.right; apply Prod.Lex.left; omega)
+
+  /-- Spine form of `substNfE_wkNfE`. -/
+  theorem substSpE_wkSpE : {Γ : Ctx} → {k b a j : Kind} → (x : Var Γ k) →
+      (y : Var (rem x) b) → (sp : SpE (rem x) a j) → (v : NfE (rem y) b) →
+      (W : NfE (rem (wkv x y)) b) →
+      W = wkNfE (swp x y) (castNfE (remSwap x y).symm v) →
+      substSpE (wkSpE x sp) (wkv x y) W
+        = wkSpE (swp x y) (castSpE (remSwap x y).symm (substSpE sp y v))
+    | _, _, _, _, _, x, y, .nil, v, W, hW => by
+      subst hW
+      simp only [wkSpE, substSpE]
+      rw [castSpE_nil]
+      simp [wkSpE]
+    | _, _, _, _, _, x, y, .cons sp₀ v₀, v, W, hW => by
+      subst hW
+      simp only [wkSpE, substSpE]
+      rw [castSpE_cons]
+      simp only [wkSpE]
+      rw [substSpE_wkSpE x y sp₀ v _ rfl, substNfE_wkNfE x y v₀ v _ rfl]
+  termination_by _ _ b _ _ _ _ sp _ _ _ => (kindSize b, 1, spESize sp)
+  decreasing_by
+    all_goals simp only [spESize]
+    all_goals (apply Prod.Lex.right; apply Prod.Lex.right; omega)
+
+  /-- Weakening distributes over the spine fold. -/
+  theorem wkNfE_appSpE : {Γ : Ctx} → {cw aH j : Kind} → (w : Var Γ cw) →
+      (F : NfE (rem w) aH) → (SP : SpE (rem w) aH j) →
+      wkNfE w (appSpE F SP) = appSpE (wkNfE w F) (wkSpE w SP)
+    | _, _, _, _, w, F, .nil => by simp [wkSpE, appSpE]
+    | _, _, _, _, w, F, .cons (b := bT) SP v => by
+      rw [appSpE_cons]
+      simp only [wkSpE]
+      rw [appSpE_cons, ← wkNfE_appSpE w F SP]
+      cases appSpE F SP with
+      | lam T =>
+        simp only [nappE, wkNfE]
+        exact (substNfE_wkNfE (Var.vs (k' := bT) w) .vz T v (wkNfE w v) rfl).symm
+  termination_by _ _ aH _ _ _ SP => (kindSize aH, 0, spESize SP)
+  decreasing_by
+    all_goals simp only [spESize]
+    all_goals first
+      | (apply Prod.Lex.right; apply Prod.Lex.right; omega)
+      | (apply Prod.Lex.left
+         have h := spEKindLe SP
+         simp only [kindSize] at h ⊢
+         omega)
+end
+
+/-- Weakening distributes over `nappE`. -/
+theorem wkNfE_nappE : {Γ : Ctx} → {cw a b : Kind} → (w : Var Γ cw) →
+    (F : NfE (rem w) (.arr a b)) → (A : NfE (rem w) a) →
+    wkNfE w (nappE F A) = nappE (wkNfE w F) (wkNfE w A)
+  | _, _, a, _, w, .lam T, A => by
+    simp only [nappE, wkNfE]
+    exact (substNfE_wkNfE (Var.vs (k' := a) w) .vz T A (wkNfE w A) rfl).symm
+
+/-- The `vz`-instance of the exchange: substituting past a fresh top slot.
+    Both casts are diagonal (`remSwap .vz y` relates `rem y` to itself), so
+    the statement is cast-free. -/
+theorem substNfE_wkNfE_vz {Γ : Ctx} {c k j : Kind} (X : Var Γ k) (s : NfE Γ j)
+    (u : NfE (rem X) k) :
+    substNfE (wkNfE (.vz (k := c) (Γ := Γ)) s) (.vs X)
+        (wkNfE (.vz (k := c) (Γ := rem X)) u)
+      = wkNfE (.vz (k := c) (Γ := rem X)) (substNfE s X u) :=
+  substNfE_wkNfE (.vz (k := c) (Γ := Γ)) X s u
+    (wkNfE (.vz (k := c) (Γ := rem X)) u) rfl
+
+/-- Spine form of `substNfE_wkNfE_vz`. -/
+theorem substSpE_wkSpE_vz {Γ : Ctx} {c k a j : Kind} (X : Var Γ k) (sp : SpE Γ a j)
+    (u : NfE (rem X) k) :
+    substSpE (wkSpE (.vz (k := c) (Γ := Γ)) sp) (.vs X)
+        (wkNfE (.vz (k := c) (Γ := rem X)) u)
+      = wkSpE (.vz (k := c) (Γ := rem X)) (substSpE sp X u) :=
+  substSpE_wkSpE (.vz (k := c) (Γ := Γ)) X sp u
+    (wkNfE (.vz (k := c) (Γ := rem X)) u) rfl
+
+/-- The `vz`-instance of the weakening exchange: pulling a fresh top slot
+    out past an arbitrary weakening. Both casts are diagonal. -/
+theorem wkNfE_wkNfE_vz {Γ : Ctx} {c k j : Kind} (w : Var Γ k) (t : NfE (rem w) j) :
+    wkNfE (.vs (k' := c) w) (wkNfE (.vz (k := c) (Γ := rem w)) t)
+      = wkNfE (.vz (k := c) (Γ := Γ)) (wkNfE w t) :=
+  wkNfE_wkNfE (.vs (k' := c) w) .vz t
+
+/-- Spine form of `wkNfE_wkNfE_vz`. -/
+theorem wkSpE_wkSpE_vz {Γ : Ctx} {c k a j : Kind} (w : Var Γ k) (sp : SpE (rem w) a j) :
+    wkSpE (.vs (k' := c) w) (wkSpE (.vz (k := c) (Γ := rem w)) sp)
+      = wkSpE (.vz (k := c) (Γ := Γ)) (wkSpE w sp) :=
+  wkSpE_wkSpE (.vs (k' := c) w) .vz sp
+
+end Systemet.L1