diff --git a/LEAN_MIGRATION.md b/LEAN_MIGRATION.md
index 39a66e1..28c8971 100644
--- a/LEAN_MIGRATION.md
+++ b/LEAN_MIGRATION.md
@@ -74,10 +74,10 @@ validate phase by phase.
 ## Status
 
 - [x] Phase 0
-- [ ] Phase 1
-- [ ] Phase 2
-- [ ] Phase 3
-- [ ] Phase 4
+- [x] Phase 1
+- [x] Phase 2
+- [x] Phase 3
+- [x] Phase 4
 - [ ] Phase 5
 - [ ] Phase 6
 - [ ] Phase 7
diff --git a/lean/Spa.lean b/lean/Spa.lean
index a980c3d..1fb1ff1 100644
--- a/lean/Spa.lean
+++ b/lean/Spa.lean
@@ -4,3 +4,5 @@ import Spa.Isomorphism
 import Spa.Lattice.Unit
 import Spa.Lattice.Prod
 import Spa.Lattice.AboveBelow
+import Spa.Lattice.IterProd
+import Spa.Lattice.FiniteMap
diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean
index 589667f..3ddb9a3 100644
--- a/lean/Spa/Lattice.lean
+++ b/lean/Spa/Lattice.lean
@@ -103,6 +103,21 @@ theorem BoundedChains.no_longer {α : Type*} [Preorder α] {n : ℕ}
     (h : BoundedChains α n) (c : LTSeries α) : c.length ≠ n + 1 :=
   fun hc => absurd (h c) (by omega)
 
+/-- Re-index a `FixedHeight` along an equality of heights (used where Agda
+just rewrites with arithmetic identities). -/
+def FixedHeight.cast {α : Type*} [Preorder α] {m n : ℕ} (h : m = n)
+    (fh : FixedHeight α m) : FixedHeight α n where
+  bot := fh.bot
+  top := fh.top
+  longestChain := fh.longestChain
+  head_longestChain := fh.head_longestChain
+  last_longestChain := fh.last_longestChain
+  length_longestChain := h ▸ fh.length_longestChain
+  bounded := h ▸ fh.bounded
+
+@[simp] theorem FixedHeight.cast_bot {α : Type*} [Preorder α] {m n : ℕ}
+    (h : m = n) (fh : FixedHeight α m) : (fh.cast h).bot = fh.bot := rfl
+
 /-- Agda: `IsFiniteHeightLattice` / `FiniteHeightLattice` (bundled). -/
 class FiniteHeightLattice (α : Type*) [Lattice α] where
   height : ℕ
