diff --git a/lake-manifest.json b/lake-manifest.json
index 418f10db..ad8d4b81 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9371548b6ac4467fea4dfc675881f6212cc5565d",
+   "rev": "9a599e9f9d787540a9d3a6f6aa5b1c6c4a387127",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "stable",
diff --git a/lean-toolchain b/lean-toolchain
index 2654c20b..96c38be8 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.26.0
\ No newline at end of file
+leanprover/lean4:v4.25.1
\ No newline at end of file
diff --git a/src/Iris/Algebra/CMRA.lean b/src/Iris/Algebra/CMRA.lean
index 4e88f9df..72cdb843 100644
--- a/src/Iris/Algebra/CMRA.lean
+++ b/src/Iris/Algebra/CMRA.lean
@@ -1136,7 +1136,7 @@ theorem inc_iff {ma mb : Option α} :
     · exact .inl Hmc.symm
     · exact .inr ⟨_, Hmc⟩
   · rintro (H|⟨_, _, _, _, (H|⟨z, _⟩)⟩) <;> subst_eqs
-    · exists mb
+    · exists mb; simp [op]
     · exists none; simp [op]; exact H.symm
     · exists some z
 
@@ -1147,7 +1147,7 @@ theorem incN_iff {ma mb : Option α} :
     · exact .inl Hmc.symm
     · exact .inr ⟨_, Hmc⟩
   · rintro (H|⟨_, _, _, _, (H|⟨z, _⟩)⟩) <;> subst_eqs
-    · exists mb
+    · exists mb; simp [op]
     · exists none; simp [op]; exact H.symm
     · exists some z
 
diff --git a/src/Iris/Algebra/COFESolver.lean b/src/Iris/Algebra/COFESolver.lean
index 9e9cacf3..2efa666a 100644
--- a/src/Iris/Algebra/COFESolver.lean
+++ b/src/Iris/Algebra/COFESolver.lean
@@ -131,7 +131,7 @@ protected def Tower.embed (k) : A F k -n> Tower F := by
       rintro a _ eq rfl
       rw [Nat.add_assoc, Nat.add_left_cancel_iff] at eq; subst a
       apply down_up
-    · cases (Nat.lt_or_eq_of_le h₁).resolve_left (h₂ ∘ Nat.lt_succ_iff.1)
+    · cases (Nat.lt_or_eq_of_le h₁).resolve_left (h₂ ∘ Nat.lt_succ.1)
       have {a b} (e₁ : i+1+a = i+1) (e₂ : i+1 = i+b) :
           down F i (eqToHom e₁ (upN F a n)) ≡ downN F b (eqToHom e₂ n) := by
         cases Nat.add_left_cancel (k := 0) e₁; cases Nat.add_left_cancel e₂
diff --git a/src/Iris/BI/Lib/BUpdPlain.lean b/src/Iris/BI/Lib/BUpdPlain.lean
deleted file mode 100644
index b68d7c94..00000000
--- a/src/Iris/BI/Lib/BUpdPlain.lean
+++ /dev/null
@@ -1,116 +0,0 @@
-import Iris.Std
-import Iris.BI
-import Iris.Algebra.Updates
-import Iris.ProofMode.Classes
-import Iris.ProofMode.Tactics
-import Iris.ProofMode.Display
-
-namespace Iris
-open Iris.Std BI
-
-/-! This file contains an alternative version of basic updates.
-
-Namely, this definition is an expression in terms of the plain modality [■],
-which can be used to instanstiate BUpd for any BIPlainly BI.
-
-cf. https://gitlab.mpi-sws.org/iris/iris/merge_requests/211
--/
-
-namespace BUpdPlain
-
-def BUpdPlain [BIBase PROP] [Plainly PROP] (P : PROP) : PROP :=
-  iprop(∀ R, (P -∗ ■ R) -∗ ■ R)
-
-section BupdPlainDef
-
-open OFE
-
-variable [BI PROP] [BIPlainly PROP]
-
-instance BUpdPlain_ne : NonExpansive (BUpdPlain (PROP := PROP)) where
-  ne _ _ _ H := forall_ne fun _ => wand_ne.ne (wand_ne.ne H .rfl) .rfl
-
-theorem BUpdPlain_intro {P : PROP} : P ⊢ BUpdPlain P := by
-  iintro Hp
-  unfold BUpdPlain
-  iintro _ H
-  iapply H
-  iexact Hp
-
-theorem BUpdPlain_mono {P Q : PROP} : (P ⊢ Q) → (BUpdPlain P ⊢ BUpdPlain Q) := by
-  intros H
-  unfold BUpdPlain
-  iintro R HQR
-  iintro Hp
-  have H1 : ⊢ iprop(Q -∗ ■ HQR) -∗ iprop(P -∗ ■ HQR) := by
-    iintro H
-    iintro Hp
-    iapply H
-    apply H
-  iintro ⟨Ha, H2⟩
-  ispecialize Ha HQR
-  iapply Ha
-  iapply H1
-  iexact H2
-
-theorem BUpdPlain_idemp {P : PROP} : BUpdPlain (BUpdPlain P) ⊢ BUpdPlain P := by
-  unfold BUpdPlain
-  iintro Hp R H
-  ispecialize Hp R as HpR
-  iapply HpR
-  iintro Hp
-  ispecialize Hp R as HpR2
-  iapply HpR2
-  iassumption
-
-theorem BUpdPlain_frame_r {P Q : PROP} : BUpdPlain P ∗ Q ⊢ (BUpdPlain iprop(P ∗ Q)) := by
-  unfold BUpdPlain
-  iintro ⟨Hp, Hq⟩ R H
-  ispecialize Hp R as HpR
-  iapply HpR
-  iintro Hp
-  iapply H
-  isplitl [Hp]
-  · iexact Hp
-  · iexact Hq
-
-theorem BUpdPlain_plainly {P : PROP} : BUpdPlain iprop(■ P) ⊢ (■ P) := by
-  unfold BUpdPlain
-  iintro H
-  ispecialize H P as HP
-  iapply HP
-  exact wand_rfl
-
-/- BiBUpdPlainly entails the alternative definition -/
-theorem BUpd_BUpdPlain [BIUpdate PROP] [BIBUpdatePlainly PROP] {P : PROP} : (|==> P) ⊢ BUpdPlain P := by
-  unfold BUpdPlain
-  iintro _ _ _
-  refine BIUpdate.frame_r.trans ?_
-  refine (BIUpdate.mono sep_symm).trans ?_
-  exact (BIUpdate.mono <| wand_elim .rfl).trans bupd_elim
-
--- We get the usual rule for frame preserving updates if we have an [own]
--- connective satisfying the following rule w.r.t. interaction with plainly.
-
-theorem own_updateP [UCMRA M] {own : M → PROP} {x : M} {Φ : M → Prop}
-  (own_updateP_plainly : ∀ (x : M) (Φ : M → Prop) (R : PROP),
-    (x ~~>: Φ) → own x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ own y -∗ ■ R) ⊢ ■ R)
-  (Hup : x ~~>: Φ) :
-    own x ⊢ BUpdPlain iprop(∃ y, ⌜Φ y⌝ ∧ own y) := by
-  iintro Hx
-  unfold BUpdPlain
-  iintro R H
-  iapply own_updateP_plainly x Φ R Hup
-  isplitl [Hx]
-  · iexact Hx
-  iintro y ⌜HΦ⌝
-  iintro Hy
-  iapply H
-  iexists y
-  isplit
-  · ipure_intro
-    exact HΦ
-  · iexact Hy
-
-end BupdPlainDef
-end BUpdPlain
diff --git a/src/Iris/BI/Plainly.lean b/src/Iris/BI/Plainly.lean
index c8b49fb4..a897bd25 100644
--- a/src/Iris/BI/Plainly.lean
+++ b/src/Iris/BI/Plainly.lean
@@ -302,9 +302,6 @@ theorem impl_wand_plainly : (■ P → Q) ⊣⊢ (■ P -∗ Q) :=
 
 end AffineBI
 
-instance plainly_absorbing (P : PROP) : Absorbing iprop(■ P) where
-  absorbing := absorbingly_elim_plainly.1
-
 end PlainlyLaws
 
 end Iris.BI