diff --git a/lean/Spa/Lattice/FiniteMap.lean b/lean/Spa/Lattice/FiniteMap.lean
new file mode 100644
index 0000000..50c0209
--- /dev/null
+++ b/lean/Spa/Lattice/FiniteMap.lean
@@ -0,0 +1,666 @@
+/-
+Port of `Lattice/FiniteMap.agda` (and the parts of `Lattice/Map.agda` it was
+built on).
+
+Representation change enabled by dropping the setoid: a finite map over a
+*fixed* key list `ks` is an association list whose key spine is *exactly* `ks`:
+
+    FiniteMap A B ks := { l : List (A × B) // l.map Prod.fst = ks }
+
+Since the spine (including order) is pinned by the type, the representation is
+canonical and propositional equality coincides with the Agda `_≈_` (pointwise
+value equality). The 1100-line `Lattice/Map.agda` — whose unordered-keys
+union/intersection and `Provenance` machinery existed to make `_≈_` workable —
+collapses into the positional `combine` below.
+
+Correspondence (Agda ↦ Lean):
+  FiniteMap, _≈_, ≈-Decidable    ↦ FiniteMap, `=`, DecidableEq instance
+  _⊔_/_⊓_ (via Map union/inter)  ↦ Max/Min via `combine`
+  isUnionSemilattice,
+  isIntersectSemilattice,
+  isLattice, lattice             ↦ instance Lattice (FiniteMap A B ks) (Lattice.mk',
+                                   i.e. the same "two semilattices + absorption" data)
+  _∈_, _∈k_, ∈k-dec, forget      ↦ Membership instance, MemKey (+ Decidable),
+                                   mem_key_of_mem
+  locate                         ↦ locate (computable)
+  all-equal-keys                 ↦ spine_eq
+  ∈k-exclusive                   ↦ immediate from memKey_iff (both sides ↔ k ∈ ks)
+  m₁≼m₂⇒m₁[k]≼m₂[k]              ↦ le_of_mem_mem (takes `ks.Nodup`; the Agda Map
+                                   carried key-uniqueness intrinsically)
+  m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂         ↦ trivial with `=` (congruence)
+  _updating_via_ + Map lemmas:
+    updating-via-keys-≡          ↦ (the `property` field of `updating`)
+    updating-via-∈k-forward      ↦ memKey_updating
+    updating-via-k∈ks            ↦ mem_updating
+    updating-via-k∈ks-≡          ↦ eq_of_mem_updating
+    updating-via-k∉ks-forward    ↦ mem_updating_of_not_mem
+    updating-via-k∉ks-backward   ↦ mem_of_mem_updating
+    f'-Monotonic (Map)           ↦ updating_mono
+  GeneralizedUpdate:
+    f'                           ↦ generalizedUpdate
+    f'-Monotonic                 ↦ generalizedUpdate_monotone
+    f'-∈k-forward                ↦ generalizedUpdate_memKey
+    f'-k∈ks                      ↦ generalizedUpdate_mem
+    f'-k∈ks-≡                    ↦ generalizedUpdate_mem_eq
+    f'-k∉ks-forward, -backward   ↦ generalizedUpdate_not_mem_forward, _backward
+  _[_], []-∈                     ↦ valuesAt, mem_valuesAt (takes `ks.Nodup`)
+  m₁≼m₂⇒m₁[ks]≼m₂[ks]            ↦ valuesAt_le
+  Provenance-union               ↦ mem_sup
+  ⊔-combines                     ↦ (omitted: only used inside the Agda
+                                   isomorphism proofs, which simplified away)
+  IterProdIsomorphism.from/to    ↦ toIter / ofIter — no `Unique ks` needed: the
+                                   spine-pinned representation is already
+                                   canonical, so the isomorphism is exact
+  from/to-preserves-≈, -⊔-distr  ↦ toIter_monotone / ofIter_monotone (with `≼`
+                                   being `≤`, the transport interface consumes
+                                   monotonicity directly)
+  from-to-inverseˡ/ʳ             ↦ toIter_ofIter / ofIter_toIter
+  to-build                       ↦ mem_ofIter_build
+  FixedHeight.fixedHeight        ↦ FiniteMap.fixedHeight (still obtained by
+                                   transport along the IterProd isomorphism)
+  ⊥-contains-bottoms             ↦ bot_contains_bots
+-/
+import Spa.Lattice.IterProd
+import Spa.Isomorphism
+
+namespace Spa
+
+/-- Agda: `FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)`. -/
+def FiniteMap (A B : Type*) (ks : List A) : Type _ :=
+  { l : List (A × B) // l.map Prod.fst = ks }
+
+namespace FiniteMap
+
+variable {A B : Type*} {ks : List A}
+
+instance [DecidableEq A] [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
+  fun a b => decidable_of_iff (a.val = b.val) Subtype.ext_iff.symm
+
+/-- Agda: `all-equal-keys`. -/
+theorem spine_eq (fm₁ fm₂ : FiniteMap A B ks) :
+    fm₁.val.map Prod.fst = fm₂.val.map Prod.fst :=
+  fm₁.property.trans fm₂.property.symm
+
+/-! ### The lattice structure (`combine` replaces Map union/intersection) -/
+
+/-- Positional combination of two maps with equal spines. -/
+def combine (f : B → B → B) (l₁ l₂ : List (A × B)) : List (A × B) :=
+  List.zipWith (fun p q => (p.1, f p.2 q.2)) l₁ l₂
+
+theorem combine_spine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)},
+    l₁.map Prod.fst = l₂.map Prod.fst →
+    (combine f l₁ l₂).map Prod.fst = l₁.map Prod.fst
+  | [], [], _ => rfl
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons, List.map_cons]
+    exact congrArg _ (combine_spine f h.2)
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
+
+theorem combine_comm (f : B → B → B) (hf : ∀ a b, f a b = f b a) :
+    ∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
+      combine f l₁ l₂ = combine f l₂ l₁
+  | [], [], _ => rfl
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons]
+    rw [h.1, hf]
+    exact congrArg _ (combine_comm f hf h.2)
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
+
+theorem combine_assoc (f : B → B → B) (hf : ∀ a b c, f (f a b) c = f a (f b c)) :
+    ∀ {l₁ l₂ l₃ : List (A × B)},
+      l₁.map Prod.fst = l₂.map Prod.fst → l₂.map Prod.fst = l₃.map Prod.fst →
+      combine f (combine f l₁ l₂) l₃ = combine f l₁ (combine f l₂ l₃)
+  | [], [], [], _, _ => rfl
+  | p :: l₁, q :: l₂, r :: l₃, h₁₂, h₂₃ => by
+    simp only [List.map_cons, List.cons.injEq] at h₁₂ h₂₃
+    simp only [combine, List.zipWith_cons_cons]
+    rw [hf]
+    exact congrArg _ (combine_assoc f hf h₁₂.2 h₂₃.2)
+  | [], [], _ :: _, _, h => by simp at h
+  | [], _ :: _, _, h, _ => by simp at h
+  | _ :: _, [], _, h, _ => by simp at h
+  | _ :: _, _ :: _, [], _, h => by simp at h
+
+theorem combine_absorb (f g : B → B → B) (hfg : ∀ a b, f a (g a b) = a) :
+    ∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
+      combine f l₁ (combine g l₁ l₂) = l₁
+  | [], [], _ => rfl
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons, hfg]
+    exact congrArg _ (combine_absorb f g hfg h.2)
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
+
+variable [Lattice B]
+
+instance : Max (FiniteMap A B ks) where
+  max fm₁ fm₂ :=
+    ⟨combine (· ⊔ ·) fm₁.val fm₂.val,
+     (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
+
+instance : Min (FiniteMap A B ks) where
+  min fm₁ fm₂ :=
+    ⟨combine (· ⊓ ·) fm₁.val fm₂.val,
+     (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
+
+@[simp] theorem sup_val (fm₁ fm₂ : FiniteMap A B ks) :
+    (fm₁ ⊔ fm₂).val = combine (· ⊔ ·) fm₁.val fm₂.val := rfl
+
+@[simp] theorem inf_val (fm₁ fm₂ : FiniteMap A B ks) :
+    (fm₁ ⊓ fm₂).val = combine (· ⊓ ·) fm₁.val fm₂.val := rfl
+
+/-- Agda: `isLattice`/`lattice` (built like the Agda record from the two
+semilattices plus absorption; `Lattice.mk'` defines `a ≤ b ↔ a ⊔ b = b`). -/
+instance : Lattice (FiniteMap A B ks) :=
+  Lattice.mk'
+    (fun a b => Subtype.ext (combine_comm _ sup_comm (spine_eq a b)))
+    (fun a b c => Subtype.ext (combine_assoc _ sup_assoc (spine_eq a b) (spine_eq b c)))
+    (fun a b => Subtype.ext (combine_comm _ inf_comm (spine_eq a b)))
+    (fun a b c => Subtype.ext (combine_assoc _ inf_assoc (spine_eq a b) (spine_eq b c)))
+    (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => sup_inf_self) (spine_eq a b)))
+    (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => inf_sup_self) (spine_eq a b)))
+
+/-! ### Membership -/
+
+instance : Membership (A × B) (FiniteMap A B ks) :=
+  ⟨fun fm p => p ∈ fm.val⟩
+
+omit [Lattice B] in
+theorem mem_def {p : A × B} {fm : FiniteMap A B ks} : p ∈ fm ↔ p ∈ fm.val :=
+  Iff.rfl
+
+/-- Agda: `_∈k_`. -/
+def MemKey (k : A) (fm : FiniteMap A B ks) : Prop :=
+  k ∈ fm.val.map Prod.fst
+
+omit [Lattice B] in
+/-- A key is in the map iff it is in the (fixed) key list
+(Agda: `∈k-exclusive` becomes a special case). -/
+theorem memKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := by
+  rw [MemKey, fm.property]
+
+/-- Agda: `∈k-dec`. -/
+instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] :
+    Decidable (MemKey k fm) :=
+  decidable_of_iff _ memKey_iff.symm
+
+omit [Lattice B] in
+/-- Agda: `forget`. -/
+theorem mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
+    (h : (k, v) ∈ fm) : MemKey k fm :=
+  List.mem_map_of_mem _ h
+
+section Locate
+
+variable [DecidableEq A]
+
+private def locateList (k : A) :
+    (l : List (A × B)) → k ∈ l.map Prod.fst → {v : B // (k, v) ∈ l}
+  | [], h => absurd h (by simp)
+  | p :: l', h =>
+    if heq : p.1 = k then
+      ⟨p.2, by rw [← heq]; exact List.mem_cons_self ..⟩
+    else
+      let ⟨v, hv⟩ := locateList k l' (by
+        rcases List.mem_cons.mp h with h' | h'
+        · exact absurd h'.symm heq
+        · exact h')
+      ⟨v, List.mem_cons_of_mem _ hv⟩
+
+/-- Agda: `locate`. -/
+def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) :
+    {v : B // (k, v) ∈ fm} :=
+  locateList k fm.val h
+
+end Locate
+
+/-! ### The pointwise order -/
+
+theorem combine_eq_right_iff : ∀ {l₁ l₂ : List (A × B)},
+    l₁.map Prod.fst = l₂.map Prod.fst →
+    (combine (· ⊔ ·) l₁ l₂ = l₂ ↔
+      List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂)
+  | [], [], _ => by simp [combine]
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons, List.cons.injEq,
+               List.forall₂_cons, Prod.ext_iff]
+    rw [show List.zipWith (fun p q : A × B => (p.1, p.2 ⊔ q.2)) l₁ l₂
+          = combine (· ⊔ ·) l₁ l₂ from rfl,
+        combine_eq_right_iff h.2]
+    constructor
+    · rintro ⟨⟨hk, hv⟩, hrest⟩
+      exact ⟨⟨hk, sup_eq_right.mp hv⟩, hrest⟩
+    · rintro ⟨⟨hk, hv⟩, hrest⟩
+      exact ⟨⟨hk, sup_eq_right.mpr hv⟩, hrest⟩
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
+
+/-- The order on finite maps is the pointwise order on values. -/
+theorem le_iff {fm₁ fm₂ : FiniteMap A B ks} :
+    fm₁ ≤ fm₂ ↔
+      List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) fm₁.val fm₂.val := by
+  rw [← sup_eq_right, ← combine_eq_right_iff (spine_eq fm₁ fm₂), Subtype.ext_iff,
+      sup_val]
+
+private theorem forall₂_spine : ∀ {l₁ l₂ : List (A × B)},
+    List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂ →
+    l₁.map Prod.fst = l₂.map Prod.fst
+  | _, _, List.Forall₂.nil => rfl
+  | _, _, List.Forall₂.cons hpq hrest => by
+    simp [List.map_cons, hpq.1, forall₂_spine hrest]
+
+private theorem forall₂_mem_mem {l₁ l₂ : List (A × B)}
+    (hf : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
+    (l₁.map Prod.fst).Nodup →
+    ∀ {k : A} {v₁ v₂ : B}, (k, v₁) ∈ l₁ → (k, v₂) ∈ l₂ → v₁ ≤ v₂ := by
+  induction hf with
+  | nil =>
+    intro _ k v₁ v₂ h₁ _
+    simp at h₁
+  | @cons p q l₁' l₂' hpq hrest ih =>
+    intro hnd k v₁ v₂ h₁ h₂
+    simp only [List.map_cons, List.nodup_cons] at hnd
+    have hspine := forall₂_spine hrest
+    rcases List.mem_cons.mp h₁ with heq₁ | h₁'
+    · rcases List.mem_cons.mp h₂ with heq₂ | h₂'
+      · rw [← heq₁, ← heq₂] at hpq
+        exact hpq.2
+      · exfalso
+        apply hnd.1
+        rw [show p.1 = k from (congrArg Prod.fst heq₁).symm, hspine]
+        exact List.mem_map_of_mem _ h₂'
+    · rcases List.mem_cons.mp h₂ with heq₂ | h₂'
+      · exfalso
+        apply hnd.1
+        rw [hpq.1, show q.1 = k from (congrArg Prod.fst heq₂).symm]
+        exact List.mem_map_of_mem _ h₁'
+      · exact ih hnd.2 h₁' h₂'
+
+/-- Agda: `m₁≼m₂⇒m₁[k]≼m₂[k]`. The `Nodup` hypothesis was carried inside the
+Agda `Map` type. -/
+theorem le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
+    (hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B}
+    (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ :=
+  forall₂_mem_mem (le_iff.mp hle) (fm₁.property.symm ▸ hks) h₁ h₂
+
+/-! ### Provenance of joined values -/
+
+omit [Lattice B] in
+private theorem mem_combine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)} {k : A} {v : B},
+    l₁.map Prod.fst = l₂.map Prod.fst →
+    (k, v) ∈ combine f l₁ l₂ →
+    ∃ v₁ v₂, v = f v₁ v₂ ∧ (k, v₁) ∈ l₁ ∧ (k, v₂) ∈ l₂
+  | [], [], _, _, _, h => by simp [combine] at h
+  | p :: l₁, q :: l₂, k, v, hsp, h => by
+    simp only [List.map_cons, List.cons.injEq] at hsp
+    simp only [combine, List.zipWith_cons_cons] at h
+    rcases List.mem_cons.mp h with heq | h'
+    · injection heq with hk hv
+      exact ⟨p.2, q.2, hv,
+        by rw [hk]; simp,
+        by rw [hk, hsp.1]; simp⟩
+    · obtain ⟨v₁, v₂, hv, h₁, h₂⟩ := mem_combine f hsp.2 h'
+      exact ⟨v₁, v₂, hv, List.mem_cons_of_mem _ h₁, List.mem_cons_of_mem _ h₂⟩
+
+/-- Agda: `Provenance-union` — a binding of a join comes from bindings of both
+maps. -/
+theorem mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
+    (h : (k, v) ∈ fm₁ ⊔ fm₂) :
+    ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ :=
+  mem_combine _ (spine_eq fm₁ fm₂) h
+
+/-! ### Updating (Agda: `_updating_via_` and `GeneralizedUpdate`) -/
+
+section Updating
+
+variable [DecidableEq A]
+
+/-- Agda: `_updating_via_` — for each key in `ks'`, replace its value by `g k`. -/
+def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
+    FiniteMap A B ks :=
+  ⟨fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p), by
+    rw [List.map_map,
+        show (Prod.fst ∘ fun p : A × B => if p.1 ∈ ks' then (p.1, g p.1) else p)
+          = Prod.fst from funext fun p => by by_cases h : p.1 ∈ ks' <;> simp [h]]
+    exact fm.property⟩
+
+omit [Lattice B] in
+@[simp] theorem updating_val (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
+    (updating fm ks' g).val
+      = fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p) := rfl
+
+omit [Lattice B] in
+/-- Agda: `updating-via-∈k-forward` (strengthened to an iff). -/
+theorem memKey_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B} :
+    MemKey k (updating fm ks' g) ↔ MemKey k fm := by
+  rw [memKey_iff, memKey_iff]
+
+omit [Lattice B] in
+/-- Agda: `updating-via-k∈ks-≡`. -/
+theorem eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
+    {ks' : List A} {g : A → B} (hk : k ∈ ks')
+    (h : (k, v) ∈ updating fm ks' g) : v = g k := by
+  obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
+  by_cases hmem : p.1 ∈ ks'
+  · rw [if_pos hmem] at heq
+    injection heq with h1 h2
+    rw [← h2, h1]
+  · rw [if_neg hmem] at heq
+    rw [heq] at hmem
+    exact absurd hk hmem
+
+omit [Lattice B] in
+/-- Agda: `updating-via-k∈ks`. -/
+theorem mem_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B}
+    (hk : k ∈ ks') (hmem : MemKey k fm) : (k, g k) ∈ updating fm ks' g := by
+  obtain ⟨v, hv⟩ := locate hmem
+  exact List.mem_map.mpr ⟨(k, v), hv, by simp [hk]⟩
+
+omit [Lattice B] in
+/-- Agda: `updating-via-k∉ks-forward`. -/
+theorem mem_updating_of_not_mem {k : A} {v : B} {fm : FiniteMap A B ks}
+    {ks' : List A} {g : A → B} (hk : k ∉ ks') (h : (k, v) ∈ fm) :
+    (k, v) ∈ updating fm ks' g :=
+  List.mem_map.mpr ⟨(k, v), h, by simp [hk]⟩
+
+omit [Lattice B] in
+/-- Agda: `updating-via-k∉ks-backward`. -/
+theorem mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
+    {ks' : List A} {g : A → B} (hk : k ∉ ks')
+    (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
+  obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
+  by_cases hmem : p.1 ∈ ks'
+  · rw [if_pos hmem] at heq
+    injection heq with h1 _
+    rw [← h1] at hk
+    exact absurd hmem hk
+  · rw [if_neg hmem] at heq
+    exact heq ▸ hp
+
+private theorem updating_mono_list {ks' : List A} {g₁ g₂ : A → B}
+    (hg : ∀ k, g₁ k ≤ g₂ k) {l₁ l₂ : List (A × B)}
+    (hl : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
+    List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2)
+      (l₁.map fun p => if p.1 ∈ ks' then (p.1, g₁ p.1) else p)
+      (l₂.map fun p => if p.1 ∈ ks' then (p.1, g₂ p.1) else p) := by
+  induction hl with
+  | nil => exact List.Forall₂.nil
+  | @cons x y l₁' l₂' hpq hrest ih =>
+    simp only [List.map_cons]
+    refine List.Forall₂.cons ?_ ih
+    obtain ⟨hk, hv⟩ := hpq
+    by_cases h : x.1 ∈ ks'
+    · rw [if_pos h, if_pos (hk ▸ h)]
+      exact ⟨hk, hk ▸ hg x.1⟩
+    · rw [if_neg h, if_neg (fun hy => h (hk.symm ▸ hy))]
+      exact ⟨hk, hv⟩
+
+/-- Agda: `f'-Monotonic` at the `Map` level. -/
+theorem updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A}
+    {g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
+    updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
+  rw [le_iff] at hfm ⊢
+  simp only [updating_val]
+  exact updating_mono_list hg hfm
+
+end Updating
+
+section GeneralizedUpdate
+
+/-! Agda: `GeneralizedUpdate` (the "Exercise 4.26" construction). -/
+
+variable [DecidableEq A] {L : Type*} [Lattice L]
+
+/-- Agda: `GeneralizedUpdate.f'`. -/
+def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
+    (ks' : List A) (l : L) : FiniteMap A B ks :=
+  (f l).updating ks' (fun k => g k l)
+
+variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}
+
+/-- Agda: `f'-Monotonic`. -/
+theorem generalizedUpdate_monotone (hf : Monotone f)
+    (hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') :=
+  fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl)
+
+omit [Lattice B] [Lattice L] in
+/-- Agda: `f'-∈k-forward`. -/
+theorem generalizedUpdate_memKey {k : A} {l : L}
+    (h : MemKey k (f l)) : MemKey k (generalizedUpdate f g ks' l) := by
+  unfold generalizedUpdate
+  exact memKey_updating.mpr h
+
+omit [Lattice B] [Lattice L] in
+/-- Agda: `f'-k∈ks`. -/
+theorem generalizedUpdate_mem {k : A} {l : L} (hk : k ∈ ks')
+    (h : MemKey k (f l)) : (k, g k l) ∈ generalizedUpdate f g ks' l := by
+  unfold generalizedUpdate
+  exact mem_updating hk h
+
+omit [Lattice B] [Lattice L] in
+/-- Agda: `f'-k∈ks-≡`. -/
+theorem generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
+    (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l := by
+  unfold generalizedUpdate at h
+  exact eq_of_mem_updating (g := fun k => g k l) hk h
+
+omit [Lattice B] [Lattice L] in
+/-- Agda: `f'-k∉ks-forward`. -/
+theorem generalizedUpdate_not_mem_forward {k : A} {v : B} {l : L} (hk : k ∉ ks')
+    (h : (k, v) ∈ f l) : (k, v) ∈ generalizedUpdate f g ks' l := by
+  unfold generalizedUpdate
+  exact mem_updating_of_not_mem hk h
+
+omit [Lattice B] [Lattice L] in
+/-- Agda: `f'-k∉ks-backward`. -/
+theorem generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks')
+    (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l := by
+  unfold generalizedUpdate at h
+  exact mem_of_mem_updating hk h
+
+end GeneralizedUpdate
+
+/-! ### Reading off values at a list of keys (Agda: `_[_]`) -/
+
+section ValuesAt
+
+variable [DecidableEq A]
+
+private def lookup? (k : A) : List (A × B) → Option B
+  | [] => none
+  | p :: l' => if p.1 = k then some p.2 else lookup? k l'
+
+/-- Agda: `_[_]`. -/
+def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B :=
+  ks'.filterMap (fun k => lookup? k fm.val)
+
+omit [Lattice B] in
+private theorem lookup?_eq_some_of_mem : ∀ {l : List (A × B)},
+    (l.map Prod.fst).Nodup → ∀ {k : A} {v : B}, (k, v) ∈ l →
+    lookup? k l = some v
+  | [], _, _, _, h => by simp at h
+  | p :: l', hnd, k, v, h => by
+    simp only [List.map_cons, List.nodup_cons] at hnd
+    rcases List.mem_cons.mp h with heq | h'
+    · rw [← heq]
+      simp [lookup?]
+    · rw [lookup?, if_neg ?_]
+      · exact lookup?_eq_some_of_mem hnd.2 h'
+      · intro hpk
+        subst hpk
+        have := List.mem_map_of_mem Prod.fst h'
+        exact hnd.1 this
+
+omit [Lattice B] in
+/-- Agda: `[]-∈`. -/
+theorem mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
+    {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' :=
+  List.mem_filterMap.mpr
+    ⟨k, hk, lookup?_eq_some_of_mem (fm.property.symm ▸ hks) h⟩
+
+private theorem lookup?_forall₂ {l₁ l₂ : List (A × B)}
+    (h : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) (k : A) :
+    Option.Rel (· ≤ ·) (lookup? k l₁) (lookup? k l₂) := by
+  induction h with
+  | nil => exact Option.Rel.none
+  | @cons p q l₁ l₂ hpq hrest ih =>
+    rw [lookup?, lookup?]
+    by_cases hc : q.1 = k
+    · rw [if_pos hc, if_pos (hpq.1.trans hc)]
+      exact Option.Rel.some hpq.2
+    · rw [if_neg hc, if_neg (fun hp => hc (hpq.1 ▸ hp))]
+      exact ih
+
+/-- Agda: `m₁≼m₂⇒m₁[ks]≼m₂[ks]`. -/
+theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
+    (ks' : List A) :
+    List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
+  induction ks' with
+  | nil => exact List.Forall₂.nil
+  | cons k ks'' ih =>
+    have hrel := lookup?_forall₂ (le_iff.mp hle) k
+    rw [valuesAt, valuesAt, List.filterMap_cons, List.filterMap_cons]
+    revert hrel
+    generalize lookup? k fm₁.val = o₁
+    generalize lookup? k fm₂.val = o₂
+    intro hrel
+    cases hrel with
+    | none => simpa [valuesAt] using ih
+    | some hv => exact List.Forall₂.cons hv (by simpa [valuesAt] using ih)
+
+end ValuesAt
+
+/-! ### The isomorphism with `IterProd` and the fixed height -/
+
+section Iso
+
+omit [Lattice B] in
+theorem val_ne_nil {k : A} {ks' : List A} (fm : FiniteMap A B (k :: ks')) :
+    fm.val ≠ [] := fun h => by
+  have hp := fm.property
+  rw [h] at hp
+  simp at hp
+
+def headVal {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → B
+  | ⟨[], h⟩ => absurd h (by simp)
+  | ⟨p :: _, _⟩ => p.2
+
+/-- Agda: `pop`. -/
+def pop {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → FiniteMap A B ks'
+  | ⟨[], h⟩ => absurd h (by simp)
+  | ⟨_ :: l, h⟩ =>
+    ⟨l, by simp only [List.map_cons, List.cons.injEq] at h; exact h.2⟩
+
+omit [Lattice B] in
+theorem val_eq_cons {k : A} {ks' : List A} :
+    ∀ fm : FiniteMap A B (k :: ks'), fm.val = (k, fm.headVal) :: fm.pop.val
+  | ⟨[], h⟩ => absurd h (by simp)
+  | ⟨p :: l, h⟩ => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp [headVal, pop, ← h.1]
+
+/-- Agda: `IterProdIsomorphism.from`. -/
+def toIter : {ks : List A} → FiniteMap A B ks → IterProd B PUnit ks.length
+  | [], _ => PUnit.unit
+  | _ :: _, fm => (fm.headVal, toIter fm.pop)
+
+/-- Agda: `IterProdIsomorphism.to` (no `Unique ks` needed: the spine-pinned
+representation is canonical). -/
+def ofIter : (ks : List A) → IterProd B PUnit ks.length → FiniteMap A B ks
+  | [], _ => ⟨[], rfl⟩
+  | k :: ks', ip =>
+    ⟨(k, ip.1) :: (ofIter ks' ip.2).val, by
+      simp [(ofIter ks' ip.2).property]⟩
+
+omit [Lattice B] in
+/-- Agda: `from-to-inverseʳ`. -/
+theorem ofIter_toIter : ∀ {ks : List A} (fm : FiniteMap A B ks),
+    ofIter ks (toIter fm) = fm
+  | [], fm => by
+    obtain ⟨val, hprop⟩ := fm
+    cases val with
+    | nil => rfl
+    | cons p l => exact absurd hprop (by simp)
+  | k :: ks', fm => Subtype.ext (by
+      show (k, fm.headVal) :: (ofIter ks' (toIter fm.pop)).val = fm.val
+      rw [ofIter_toIter fm.pop, ← val_eq_cons fm])
+
+omit [Lattice B] in
+/-- Agda: `from-to-inverseˡ`. -/
+theorem toIter_ofIter : ∀ (ks : List A) (ip : IterProd B PUnit ks.length),
+    toIter (ofIter ks ip) = ip
+  | [], _ => rfl
+  | k :: ks', ip => by
+    show (headVal (ofIter (k :: ks') ip), toIter (pop (ofIter (k :: ks') ip))) = ip
+    rw [show pop (ofIter (k :: ks') ip) = ofIter ks' ip.2 from rfl,
+        toIter_ofIter ks' ip.2]
+    rfl
+
+theorem headVal_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
+    (h : fm₁ ≤ fm₂) : fm₁.headVal ≤ fm₂.headVal := by
+  have h' := le_iff.mp h
+  rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
+  exact (List.forall₂_cons.mp h').1.2
+
+theorem pop_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
+    (h : fm₁ ≤ fm₂) : fm₁.pop ≤ fm₂.pop := by
+  rw [le_iff]
+  have h' := le_iff.mp h
+  rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
+  exact (List.forall₂_cons.mp h').2
+
+/-- Agda: `from-preserves-≈` and `from-⊔-distr` (see header note). -/
+theorem toIter_monotone : ∀ {ks : List A},
+    Monotone (toIter : FiniteMap A B ks → IterProd B PUnit ks.length)
+  | [] => fun _ _ _ => le_refl _
+  | _ :: _ => fun _ _ h =>
+    Prod.mk_le_mk.mpr ⟨headVal_le h, toIter_monotone (pop_le h)⟩
+
+/-- Agda: `to-preserves-≈` and `to-⊔-distr` (see header note). -/
+theorem ofIter_monotone : ∀ (ks : List A), Monotone (ofIter (A := A) (B := B) ks)
+  | [] => fun _ _ _ => le_refl _
+  | k :: ks' => fun ip₁ ip₂ h => by
+    rw [le_iff]
+    show List.Forall₂ _ ((k, ip₁.1) :: (ofIter ks' ip₁.2).val)
+                        ((k, ip₂.1) :: (ofIter ks' ip₂.2).val)
+    exact List.Forall₂.cons ⟨rfl, h.1⟩ (le_iff.mp (ofIter_monotone ks' h.2))
+
+/-- Agda: `FixedHeight.fixedHeight` — a finite map into a lattice of height
+`hB` has height `|ks| · hB`, by transport along the `IterProd` isomorphism. -/
+def fixedHeight {hB : ℕ} (fhB : FixedHeight B hB) (ks : List A) :
+    FixedHeight (FiniteMap A B ks) (ks.length * hB) :=
+  ((IterProd.fixedHeight fhB punitFixedHeight ks.length).transport
+      (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
+      (toIter_ofIter ks) (fun fm => ofIter_toIter fm)).cast (by ring)
+
+omit [Lattice B] in
+/-- Agda: `to-build`. -/
+theorem mem_ofIter_build {b : B} : ∀ {ks : List A} {k : A} {v : B},
+    (k, v) ∈ ofIter ks (IterProd.build b PUnit.unit ks.length) → v = b
+  | [], _, _, h => by simp [ofIter, mem_def] at h
+  | k' :: ks', k, v, h => by
+    rcases List.mem_cons.mp h with heq | h'
+    · exact (Prod.ext_iff.mp heq).2
+    · exact mem_ofIter_build h'
+
+/-- Agda: `⊥-contains-bottoms`. -/
+theorem bot_contains_bots {hB : ℕ} (fhB : FixedHeight B hB) {k : A} {v : B}
+    (h : (k, v) ∈ (fixedHeight fhB ks).bot) : v = fhB.bot := by
+  have hbot : (fixedHeight fhB ks).bot
+      = ofIter ks (IterProd.build fhB.bot PUnit.unit ks.length) := by
+    show ofIter ks (IterProd.fixedHeight fhB punitFixedHeight ks.length).bot = _
+    rw [IterProd.bot_fixedHeight]
+  rw [hbot] at h
+  exact mem_ofIter_build h
+
+end Iso
+
+end FiniteMap
+
+end Spa
diff --git a/lean/Spa/Lattice/IterProd.lean b/lean/Spa/Lattice/IterProd.lean
new file mode 100644
index 0000000..967cdf3
--- /dev/null
+++ b/lean/Spa/Lattice/IterProd.lean
@@ -0,0 +1,76 @@
+/-
+Port of `Lattice/IterProd.agda`: the `k`-fold product `A × (A × ⋯ × B)`.
+
+With propositional equality and typeclasses, the Agda `Everything` record
+(which threaded the lattice operations and the conditional fixed-height proof
+through one recursion, so that the operations built by separate recursions
+would agree) is no longer needed: the `Lattice` instance is one recursive
+definition, and the fixed-height structure is another recursion over it.
+
+Correspondence:
+  IterProd            ↦ Spa.IterProd
+  build               ↦ Spa.IterProd.build
+  isLattice/lattice   ↦ instance Spa.IterProd.instLattice
+  fixedHeight,
+  isFiniteHeightLattice,
+  finiteHeightLattice ↦ Spa.IterProd.fixedHeight (+ FiniteHeightLattice instance)
+  ⊥-built             ↦ Spa.IterProd.bot_fixedHeight
+-/
+import Spa.Lattice.Prod
+import Spa.Lattice.Unit
+import Mathlib.Tactic.Ring
+
+namespace Spa
+
+universe u
+
+/-- Agda: `IterProd k = iterate k (A × ·) B`. (As in the Agda module, `A` and
+`B` are constrained to the same universe to keep the recursion simple.) -/
+def IterProd (A B : Type u) : ℕ → Type u
+  | 0 => B
+  | k + 1 => A × IterProd A B k
+
+namespace IterProd
+
+variable {A B : Type u}
+
+instance instLattice [Lattice A] [Lattice B] :
+    ∀ k, Lattice (IterProd A B k)
+  | 0 => inferInstanceAs (Lattice B)
+  | k + 1 => @Prod.instLattice A (IterProd A B k) _ (instLattice k)
+
+instance instDecidableEq [DecidableEq A] [DecidableEq B] :
+    ∀ k, DecidableEq (IterProd A B k)
+  | 0 => inferInstanceAs (DecidableEq B)
+  | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (instDecidableEq k)
+
+/-- Agda: `build`. -/
+def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
+  | 0 => b
+  | k + 1 => (a, build a b k)
+
+variable [Lattice A] [Lattice B]
+
+/-- Agda: `fixedHeight` (the `isFiniteHeightIfSupported` recursion). -/
+def fixedHeight {hA hB : ℕ} (fhA : FixedHeight A hA) (fhB : FixedHeight B hB) :
+    (k : ℕ) → FixedHeight (IterProd A B k) (k * hA + hB)
+  | 0 => fhB.cast (by ring)
+  | k + 1 => (fhA.prod (fixedHeight fhA fhB k)).cast (by ring)
+
+/-- Agda: `⊥-built` — the bottom of the iterated product is built from the
+component bottoms. -/
+theorem bot_fixedHeight {hA hB : ℕ} (fhA : FixedHeight A hA) (fhB : FixedHeight B hB) :
+    ∀ k, (fixedHeight fhA fhB k).bot = build fhA.bot fhB.bot k
+  | 0 => rfl
+  | k + 1 => by
+    show (fhA.bot, (fixedHeight fhA fhB k).bot) = (fhA.bot, build fhA.bot fhB.bot k)
+    rw [bot_fixedHeight fhA fhB k]
+
+instance [IA : FiniteHeightLattice A] [IB : FiniteHeightLattice B] (k : ℕ) :
+    FiniteHeightLattice (IterProd A B k) where
+  height := k * IA.height + IB.height
+  fixedHeight := fixedHeight IA.fixedHeight IB.fixedHeight k
+
+end IterProd
+
+end Spa
diff --git a/lean/Spa/Lattice/Unit.lean b/lean/Spa/Lattice/Unit.lean
index 3e7cc22..7ca7ec8 100644
--- a/lean/Spa/Lattice/Unit.lean
+++ b/lean/Spa/Lattice/Unit.lean
@@ -17,16 +17,19 @@ theorem boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton 
   push_neg at hc
   exact (c.step ⟨0, by omega⟩).ne (Subsingleton.elim _ _)
 
-/-- Agda: `Lattice/Unit.agda`'s `fixedHeight`/`isFiniteHeightLattice`. -/
+/-- Agda: `Lattice/Unit.agda`'s `fixedHeight`. -/
+def punitFixedHeight : FixedHeight PUnit 0 where
+  bot := PUnit.unit
+  top := PUnit.unit
+  longestChain := RelSeries.singleton _ PUnit.unit
+  head_longestChain := rfl
+  last_longestChain := rfl
+  length_longestChain := rfl
+  bounded := boundedChains_of_subsingleton PUnit 0
+
+/-- Agda: `Lattice/Unit.agda`'s `isFiniteHeightLattice`. -/
 instance : FiniteHeightLattice PUnit where
   height := 0
-  fixedHeight :=
-    { bot := PUnit.unit
-      top := PUnit.unit
-      longestChain := RelSeries.singleton _ PUnit.unit
-      head_longestChain := rfl
-      last_longestChain := rfl
-      length_longestChain := rfl
-      bounded := boundedChains_of_subsingleton PUnit 0 }
+  fixedHeight := punitFixedHeight
 
 end Spa