diff --git a/src/Iris/Examples/Resources.lean b/src/Iris/Examples/Resources.lean
index 9fe30d7f..b3f26e50 100644
--- a/src/Iris/Examples/Resources.lean
+++ b/src/Iris/Examples/Resources.lean
@@ -3,6 +3,7 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
+import Iris.BI
 import Iris.ProofMode
 import Iris.Algebra.IProp
 import Iris.Instances.UPred.Instance
diff --git a/src/Iris/Instances/UPred/Instance.lean b/src/Iris/Instances/UPred/Instance.lean
index ceab2607..3ee48c68 100644
--- a/src/Iris/Instances/UPred/Instance.lean
+++ b/src/Iris/Instances/UPred/Instance.lean
@@ -9,7 +9,6 @@ import Iris.Algebra.OFE
 import Iris.Algebra.CMRA
 import Iris.Algebra.UPred
 import Iris.Algebra.Updates
-import Iris.BI.Lib.BUpdPlain
 
 section UPredInstance
 
@@ -494,45 +493,3 @@ instance : BIAffine (UPred M) := ⟨by infer_instance⟩
 -- TODO: Port derived lemmas
 
 end UPred
-
-section UPredAlt
-
-open BUpdPlain CMRA UPred
-
-/-
-## Compatibility between the UPred model of BUpd and the BUpd construction for generic BIPlainly instances
--/
-
-def BUpdPlain_pred [UCMRA M] (P : UPred M) (y : M) : UPred M where
-  holds k _ := ∃ x'', ✓{k} (x'' • y) ∧ P k x''
-  mono {_} := fun ⟨z, Hz1, Hz2⟩ _ Hn =>
-    ⟨z, validN_of_le Hn Hz1, P.mono Hz2 (incN_refl z) Hn⟩
-
-/-- The alternative definition entails the ordinary basic update -/
-theorem BUpdPlain_bupd [UCMRA M] (P : UPred M) : BUpdPlain P ⊢ |==> P := by
-  intro n x Hx H k y Hkn Hxy
-  refine (H _ ⟨BUpdPlain_pred P y, rfl⟩) k y Hkn Hxy ?_
-  intro _ z _ Hvyz HP
-  refine ⟨z, validN_ne op_commN Hvyz, HP⟩
-
-theorem BUpdPlain_bupd_iff [UCMRA M] (P : UPred M) : BUpdPlain P ⊣⊢ |==> P :=
-  ⟨BUpdPlain_bupd P, BUpd_BUpdPlain⟩
-
-theorem ownM_updateP [UCMRA M] {x : M} {R : UPred M} (Φ : M → Prop) (Hup : x ~~>: Φ) :
-    ownM x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ ownM y -∗ ■ R) ⊢ ■ R := by
-  intro n z Hv ⟨x1, z2, Hx, ⟨z1, Hz1⟩, HR⟩
-  have Hvalid : ✓{n} (x •? some (z1 • z2)) := by
-    show ✓{n} (x • (z1 • z2))
-    refine CMRA.validN_ne ?_ Hv
-    calc z ≡{n}≡ x1 • z2 := Hx
-         _ ≡{n}≡ (x • z1) • z2 := Hz1.op_l
-         _ ≡{n}≡ x • (z1 • z2) := CMRA.assoc.symm.dist
-  have ⟨y, HΦy, Hvalid_y⟩ := Hup n (some (z1 • z2)) Hvalid
-  have Hp := HR (iprop(⌜Φ y⌝ -∗ (UPred.ownM y -∗ ■ R))) ⟨y, rfl⟩
-  refine Hp n z1 (Nat.le_refl _) ?_ HΦy n y (Nat.le_refl _) ?_ (incN_refl y)
-  · exact CMRA.validN_ne CMRA.comm.dist (CMRA.validN_op_right Hvalid)
-  · apply CMRA.validN_ne ?_ Hvalid_y
-    calc y • (z1 • z2) ≡{n}≡ y • (z2 • z1) := CMRA.comm.dist.op_r
-         _ ≡{n}≡ (z2 • z1) • y := CMRA.comm.symm.dist
-
-section UPredAlt
diff --git a/src/Iris/Std.lean b/src/Iris/Std.lean
index b5a3083b..a679e7c8 100644
--- a/src/Iris/Std.lean
+++ b/src/Iris/Std.lean
@@ -1,5 +1,7 @@
 import Iris.Std.Classes
 import Iris.Std.Expr
+import Iris.Std.Heap
+import Iris.Std.HeapInstances
 import Iris.Std.Nat
 import Iris.Std.Prod
 import Iris.Std.Qq
diff --git a/src/Iris/Std/HeapInstances.lean b/src/Iris/Std/HeapInstances.lean
new file mode 100644
index 00000000..70a1ed25
--- /dev/null
+++ b/src/Iris/Std/HeapInstances.lean
@@ -0,0 +1,364 @@
+/-
+Copyright (c) 2025 Alok Singh. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alok Singh
+-/
+
+import Iris.Std.Heap
+import Std.Data.TreeMap
+import Std.Data.ExtTreeMap
+
+/-!
+# Heap Instances for Standard Types
+
+This file provides `Store` and `Heap` instances for standard Lean types.
+
+## Main instances
+
+- `Store` instance for functions `K → V` (total stores)
+- `Heap` instance for functions `K → Option V` (partial stores / heaps)
+- `RepFunStore` and `IsoFunStore` instances for function types
+- `Store` and `Heap` instances for `TreeMap` and `ExtTreeMap`
+
+## Implementation notes
+
+The function type `K → Option V` provides a canonical heap implementation where:
+- `get` is just function application
+- `set` uses function update
+- `empty` returns `fun _ => none`
+- `hmap` and `merge` are defined pointwise
+
+## Constraints
+
+The TreeMap/ExtTreeMap instances require `LawfulEqCmp cmp`, which states that
+`cmp k k' = .eq → k = k'`. This is necessary because TreeMap only guarantees
+key uniqueness up to the comparator—without this constraint, we couldn't prove
+`get (set t k v) k = v` since the stored key might differ from `k`.
+
+-/
+
+namespace Iris.Std
+
+/-! ## Function Store Instance -/
+
+section FunStore
+
+variable {K V : Type _}
+
+/-- Functions form a total store. -/
+instance instStoreFun [DecidableEq K] : Store (K → V) K V where
+  get t k := t k
+  set t k v := fun k' => if k = k' then v else t k'
+  get_set_eq {t k k' v} h := by grind
+  get_set_ne {t k k' v} h := by grind
+
+/-- Functions represent all functions (trivially). -/
+instance instRepFunStoreFun [DecidableEq K] : RepFunStore (K → V) K V where
+  rep _ := True
+  rep_get _ := trivial
+  of_fun f := f.val
+  get_of_fun := rfl
+
+/-- Functions are isomorphic to themselves. -/
+instance instIsoFunStoreFun [DecidableEq K] : IsoFunStore (K → V) K V where
+  of_fun_get := rfl
+
+end FunStore
+
+/-! ## Function Heap Instance -/
+
+section FunHeap
+
+variable {K V : Type _} [DecidableEq K]
+
+/-- Functions to Option form a heap. -/
+instance instHeapFun : Heap (K → Option V) K V where
+  empty := fun _ => none
+  hmap f t k := (t k).bind (f k)
+  merge op t1 t2 k := Option.merge op (t1 k) (t2 k)
+  get_empty := rfl
+  get_hmap := rfl
+  get_merge := rfl
+
+end FunHeap
+
+end Iris.Std
+
+/-! ## TreeMap Heap Instance -/
+
+namespace Std.TreeMap
+
+section HeapInstance
+
+variable {K V : Type _} {cmp : K → K → Ordering}
+
+variable [TransCmp cmp]
+
+/-- TreeMap forms a Store with Option values.
+
+Note: This requires that `cmp k k' = .eq` implies `k = k'` (i.e., `LawfulEqCmp`).
+-/
+instance instStore [LawfulEqCmp cmp] : Store (TreeMap K V cmp) K (Option V) where
+  get t k := t[k]?
+  set t k v := t.alter k (fun _ => v)
+  get_set_eq {t k k' v} h := by grind
+  get_set_ne {t k k' v} h := by simp [getElem?_alter]; grind
+
+/-! ### Connection to List foldl -/
+
+open Std.DTreeMap.Internal in
+private theorem get?_foldl_alter_impl_sigma [inst : Ord K] [TransOrd K]
+    {l : List ((a : K) × (fun _ => V) a)}
+    {init : Impl K (fun _ => V)} {f : K → V → V → V} {k : K}
+    (hinit : init.WF)
+    (hl : l.Pairwise (fun a b => compare a.1 b.1 ≠ .eq)) :
+    Impl.Const.get? (l.foldl (fun acc kv =>
+        Impl.Const.alter! kv.1 (fun
+          | none => some kv.2
+          | some v1 => some (f kv.1 v1 kv.2)) acc) init) k =
+      match Impl.Const.get? init k, l.find? (fun kv => compare kv.1 k == .eq) with
+      | some v1, some kv2 => some (f kv2.1 v1 kv2.2)
+      | some v1, none => some v1
+      | none, some kv2 => some kv2.2
+      | none, none => none := by
+  induction l generalizing init with
+  | nil =>
+    simp only [List.foldl_nil, List.find?_nil]
+    cases Impl.Const.get? init k <;> rfl
+  | cons hd tl ih =>
+    simp only [List.foldl_cons]
+    let alterFn : Option V → Option V := fun
+      | none => some hd.2
+      | some v1 => some (f hd.1 v1 hd.2)
+    have hwf_new : (Impl.Const.alter! hd.1 alterFn init).WF :=
+      Impl.WF.constAlter! (f := alterFn) hinit
+    rw [ih hwf_new (hl.tail)]
+    by_cases heq : compare hd.1 k = .eq
+    · rw [Impl.Const.get?_alter! hinit]
+      simp only [heq, ↓reduceIte, List.find?_cons, beq_self_eq_true]
+      have htl : tl.find? (fun kv => compare kv.1 k == .eq) = none := List.find?_eq_none.mpr fun kv hkv hkv_eq => by
+        simp only [beq_iff_eq] at hkv_eq
+        exact List.rel_of_pairwise_cons hl hkv (TransCmp.eq_trans heq (OrientedCmp.eq_symm hkv_eq))
+      rw [htl, ← Impl.Const.get?_congr hinit heq]
+      cases Impl.Const.get? init hd.1 <;> simp [alterFn]
+    · rw [Impl.Const.get?_alter! hinit]; simp [heq]
+
+/-- Helper lemma: foldl over list with alter has the expected getElem? behavior.
+    This is the key induction lemma for proving getElem?_mergeWith. -/
+theorem foldl_alter_getElem? {l : List (K × V)} {init : TreeMap K V cmp} {f : K → V → V → V}
+    {k : K} (hl : l.Pairwise (fun a b => cmp a.1 b.1 ≠ .eq)) :
+    (l.foldl (fun acc kv => acc.alter kv.1 fun
+        | none => some kv.2
+        | some v1 => some (f kv.1 v1 kv.2)) init)[k]? =
+      match init[k]?, l.find? (fun kv => cmp kv.1 k == .eq) with
+      | some v1, some kv2 => some (f kv2.1 v1 kv2.2)
+      | some v1, none => some v1
+      | none, some kv2 => some kv2.2
+      | none, none => none := by
+  induction l generalizing init with
+  | nil =>
+    simp only [List.foldl_nil, List.find?_nil]
+    cases init[k]? <;> rfl
+  | cons hd tl ih =>
+    simp only [List.foldl_cons]
+    rw [ih (hl.tail)]
+    by_cases heq : cmp hd.1 k = .eq
+    · -- hd.1 matches k
+      simp only [getElem?_alter, getElem?_congr (OrientedCmp.eq_symm heq), List.find?_cons, heq, beq_self_eq_true]
+      have htl : tl.find? (fun kv => cmp kv.1 k == .eq) = none := List.find?_eq_none.mpr fun kv hkv hkv_eq => by
+        simp only [beq_iff_eq] at hkv_eq
+        exact List.rel_of_pairwise_cons hl hkv (TransCmp.eq_trans heq (OrientedCmp.eq_symm hkv_eq))
+      simp only [htl, ReflCmp.compare_self, ↓reduceIte]
+      cases init[hd.1]? <;> rfl
+    · -- hd.1 doesn't match k
+      simp [getElem?_alter, heq]
+
+/-- `find?` commutes with mapping sigma types to product types. -/
+theorem find?_map_sigma {α : Type _} {β : α → Type _} {γ : Type _}
+    {l : List ((a : α) × β a)} {p : α × γ → Bool} {f : (e : (a : α) × β a) → γ} :
+    (l.map (fun e => (e.1, f e))).find? p =
+      (l.find? (p ∘ fun e => (e.1, f e))).map (fun e => (e.1, f e)) := by
+  induction l with
+  | nil => rfl
+  | cons hd tl ih => simp only [List.map_cons, List.find?_cons, Function.comp]; split <;> simp_all
+
+/-- TreeMap.mergeWith equals list foldl with alter at the getElem? level. -/
+theorem getElem?_mergeWith_eq_foldl [LawfulEqCmp cmp] {t₁ t₂ : TreeMap K V cmp}
+    {f : K → V → V → V} {k : K} :
+    (t₁.mergeWith f t₂)[k]? = (t₂.toList.foldl (fun acc kv =>
+        acc.alter kv.1 fun | none => some kv.2 | some v1 => some (f kv.1 v1 kv.2)) t₁)[k]? := by
+  rw [foldl_alter_getElem? (distinct_keys_toList (t := t₂))]
+  letI : Ord K := ⟨cmp⟩
+
+  have h_impl : (t₁.mergeWith f t₂)[k]? =
+      Std.DTreeMap.Internal.Impl.Const.get?
+        (Std.DTreeMap.Internal.Impl.Const.mergeWith! f t₁.inner.inner t₂.inner.inner) k :=
+    congrArg (Std.DTreeMap.Internal.Impl.Const.get? · k)
+      (Std.DTreeMap.Internal.Impl.Const.mergeWith_eq_mergeWith! ..)
+
+  have h_foldl : Std.DTreeMap.Internal.Impl.Const.mergeWith! f t₁.inner.inner t₂.inner.inner =
+      Std.DTreeMap.Internal.Impl.foldl (fun t a b₂ =>
+        Std.DTreeMap.Internal.Impl.Const.alter! a (fun
+          | none => some b₂
+          | some b₁ => some (f a b₁ b₂)) t) t₁.inner.inner t₂.inner.inner := rfl
+
+  have h_list : Std.DTreeMap.Internal.Impl.foldl (fun t a b₂ =>
+        Std.DTreeMap.Internal.Impl.Const.alter! a (fun
+          | none => some b₂
+          | some b₁ => some (f a b₁ b₂)) t) t₁.inner.inner t₂.inner.inner =
+      t₂.inner.inner.toListModel.foldl (fun acc p =>
+        Std.DTreeMap.Internal.Impl.Const.alter! p.1 (fun
+          | none => some p.2
+          | some b₁ => some (f p.1 b₁ p.2)) acc) t₁.inner.inner := by
+    rw [Std.DTreeMap.Internal.Impl.foldl_eq_foldl]
+
+  have hdist : t₂.inner.inner.toListModel.Pairwise (fun a b => compare a.1 b.1 ≠ .eq) :=
+    (List.pairwise_map.mp <|
+      Std.DTreeMap.Internal.Impl.SameKeys.ordered_iff_pairwise_keys.mp t₂.inner.wf.ordered).imp
+      fun hlt heq => nomatch heq ▸ hlt
+
+  -- Connect t₁[k]? with the internal get?
+  have h_get_eq : t₁[k]? = Std.DTreeMap.Internal.Impl.Const.get? t₁.inner.inner k := rfl
+
+  rw [h_impl, h_foldl, h_list, get?_foldl_alter_impl_sigma t₁.inner.wf hdist, h_get_eq]
+
+  have h_toList : t₂.toList = t₂.inner.inner.toListModel.map (fun e => (e.1, e.2)) :=
+    Std.DTreeMap.Internal.Impl.Const.toList_eq_toListModel_map
+
+  have h_find : ∀ (l : List ((a : K) × (fun _ => V) a)),
+      (l.map (fun e => (e.1, e.2))).find? (fun kv => cmp kv.1 k == .eq) =
+      (l.find? (fun kv => cmp kv.1 k == .eq)).map (fun e => (e.1, e.2)) := by
+    intro l; induction l with
+    | nil => rfl
+    | cons hd tl ih => simp only [List.map_cons, List.find?_cons]; split <;> grind
+
+  have hfind_eq := h_find t₂.inner.inner.toListModel
+  rw [← h_toList] at hfind_eq
+
+  cases hres : t₂.inner.inner.toListModel.find? (fun kv => cmp kv.1 k == .eq) <;>
+    (simp only [hfind_eq, hres, Option.map_none, Option.map_some];
+     cases Std.DTreeMap.Internal.Impl.Const.get? t₁.inner.inner k <;> rfl)
+
+/-- If `k` is not in the map, `find?` on `toList` returns `none`. -/
+theorem find?_eq_none_of_getElem?_eq_none [LawfulEqCmp cmp] {t : TreeMap K V cmp} {k : K}
+    (hget : t[k]? = none) : t.toList.find? (fun kv => cmp kv.1 k == .eq) = none := by
+  apply List.find?_eq_none.mpr; intro kv hkv heq; simp only [beq_iff_eq] at heq
+  exact absurd (getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList.mpr
+    ⟨kv.1, OrientedCmp.eq_symm heq, hkv⟩) (by simp [hget])
+
+/-- If `k` is in the map with value `v`, `find?` returns a matching key-value pair. -/
+theorem find?_eq_some_of_getElem?_eq_some [LawfulEqCmp cmp] {t : TreeMap K V cmp} {k : K} {v : V}
+    (hget : t[k]? = some v) :
+    ∃ kv, t.toList.find? (fun kv => cmp kv.1 k == .eq) = some kv ∧
+      kv.2 = v ∧ cmp kv.1 k = .eq := by
+  obtain ⟨k', hcmp, hmem⟩ := getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList.mp hget
+  have hpred : (fun kv : K × V => cmp kv.1 k == .eq) (k', v) = true :=
+    by simp [OrientedCmp.eq_symm hcmp]
+  have hisSome := List.find?_isSome (p := fun kv => cmp kv.1 k == .eq) |>.mpr ⟨(k', v), hmem, hpred⟩
+  obtain ⟨kv, hfind⟩ := Option.isSome_iff_exists.mp hisSome
+  have hkv_cmp : cmp kv.1 k = .eq := by simpa [beq_iff_eq] using List.find?_some hfind
+  refine ⟨kv, hfind, ?_, hkv_cmp⟩
+  have := getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList.mpr
+    ⟨kv.1, OrientedCmp.eq_symm hkv_cmp, List.mem_of_find?_eq_some hfind⟩
+  grind
+
+/-- getElem? of mergeWith has the expected semantics.
+
+This lemma states that `mergeWith` behaves as expected: it combines two maps such that:
+- If both maps have a key, the merge function is applied
+- If only one map has a key, that value is used
+- If neither has the key, the result is none
+
+The proof uses the internal implementation details of TreeMap.mergeWith, which is
+defined as a foldl over the second tree using alter operations.
+-/
+@[simp] theorem getElem?_mergeWith' [LawfulEqCmp cmp] {t₁ t₂ : TreeMap K V cmp}
+    {f : K → V → V → V} {k : K} :
+    (t₁.mergeWith f t₂)[k]? =
+      match t₁[k]?, t₂[k]? with
+      | some v1, some v2 => some (f k v1 v2)
+      | some v1, none => some v1
+      | none, some v2 => some v2
+      | none, none => none := by
+  have hfoldl := foldl_alter_getElem? (init := t₁) (f := f) (k := k) (distinct_keys_toList (t := t₂))
+  have mergeWith_eq := getElem?_mergeWith_eq_foldl (t₁ := t₁) (t₂ := t₂) (f := f) (k := k)
+  cases h2 : t₂[k]? with
+  | none => cases h1 : t₁[k]? <;> rw [mergeWith_eq, hfoldl, h1, find?_eq_none_of_getElem?_eq_none h2]
+  | some v2 =>
+    obtain ⟨kv, hfind, hval, hcmp⟩ := find?_eq_some_of_getElem?_eq_some h2
+    have heq : kv.1 = k := LawfulEqCmp.eq_of_compare hcmp
+    cases h1 : t₁[k]? <;> (rw [mergeWith_eq, hfoldl, h1, hfind]; subst heq hval; rfl)
+
+/-- TreeMap forms a Heap. -/
+instance instHeap [LawfulEqCmp cmp] : Heap (TreeMap K V cmp) K V where
+  empty := {}
+  hmap f t := t.filterMap f
+  merge op t1 t2 := t1.mergeWith (fun _ v1 v2 => op v1 v2) t2
+  get_empty := rfl
+  get_hmap {f t k} := by
+    show (filterMap f t)[k]? = t[k]?.bind (f k); simp [getElem?_filterMap, Option.pbind_eq_bind, getKey_eq]
+  get_merge {op t1 t2 k} := by
+    show (mergeWith _ t1 t2)[k]? = Option.merge op t1[k]? t2[k]?; simp only [getElem?_mergeWith']; cases t1[k]? <;> cases t2[k]? <;> rfl
+
+end HeapInstance
+
+end Std.TreeMap
+
+/-! ## ExtTreeMap Heap Instance -/
+
+namespace Std.ExtTreeMap
+
+section HeapInstance
+
+variable {K V : Type _} {cmp : K → K → Ordering}
+
+variable [TransCmp cmp]
+
+/-- ExtTreeMap forms a Store with Option values.
+
+Note: This requires that `cmp k k' = .eq` implies `k = k'` (i.e., `LawfulEqCmp`).
+-/
+instance instStore [LawfulEqCmp cmp] : Store (ExtTreeMap K V cmp) K (Option V) where
+  get t k := t[k]?
+  set t k v := t.alter k (fun _ => v)
+  get_set_eq {t k k' v} h := by grind
+  get_set_ne {t k k' v} h := by simp [getElem?_alter]; grind
+
+/-- getElem? of mergeWith has the expected semantics for ExtTreeMap.
+
+The proof uses quotient induction to reduce to DTreeMap representatives,
+then reuses the TreeMap proof since both share the same internal implementation. -/
+@[simp] theorem getElem?_mergeWith' [LawfulEqCmp cmp] {t₁ t₂ : ExtTreeMap K V cmp}
+    {f : K → V → V → V} {k : K} :
+    (t₁.mergeWith f t₂)[k]? =
+      match t₁[k]?, t₂[k]? with
+      | some v1, some v2 => some (f k v1 v2)
+      | some v1, none => some v1
+      | none, some v2 => some v2
+      | none, none => none := by
+  show ExtDTreeMap.Const.get? (ExtDTreeMap.Const.mergeWith f t₁.inner t₂.inner) k =
+    match ExtDTreeMap.Const.get? t₁.inner k, ExtDTreeMap.Const.get? t₂.inner k with
+    | some v1, some v2 => some (f k v1 v2)
+    | some v1, none => some v1
+    | none, some v2 => some v2
+    | none, none => none
+  obtain ⟨q₁⟩ := t₁.inner
+  obtain ⟨q₂⟩ := t₂.inner
+  induction q₁ using Quotient.ind with
+  | _ m₁ => induction q₂ using Quotient.ind with
+    | _ m₂ => exact Std.TreeMap.getElem?_mergeWith' (t₁ := ⟨m₁⟩) (t₂ := ⟨m₂⟩) (f := f) (k := k)
+
+/-- ExtTreeMap forms a Heap. -/
+instance instHeap [LawfulEqCmp cmp] : Heap (ExtTreeMap K V cmp) K V where
+  empty := {}
+  hmap f t := t.filterMap f
+  merge op t1 t2 := t1.mergeWith (fun _ v1 v2 => op v1 v2) t2
+  get_empty := rfl
+  get_hmap {f t k} := by
+    show (filterMap f t)[k]? = t[k]?.bind (f k); simp [getElem?_filterMap, Option.pbind_eq_bind, getKey_eq]
+  get_merge {op t1 t2 k} := by
+    show (mergeWith _ t1 t2)[k]? = Option.merge op t1[k]? t2[k]?; simp only [getElem?_mergeWith']; cases t1[k]? <;> cases t2[k]? <;> rfl
+
+end HeapInstance
+
+end Std.ExtTreeMap