diff --git a/src/Iris/Algebra.lean b/src/Iris/Algebra.lean
index 2fc931d7..94acb87f 100644
--- a/src/Iris/Algebra.lean
+++ b/src/Iris/Algebra.lean
@@ -3,3 +3,5 @@ import Iris.Algebra.CMRA
 import Iris.Algebra.COFESolver
 import Iris.Algebra.OFE
 import Iris.Algebra.Frac
+import Iris.Algebra.Heap
+import Iris.Algebra.Lib
diff --git a/src/Iris/Algebra/CMRA.lean b/src/Iris/Algebra/CMRA.lean
index dd726f91..3a5e6908 100644
--- a/src/Iris/Algebra/CMRA.lean
+++ b/src/Iris/Algebra/CMRA.lean
@@ -183,6 +183,7 @@ theorem op_opM_assoc (x y : α) (mz : Option α) : (x • y) •? mz ≡ x • (
 theorem op_opM_assoc_dist (x y : α) (mz : Option α) : (x • y) •? mz ≡{n}≡ x • (y •? mz) := by
   unfold op?; cases mz <;> simp [assoc.dist, Dist.symm]
 
+
 /-! ## Validity -/
 
 theorem Valid.validN : ✓ (x : α) → ✓{n} x := (valid_iff_validN.1 · _)
@@ -1098,6 +1099,10 @@ theorem CMRA.op_some_opM_assoc (x y : α) (mz : Option α) : (x • y) •? mz 
   | none   => .rfl
   | some _ => assoc.symm
 
+theorem CMRA.opM_opM_assoc {x : α} {y z : Option α} : (x •? y) •? z ≡ x •? (y • z) := by
+  cases y <;> cases z <;> simp [CMRA.op?, CMRA.op, optionOp]
+  exact assoc.symm
+
 theorem CMRA.op_some_opM_assoc_dist (x y : α) (mz : Option α) :
     (x • y) •? mz ≡{n}≡ x •? (some y • mz) :=
   match mz with
@@ -1116,7 +1121,7 @@ theorem CMRA.inc_of_some_inc_some [CMRA.IsTotal α] {x y : α} (h : some y ≼ s
   | none => ⟨core y, (CMRA.equiv_of_some_equiv_some hmz).trans (op_core y).symm⟩
   | some z => ⟨z, hmz⟩
 
-theorem CMRA.incN_of_some_incN_some [CMRA.IsTotal α] {x y : α} : some y ≼{n} some x → y ≼{n} x
+theorem CMRA.incN_of_Option.some_incN_some_iff_some [CMRA.IsTotal α] {x y : α} : some y ≼{n} some x → y ≼{n} x
   | ⟨none, hmz⟩ => ⟨core y, (CMRA.dist_of_some_dist_some hmz).trans (op_core_dist y).symm⟩
   | ⟨some z, hmz⟩ => ⟨z, hmz⟩
 
@@ -1134,6 +1139,163 @@ theorem not_valid_some_exclN_op_left {n} {x : α} [CMRA.Exclusive x] {y : α} :
 theorem validN_op_unit {n} {x : Option α} (vx : ✓{n} x) : ✓{n} x • CMRA.unit := by
   cases x <;> trivial
 
+theorem Option.inc_iff {ma mb : Option α} :
+    ma ≼ mb ↔ ma = none ∨ ∃ a b, ma = some a ∧ mb = some b ∧ (a ≡ b ∨ a ≼ b) := by
+  constructor
+  · rintro ⟨mc, Hmc⟩
+    cases ma <;> cases mb <;> cases mc <;> simp_all [CMRA.op, optionOp]
+    · exact .inl Hmc.symm
+    · right; rename_i v3; exists v3
+  · rintro (H|⟨a, b, Ha, Hb, (H|⟨z, Hz⟩)⟩)
+    · subst H; exists mb; simp [CMRA.op, optionOp]
+    · subst Ha; subst Hb; exists none; simp [CMRA.op, optionOp]; exact H.symm
+    · subst Ha; subst Hb; exists some z
+
+theorem Option.incN_iff {ma mb : Option α} :
+    ma ≼{n} mb ↔ ma = none ∨ ∃ a b, ma = some a ∧ mb = some b ∧ (a ≡{n}≡ b ∨ a ≼{n} b) := by
+  constructor
+  · rintro ⟨mc, Hmc⟩
+    cases ma <;> cases mb <;> cases mc <;> simp_all [CMRA.op, optionOp]
+    · exact .inl Hmc.symm
+    · right; rename_i v3; exists v3
+  · rintro (H|⟨a, b, Ha, Hb, (H|⟨z, Hz⟩)⟩)
+    · subst H; exists mb; simp [CMRA.op, optionOp]
+    · subst Ha; subst Hb; exists none; simp [CMRA.op, optionOp]; exact H.symm
+    · subst Ha; subst Hb; exists some z
+
+theorem Option.inc_iff_isTotal [CMRA.IsTotal α] {ma mb : Option α} :
+    ma ≼ mb ↔ ma = none ∨ ∃ a b, ma = some a ∧ mb = some b ∧ a ≼ b := by
+  apply Option.inc_iff.trans _
+  constructor
+  · rintro (H|⟨a, b, Ha, Hb, (H|H)⟩)
+    · exact .inl H
+    · right
+      refine ⟨a, b, Ha, Hb, ?_⟩
+      exists (CMRA.core a)
+      exact H.symm.trans (CMRA.op_core a).symm
+    · exact .inr ⟨a, b, Ha, Hb, H⟩
+  · rintro (H|⟨a, b, Ha, Hb, H⟩)
+    · exact .inl H
+    · exact .inr ⟨a, b, Ha, Hb, .inr H⟩
+
+theorem Option.incN_iff_isTotal [CMRA.IsTotal α] {ma mb : Option α} :
+    ma ≼{n} mb ↔ ma = none ∨ ∃ a b, ma = some a ∧ mb = some b ∧ a ≼{n} b := by
+  apply Option.incN_iff.trans _
+  constructor
+  · rintro (H|⟨a, b, Ha, Hb, (H|H)⟩)
+    · exact .inl H
+    · right
+      refine ⟨a, b, Ha, Hb, ?_⟩
+      exists (CMRA.core a)
+      apply H.symm.trans (CMRA.op_core_dist a).symm
+    · exact .inr ⟨a, b, Ha, Hb, H⟩
+  · rintro (H|⟨a, b, Ha, Hb, H⟩)
+    · exact .inl H
+    · exact .inr ⟨a, b, Ha, Hb, .inr H⟩
+
+theorem Option.some_incN_some_iff {a b : α} : some a ≼{n} some b ↔ a ≡{n}≡ b ∨ a ≼{n} b := by
+  apply Option.incN_iff.trans; simp
+
+-- Here
+theorem Option.some_inc_some_iff {a b : α} : some a ≼ some b ↔ a ≡ b ∨ a ≼ b := by
+  apply Option.inc_iff.trans; simp
+
+theorem Option.eqv_of_inc_exclusive [CMRA.Exclusive (a : α)] {b : α} (H : some a ≼ some b) (Hv : ✓ b) :
+     a ≡ b := by
+  rcases Option.inc_iff.mp H with (H|⟨a', b', Ha, Hb, H⟩); simp at H
+  simp only [Option.some.injEq] at Ha Hb; subst Ha; subst Hb
+  rcases H with (H|H); trivial
+  exact (CMRA.not_valid_of_excl_inc H Hv).elim
+
+theorem Option.dst_of_inc_exclusive [CMRA.Exclusive (a : α)] {b : α} (H : some a ≼{n} some b) (Hv : ✓{n} b)  :
+    a ≡{n}≡ b := by
+  rcases Option.incN_iff.mp H with (H|⟨a', b', Ha, Hb, H⟩); simp at H
+  simp only [Option.some.injEq] at Ha Hb; subst Ha; subst Hb
+  rcases H with (H|H); trivial
+  exact (CMRA.not_valid_of_exclN_inc H Hv).elim
+
+theorem Option.some_inc_some_iff_isTotal [CMRA.IsTotal α] {a b : α} : some a ≼ some b ↔ a ≼ b := by
+  apply Option.some_inc_some_iff.trans
+  refine ⟨?_, .inr⟩
+  rintro (H|H)
+  · exists (CMRA.core a)
+    exact H.symm.trans (CMRA.op_core a).symm
+  · exact H
+
+theorem Option.some_incN_some_iff_isTotal [CMRA.IsTotal α] {a b : α} : some a ≼{n} some b ↔ a ≼{n} b := by
+  apply Option.some_incN_some_iff.trans
+  refine ⟨?_, .inr⟩
+  rintro (H|H)
+  · exists (CMRA.core a)
+    exact H.symm.trans (CMRA.op_core_dist a).symm
+  · exact H
+
+instance {a : α} [Hid : CMRA.IdFree a] [Hc : CMRA.Cancelable a] : CMRA.Cancelable (some a) := by
+  constructor
+  rintro n (_|b) (_|c) _ HE
+  · trivial
+  · rename_i h
+    simp [CMRA.op, optionOp] at HE
+    exact Hid.id_free0_r c (CMRA.valid0_of_validN h) (HE.symm.le (n.zero_le))
+  · rename_i h
+    simp [CMRA.op, optionOp] at HE
+    apply Hid.id_free0_r b
+    · simp [CMRA.op, optionOp, CMRA.ValidN, optionValidN] at h
+      apply CMRA.valid0_of_validN
+      exact (Dist.validN HE).mp h
+    · apply Dist.le HE (n.zero_le)
+  · simp [OFE.Dist, Option.Forall₂]
+    apply Hc.cancelableN
+    · rename_i h; exact h
+    · apply HE
+
+instance (ma : Option α) [Hid : ∀ a : α, CMRA.IdFree a] [Hc : ∀ a : α, CMRA.Cancelable a] :
+    CMRA.Cancelable ma := by
+  cases ma
+  constructor
+  · simp [CMRA.op, optionOp]
+  · infer_instance
+
+-- Weird that replacing this proof with the #print-ed term doesn't work for some reason
+theorem Option.validN_of_incN_validN {a b : α} (Hv : ✓{n} a) (Hinc : some b ≼{n} some a) : ✓{n} b :=  by
+  apply CMRA.validN_of_incN Hinc
+  apply Hv
+
+-- Same, can't replace with #print-ed term
+theorem Option.valid_of_inc_valid {a b : α} (Hv : ✓ a) (Hinc : some b ≼ some a) : ✓ b :=  by
+  apply CMRA.valid_of_inc Hinc
+  apply Hv
+
+theorem Option.some_inc_some_iff_op? {a b : α} : some a ≼ some b ↔ ∃ mc, b ≡ a •? mc := by
+  simp [Option.inc_iff]
+  constructor
+  · rintro (H|H)
+    · exists none; simpa [CMRA.op?] using H.symm
+    · rcases H with ⟨mc', H⟩
+      exists (some mc')
+  · rintro ⟨(_|z), H⟩
+    · exact .inl H.symm
+    · right; exists z
+
+theorem Option.some_incN_some_iff_op? {a b : α} : some a ≼{n} some b ↔ ∃ mc, b ≡{n}≡ a •? mc := by
+  simp [Option.incN_iff]
+  constructor
+  · rintro (H|H)
+    · exists none; simpa [CMRA.op?] using H.symm
+    · rcases H with ⟨mc', H⟩
+      exists (some mc')
+  · rintro ⟨(_|z), H⟩
+    · exact .inl H.symm
+    · right; exists z
+
+instance [CMRA.Discrete α] : CMRA.Discrete (Option α) where
+  discrete_valid {x} := by
+    cases x <;> simp [CMRA.Valid, optionValid]
+    exact (CMRA.discrete_valid ·)
+
+theorem Option.some_op_op? {a : α} {ma : Option α} : some a • ma = some (a •? ma) := by
+  cases ma <;> simp [CMRA.op?, CMRA.op, optionOp]
+
 end option
 
 section unit
@@ -1232,6 +1394,12 @@ theorem valid_snd {x : α × β} (h : ✓ x) : ✓ x.snd := h.right
 theorem validN_fst {n} {x : α × β} (h : ✓{n} x) : ✓{n} x.fst := h.left
 theorem validN_snd {n} {x : α × β} (h : ✓{n} x) : ✓{n} x.snd := h.right
 
+instance [CMRA.Discrete α] [CMRA.Discrete β]: CMRA.Discrete (α × β) where
+  discrete_valid := by
+    rintro ⟨_, _⟩
+    simp [CMRA.ValidN]
+    exact (⟨CMRA.discrete_valid ·, CMRA.discrete_valid ·⟩)
+
 end Prod
 
 section optionOF
diff --git a/src/Iris/Algebra/DFrac.lean b/src/Iris/Algebra/DFrac.lean
index e578e167..6cadc8fa 100644
--- a/src/Iris/Algebra/DFrac.lean
+++ b/src/Iris/Algebra/DFrac.lean
@@ -7,6 +7,8 @@ Authors: Markus de Medeiros, Mario Carneiro
 import Iris.Algebra.CMRA
 import Iris.Algebra.OFE
 import Iris.Algebra.Frac
+import Iris.Algebra.Updates
+import Iris.Algebra.LocalUpdates
 
 namespace Iris
 
@@ -138,4 +140,66 @@ theorem valid_discard : ✓ (discard : DFrac F) := by simp [CMRA.Valid, valid]
 theorem valid_own_op_discard {q : F} : ✓ own q • discard ↔ Fractional q := by
   simp [CMRA.op, op, CMRA.Valid, valid]
 
+instance : CMRA.Discrete (DFrac F) where
+  discrete_valid {x} := by simp [CMRA.Valid, CMRA.ValidN]
+
+theorem DFrac.is_discrete {q : DFrac F} : OFE.DiscreteE q := ⟨congrArg id⟩
+
+instance : CMRA.Discrete (DFrac F) where
+  discrete_valid {x} := by simp [CMRA.Valid, CMRA.ValidN]
+
+instance : CMRA.Discrete (DFrac F) where
+  discrete_valid {x} := by simp [CMRA.Valid, CMRA.ValidN]
+
+-- dfrac_discard_update
+theorem DFrac.update_discard {dq : DFrac F} : dq ~~> .discard := by
+  rintro n (_|⟨q|_|q⟩) H <;>
+    have H' := (CMRA.valid_iff_validN' n).mpr H <;>
+    apply (CMRA.valid_iff_validN' n).mp <;>
+    simp [CMRA.op?] at H' ⊢
+  · simp [CMRA.Valid, valid]
+  · cases dq
+    · exact valid_op_own H
+    · exact H
+    · exact valid_op_own H
+  · simp [CMRA.Valid, valid, CMRA.op, op]
+  · cases dq
+    · exact CMRA.valid_op_right _ _ H
+    · exact H
+    · exact CMRA.valid_op_right _ _ H
+
+-- dfrac_undiscard_update
+theorem DFrac.update_acquire [IsSplitFraction F] :
+    (.discard : DFrac F) ~~>: fun k => ∃ q, k = .own q := by
+  apply UpdateP.discrete.mpr
+  rintro (_|⟨q|_|q⟩)
+  · rintro _
+    exists (.own One.one)
+    refine ⟨⟨One.one, rfl⟩, ?_⟩
+    simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid, add_comm]
+    apply UFraction.one_whole.1
+  · rintro ⟨q', HP⟩
+    exists (.own q')
+    refine ⟨⟨q', rfl⟩, ?_⟩
+    simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid, add_comm]
+    exact HP
+  · intro _
+    let q' : F := (IsSplitFraction.split One.one).1
+    exists (.own q')
+    refine ⟨⟨q', rfl⟩, ?_⟩
+    simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid]
+    exists (IsSplitFraction.split One.one).2
+    rw [IsSplitFraction.split_add]
+    apply UFraction.one_whole.1
+  · rintro ⟨q', HP⟩
+    let q'' : F := (IsSplitFraction.split q').1
+    exists (.own q'')
+    refine ⟨⟨q'', rfl⟩, ?_⟩
+    simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid]
+    rw [add_comm]
+    exists (IsSplitFraction.split q').2
+    rw [← add_assoc]
+    rw [IsSplitFraction.split_add]
+    exact HP
+
 end dfrac
diff --git a/src/Iris/Algebra/Frac.lean b/src/Iris/Algebra/Frac.lean
index 59be0f53..3f94d905 100644
--- a/src/Iris/Algebra/Frac.lean
+++ b/src/Iris/Algebra/Frac.lean
@@ -27,6 +27,10 @@ class Fraction (α : Type _) extends Add α where
   add_ne : ∀ {a b : α}, a ≠ b + a
   proper_add_mono_left : ∀ {a b : α}, Proper (a + b) → Proper a
 
+class IsSplitFraction (α : Type _) [Fraction α] where
+  split : α → α × α
+  split_add {a : α} : (split a).1 + (split a).2 = a
+
 namespace Fraction
 
 /-- A fraction does not represent the entire resource.
diff --git a/src/Iris/Algebra/Heap.lean b/src/Iris/Algebra/Heap.lean
new file mode 100644
index 00000000..1db3bfa6
--- /dev/null
+++ b/src/Iris/Algebra/Heap.lean
@@ -0,0 +1,596 @@
+/-
+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.Algebra.CMRA
+import Iris.Algebra.OFE
+
+open Iris
+
+/-! ## Generic heaps
+
+Note: There are three definitions of equivalence in this file
+
+[1] OFE.Equiv (pointwise equvalence)
+[2] StoreO.Equiv (pointwise equality of .get)
+[3] Eq (equality of representations)
+
+[3] -> [2] -> [1] always
+[1] -> [2] when the value type is Leibniz
+[2] -> [3] when the store is an IsoFunStore
+-/
+
+-- TODO: Move this to a generic set theory library
+def set_disjoint {X : Type _} (S1 S2 : X → Prop) : Prop := ∀ x : X, ¬(S1 x ∧ S2 x)
+def set_union {X : Type _} (S1 S2 : X → Prop) : X → Prop := fun x => S1 x ∨ S2 x
+def set_included {X : Type _} (S1 S2 : X → Prop) : Prop := ∀ x, S1 x → S2 x
+
+/-- The type `T` can store and retrieve keys of type `K` and obtain values of type `V`. -/
+class Store (T : Type _) (K V : outParam (Type _)) where
+  get : T → K → V
+  set : T → K → V → T
+  get_set_eq {t k k' v} : k = k' → get (set t k v) k' = v
+  get_set_ne {t k k' v} : k ≠ k' → get (set t k v) k' = get t k'
+export Store (get set get_set_eq get_set_ne)
+
+open Classical in
+theorem Store.get_set [Store T K V] {t : T} {k k' : K} {v : V} :
+    get (set t k v) k' = if k = k' then v else get t k' := by
+  split <;> rename_i h
+  · exact get_set_eq h
+  · exact get_set_ne h
+
+/-- An index-dependent predicate holds at every member of the store. -/
+def Store.all [Store T K V] (P : K → V → Prop) : T → Prop :=
+  fun t => ∀ k, P k (get t k)
+
+/-- Two Stores are pointwise equivalent. -/
+@[simp] def Store.Equiv [Store T K V] (t1 t2 : T) : Prop := get t1 = get t2
+
+instance Store.Equiv_trans [Store T K V] : Trans Equiv (Equiv (T := T)) Equiv := ⟨by simp_all⟩
+
+/-- RepFunStore: The type T can represent all functions that satisfy Rep.
+For instance, this holds with `rep _ = True` when `T = K → V`. On the other hand, when
+`T = list (K × Option V)` representing a partial function with an association list, this holds
+when `rep f` is the predicate that says `f` has finite domain. -/
+class RepFunStore (T : Type _) (K V : outParam (Type _)) [Store T K V] where
+  rep : (K → V) → Prop
+  rep_get (t : T) : rep (get t)
+  ofFun : { f : K → V // rep f } → T
+  get_ofFun: get (ofFun f) = f
+export RepFunStore (rep rep_get ofFun get_ofFun)
+
+/-- IsoFunStore: The type T is isomorphic the type of functions `{f : Rep f}`, or in other words,
+equality of T is the same as equality of `{f : Rep f}`. -/
+class IsoFunStore (T : Type _) (K V : outParam (Type _)) [Store T K V] extends RepFunStore T K V where
+  ofFun_get {t : T} : ofFun ⟨get t, rep_get t⟩ = t
+export IsoFunStore (ofFun_get)
+
+theorem IsStoreIso.ext [Store T K V] [IsoFunStore T K V] {t1 t2 : T}
+    (H : ∀ k, get t1 k = get t2 k) : t1 = t2 := by
+  rw [← ofFun_get (t := t1), ← ofFun_get (t := t2)]
+  congr 2; exact funext H
+
+/-- [2] → [3] -/
+theorem IsoFunStore.store_eq_of_Equiv [Store T K V] [IsoFunStore T K V] {t1 t2 : T} :
+    Store.Equiv t1 t2 → t1 = t2 := (IsStoreIso.ext <| fun k => congrFun · k)
+
+/-- Stores of type T1 can be coerced to stores of type T2. -/
+class HasStoreMap (T1 T2 : Type _) (K V1 V2 : outParam (Type _)) [Store T1 K V1] [Store T2 K V2] where
+  /-- Map a function that depends on the elemet across the entire structure  -/
+  dmap (f : K → V1 → V2) : T1 → T2
+  get_dmap : get (dmap f t) k = f k (get t k)
+export HasStoreMap (dmap get_dmap)
+
+/-- Map between heaps that preserves non-allocations. -/
+class HasHHMap (T1 T2 : Type _) (K V1 V2 : outParam (Type _))
+   [Store T1 K (Option V1)] [Store T2 K (Option V2)] where
+  hhmap (f : K → V1 → Option V2) : T1 → T2
+  hhmap_get (f : K → V1 → Option V2) : get (hhmap f t) k = (get t k).bind (f k)
+export HasHHMap (hhmap hhmap_get)
+
+def HasStoreMap.map (f : V1 → V2) [Store T1 K V1] [Store T2 K V2] [HasStoreMap T1 T2 K V1 V2] : T1 → T2 :=
+  HasStoreMap.dmap (fun (_ : K) => f)
+
+class Heap (T : Type _) (K V : outParam (Type _)) extends Store T K (Option V) where
+  empty : T
+  hmap (f : K → V → Option V) : T → T
+  merge (op : V → V → V) : T → T → T
+  get_empty : get empty k = none
+  get_hmap : get (hmap f t) k = (get t k).bind (f k)
+  get_merge : get (merge op t1 t2) k = Option.merge op (get t1 k) (get t2 k)
+export Heap (empty hmap merge get_empty get_hmap get_merge)
+
+theorem hmap_alloc [Heap T K V] {t : T} (H : get t k = some v) : get (hmap f t) k = f k v := by
+  simp [get_hmap, bind, H]
+
+theorem hmap_unalloc [Heap T K V] {t : T} (H : get t k = none) : get (hmap f t) k = none := by
+  simp [get_hmap, bind, H]
+
+/-- The heap of a single point -/
+def Heap.point [Heap T K V] (k : K) (v : Option V) : T := set empty k v
+
+/-- Delete an element from a heap by setting its value to .none -/
+def Heap.delete [Heap T K V] (t : T) (k : K) : T := set t k none
+
+/-- The domain of a heap is the set of keys that map to .some values. -/
+def Heap.dom [Heap T K V] (t : T) : K → Prop := fun k => (get t k).isSome
+
+@[simp] def Heap.union [Heap T K V] : T → T → T := merge (fun v _ => v)
+
+theorem Heap.point_get_eq [Heap T K V] (H : k = k') : get (point k v : T) k' = v := by
+  rw [point, get_set_eq H]
+
+theorem Heap.point_get_ne [Heap T K V] (H : k ≠ k') : get (point k v : T) k' = none := by
+  rw [point, get_set_ne H, get_empty]
+
+open Classical in
+theorem Heap.get_point [Heap T K V] {k k' : K} {v : Option V} :
+    get (point k v : T) k' = if k = k' then v else .none := by
+  split <;> rename_i h
+  · exact point_get_eq h
+  · exact point_get_ne h
+
+/-- An AllocHeap is a heap which can allocate elements under some condition. -/
+class AllocHeap (T : Type _) (K V : outParam (Type _)) extends Heap T K V where
+  notFull : T → Prop
+  fresh {t : T} : notFull t → K
+  get_fresh  {H : notFull t} : get t (fresh H) = none
+export AllocHeap (notFull fresh get_fresh)
+
+/-- An UnboundeHeap is a heap which can allocate an unbounded number of elements starting at empty. -/
+class UnboundedHeap (T : Type _) (K V : outParam (Type _)) extends AllocHeap T K V where
+  notFull_empty : notFull (empty : T)
+  notFull_set_fresh {H : notFull t} : notFull (set t (fresh H) v)
+export UnboundedHeap (notFull_empty notFull_set_fresh)
+
+section ofe
+open OFE
+
+instance Store.instOFE [Store T K V] [OFE V] : OFE T where
+  Equiv s0 s1  := get s0 ≡ get s1
+  Dist n s0 s1 := get s0 ≡{n}≡ get s1
+  dist_eqv     := ⟨fun _ => .of_eq rfl, (·.symm), (·.trans ·)⟩
+  equiv_dist   := equiv_dist
+  dist_lt      := dist_lt
+
+@[simp] def Store.toMap [Store T K V] [OFE V] : T -n> (K → V) where
+  f x := get x
+  ne.1 {_ _ _} H k := H k
+
+@[simp] def Store.ofMap [Store T K V] [R : RepFunStore T K V] [OFE V] : {f : K → V // R.rep f} -n> T where
+  f x := ofFun x
+  ne.1 {_ _ _} H k := by rw [get_ofFun, get_ofFun]; exact H k
+
+instance get_ne [Store T K V] [OFE V] (k : K) : NonExpansive (get · k : T → V) where
+  ne {_ _ _} Ht := Ht k
+
+instance [Store T K V] [OFE V] (k : K) : NonExpansive₂ (set · k · : T → V → T) where
+  ne {_ _ _} Hv {_ _} Ht k' := by
+    if h : k = k'
+      then rw [get_set_eq h, get_set_eq h]; exact Ht
+      else rw [get_set_ne h, get_set_ne h]; exact Hv k'
+
+theorem Store.eqv_of_Equiv [OFE V] [Store T K V] {t1 t2 : T} (H : Equiv t1 t2) : t1 ≡ t2 :=
+  (.of_eq <| congrFun H ·)
+
+instance [Heap T K V] [OFE V] (op : V → V → V) [NonExpansive₂ op] :
+    NonExpansive₂ (merge (T := T) op) where
+  ne _ {_ _} Ht {_ _} Hs k := by
+    simp only [get_merge]
+    exact NonExpansive₂.ne (Ht k) (Hs k)
+
+instance [Store T1 K V1] [Store T2 K V2] [OFE V1] [OFE V2] (f : K → V1 → V2)
+  [∀ k, NonExpansive (f k)] [HasStoreMap T1 T2 K V1 V2] : NonExpansive (dmap f : T1 → T2) where
+  ne _ {_ _} H k := by simp only [get_dmap]; exact NonExpansive.ne (H k)
+
+/-- Project a chain of stores through it's kth coordinate to a chain of values. -/
+def Store.chain [Store T K V] [OFE V] (k : K) (c : Chain T) : Chain V where
+  chain i := get (c i) k
+  cauchy Hni := c.cauchy Hni k
+
+theorem Store.chain_get [Store T K V] [OFE V] (k : K) (c : Chain T) :
+    (chain k c) i = get (c i) k := by
+  simp [chain]
+
+open Store in
+instance Heap.instCOFE [Heap T K V] [COFE V] : COFE T where
+  compl c := hmap (fun _ => COFE.compl <| c.map ⟨_, get_ne ·⟩) (c 0)
+  conv_compl {_ c} k := by
+    rw [get_hmap]
+    rcases H : get (c.chain 0) k
+    · rw [← chain_get, chain_none_const (c := chain k c) (n := 0) (H▸rfl)]; rfl
+    · exact IsCOFE.conv_compl
+
+end ofe
+
+section cmra
+open CMRA
+
+/- ## A CMRA on Heaps -/
+
+variable [Heap T K V] [CMRA V]
+
+@[simp] def Store.op (s1 s2 : T) : T := merge (K := K) CMRA.op s1 s2
+@[simp] def Store.unit : T := empty
+@[simp] def Store.pcore (s : T) : Option T := some <| hmap (fun _ => CMRA.pcore) s
+@[simp] def Store.valid (s : T) : Prop := ∀ k, ✓ (get s k : Option V)
+@[simp] def Store.validN (n : Nat) (s : T) : Prop := ∀ k, ✓{n} (get s k : Option V)
+
+theorem lookup_incN {n} {m1 m2 : T} :
+    (∃ (z : T), m2 ≡{n}≡ Store.op m1 z) ↔
+    ∀ i, (∃ z, (get m2 i) ≡{n}≡ (get m1 i) • z) := by
+  refine ⟨fun ⟨z, Hz⟩ i => ?_, fun H => ?_⟩
+  · refine ⟨get z i, ?_⟩
+    refine .trans (get_ne i |>.ne Hz) ?_
+    simp only [Store.op, op, optionOp, get_merge]
+    cases get m1 i <;> cases get z i <;> simp
+  · obtain ⟨f, Hf⟩ := Classical.axiomOfChoice H
+    exists hmap (fun k _ => f k) m2
+    refine fun i => (Hf i).trans ?_
+    specialize Hf i; revert Hf
+    simp [CMRA.op, optionOp, get_merge, get_hmap]
+    cases get m2 i <;> cases get m1 i <;> cases f i <;> simp
+
+theorem lookup_inc {m1 m2 : T} :
+    (∃ (z : T), m2 ≡ Store.op m1 z) ↔
+    ∀ i, (∃ z, (Store.get m2 i) ≡ (Store.get m1 i) • z) := by
+  refine ⟨fun ⟨z, Hz⟩ i => ?_, fun H => ?_⟩
+  · refine ⟨get z i, ?_⟩
+    refine .trans (get_ne i |>.eqv Hz) ?_
+    simp only [Store.op, op, optionOp, get_merge]
+    cases get m1 i <;> cases get z i <;> simp
+  · obtain ⟨f, Hf⟩ := Classical.axiomOfChoice H
+    exists hmap (fun k _ => f k) m2
+    refine fun i => (Hf i).trans ?_
+    specialize Hf i; revert Hf
+    simp [CMRA.op, optionOp, get_merge, get_hmap]
+    cases get m2 i <;> cases get m1 i <;> cases f i <;> simp
+
+open OFE in
+instance instStoreCMRA : CMRA T where
+  pcore := Store.pcore
+  op := Store.op
+  ValidN := Store.validN
+  Valid := Store.valid
+  op_ne.ne _ x1 x2 H i := by
+    specialize H i; revert H; rename_i x _
+    simp [op, get_merge]
+    cases get x1 i <;> cases get x2 i <;> cases get x i <;> simp
+    apply op_right_dist
+  pcore_ne {n x y _} H := by
+    simp only [Store.pcore, Option.some.injEq, exists_eq_left']
+    refine (· ▸ fun k => ?_); specialize H k; revert H
+    rw [get_hmap, get_hmap]
+    cases Store.get x k <;> cases Store.get y k <;> simp
+    exact (NonExpansive.ne ·)
+  validN_ne Hx H k :=
+    validN_ne (NonExpansive.ne (f := (Store.get · k : T → Option V)) Hx) (H k)
+  valid_iff_validN :=
+    ⟨fun H n k => valid_iff_validN.mp (H k) n,
+     fun H k => valid_iff_validN.mpr (H · k)⟩
+  validN_succ H k := validN_succ (H k)
+  validN_op_left {n x1 x2} H k := by
+    refine validN_op_left (y := Store.get x2 k) ?_
+    specialize H k; revert H
+    simp only [Store.op, get_merge, Option.merge]
+    cases get x1 k <;> cases get x2 k <;> simp [optionOp, op]
+  assoc {x y z} k := by
+    simp only [Store.op, get_merge]
+    cases Store.get x k <;> cases Store.get y k <;> cases Store.get z k <;> simp
+    exact assoc
+  comm {x y} k := by
+    simp [Store.op, Heap.get_merge]
+    cases Store.get x k <;> cases Store.get y k <;> simp
+    exact comm
+  pcore_op_left {x cx} H k := by
+    simp only [← Option.getD_some (a := cx) (b := cx), Store.op, get_merge]
+    cases Hcx : Store.get cx k <;> cases hx : Store.get x k <;> simp <;>
+      simp only [Store.pcore, Option.some.injEq] at H
+    · rw [← H, hmap_unalloc hx] at Hcx
+      cases Hcx
+    · apply pcore_op_left
+      rw [← Hcx, ← H, hmap_alloc hx]
+  pcore_idem {x cx} H := by
+    simp only [Store.pcore, Option.some.injEq] at H
+    change (Store.pcore cx |>.getD cx) ≡ cx
+    intro k
+    simp [← H, get_hmap]
+    rcases Store.get x k with (_|v) <;> simp
+    cases HY : pcore v; simp
+    exact pcore_idem HY
+  pcore_op_mono := by
+    apply pcore_op_mono_of_core_op_mono
+    rintro x cx y ⟨z, Hz⟩
+    suffices ∃ z, (Store.pcore y |>.getD y) ≡ Store.op (Store.pcore x |>.getD x) z by
+      rintro Hx
+      simp only [Store.pcore, Option.some.injEq, Store.op, exists_eq_left']
+      rcases this with ⟨z', Hz'⟩
+      exists z'
+      refine .trans Hz' (fun i => ?_)
+      cases get z' i <;> cases get x i <;> simp_all
+    refine lookup_inc.mpr (fun i => ?_)
+    obtain ⟨v', Hv'⟩ : (core (Store.get x i)) ≼ (core (Store.get y i))  := by
+      apply core_mono
+      exists get z i
+      have Hz := Hz i; revert Hz
+      simp [CMRA.op, optionOp, get_merge]
+      cases get x i <;> cases get z i <;> simp_all
+    exists v'
+    simp_all [core, pcore, optionCore, get_hmap]
+  extend {n x y1 y2} Hm Heq := by
+    have Hslice i : Store.get x i ≡{n}≡ Store.get y1 i • Store.get y2 i := by
+      refine (get_ne i |>.ne Heq).trans ?_
+      simp [CMRA.op, get_merge, optionOp]
+      cases get y1 i <;> cases get y2 i <;> simp
+    let extendF (i : K) := CMRA.extend (Hm i) (Hslice i)
+    exists hmap (fun k (_ : V) => extendF k |>.fst) y1
+    exists hmap (fun k (_ : V) => extendF k |>.snd.fst) y2
+    simp [Store.op, get_merge]
+    refine ⟨fun i => ?_, fun i => ?_, fun i => ?_⟩
+    all_goals rcases hF : extendF i with ⟨z1, z2, Hm, Hz1, Hz2⟩
+    · refine Hm.trans ?_
+      simp [Store.op, get_merge, hF, CMRA.op, optionOp]
+      cases z1 <;> cases z2 <;> cases h1 : get y1 i <;> cases h2 : get y2 i <;> simp [h1, h2] at Hz1 Hz2
+      · rw [hmap_unalloc h1, hmap_unalloc h2]; simp
+      · rw [hmap_unalloc h1, hmap_alloc h2, hF]; simp
+      · rw [hmap_alloc h1, hmap_unalloc h2, hF]; simp
+      · rw [hmap_alloc h1, hmap_alloc h2, hF]; simp
+    · cases h : Store.get y1 i
+      · rw [hmap_unalloc h]
+      · rw [hmap_alloc h, ← h, hF]; exact Hz1
+    · cases h : Store.get y2 i
+      · rw [hmap_unalloc h]
+      · rw [hmap_alloc h, ← h, hF]; exact Hz2
+
+instance instStoreUCMRA : UCMRA T where
+  unit := Store.unit
+  unit_valid := by
+    simp [CMRA.Valid, Store.valid, optionValid, Store.unit, get_empty]
+  unit_left_id _ := by
+    simp [CMRA.op, Heap.get_merge, Store.unit, get_empty]
+  pcore_unit _ := by
+    simp [Store.unit, hmap_unalloc get_empty, get_empty]
+
+end cmra
+
+namespace Heap
+
+variable {K V : Type _} [Heap T K V] [CMRA V]
+open CMRA Store
+
+theorem validN_get_validN {m : T} (Hv : ✓{n} m) (He : get m i ≡{n}≡ some x) : ✓{n} x := by
+  specialize Hv i; revert Hv
+  rcases h : get m i <;> simp [h] at He
+  exact OFE.Dist.validN He |>.mp
+
+theorem valid_get_valid {m : T} (Hv : ✓ m) (He : get m i ≡ some x) : ✓ x :=
+  valid_iff_validN.mpr (fun _ => validN_get_validN Hv.validN He.dist)
+
+theorem insert_validN {m : T} (Hx : ✓{n} x) (Hm : ✓{n} m) : ✓{n} (set m i x) := by
+  intro k
+  rw [get_set]; split; rename_i He
+  · exact Hx
+  · apply Hm
+
+theorem insert_valid {m : T} (Hx : ✓ x) (Hm : ✓ m) : ✓ (set m i x) :=
+  valid_iff_validN.mpr (fun _ => insert_validN Hx.validN Hm.validN)
+
+theorem point_valid_iff : ✓ (point i x : T) ↔ ✓ x := by
+  refine ⟨fun H => ?_, fun H k => ?_⟩
+  · specialize H i; rw [point_get_eq rfl] at H; trivial
+  · rw [get_point]; split <;> trivial
+
+theorem point_validN_iff : ✓{n} (point i x : T) ↔ ✓{n} x := by
+  refine ⟨fun H => ?_, fun H k => ?_⟩
+  · specialize H i; rw [point_get_eq rfl] at H; trivial
+  · rw [get_point]; split <;> trivial
+
+theorem delete_validN {m : T} (Hv : ✓{n} m) : ✓{n} (delete m i) := by
+  intro k
+  rw [delete, get_set]; split
+  · trivial
+  · exact Hv k
+
+theorem delete_valid {m : T} (Hv : ✓ m) : ✓ (delete m i) :=
+  valid_iff_validN.mpr (fun _ => delete_validN Hv.validN)
+
+theorem set_equiv_point_op_point {m : T} (Hemp : get m i = none) : Equiv (set m i x) (point i x • m) := by
+  refine funext (fun k => ?_)
+  simp [CMRA.op, Store.op, Equiv, get_merge, Option.merge, get_point, Hemp, get_set]
+  split <;> rename_i He
+  · rw [← He, Hemp]; cases x <;> rfl
+  · cases (Store.get m k) <;> rfl
+
+theorem set_eq_point_op_point [IsoFunStore T K (Option V)] {m : T} (Hemp : get m i = none) :
+    set m i x = point i x • m :=
+  IsoFunStore.store_eq_of_Equiv (set_equiv_point_op_point Hemp)
+
+theorem core_point_equiv {i : K} {x : V} {cx} (Hpcore : pcore x = some cx) :
+    Equiv (T := T) (core <| point i (some x)) (point i (some cx)) := by
+  refine funext fun k => ?_
+  simp [← Hpcore, core, CMRA.pcore, get_point, get_hmap]
+  split <;> rfl
+
+theorem point_core_eq [IsoFunStore T K (Option V)] {i : K} {x : V} {cx} (Hpcore : pcore x = some cx) :
+    core (point (T := T) i (some x)) = point i (some cx)  :=
+  IsoFunStore.store_eq_of_Equiv (core_point_equiv Hpcore)
+
+theorem point_core_eqv {i : K} {x : V} {cx} (Hpcore : pcore x ≡ some cx) :
+    core (point (T := T) i (some x)) ≡ point i (some cx) := by
+  intro k
+  simp [core, CMRA.pcore, get_point, get_hmap]
+  split <;> trivial
+
+theorem point_core_total [IsTotal V] {i : K} {x : V} :
+    Equiv (core <| point (T := T) i (some x)) ((point i (some (core x)))) := by
+  obtain ⟨_, Hxc⟩ := total x
+  apply (core_point_equiv Hxc).trans
+  simp [core, Hxc]
+
+theorem point_core_total_eq [IsTotal V] [IsoFunStore T K (Option V)] {i : K} {x : V} :
+    core (point (T := T) i (some x)) = point i (some (core x)) :=
+  IsoFunStore.store_eq_of_Equiv point_core_total
+
+theorem point_op_point {i : K} {x y : V} :
+    Equiv ((point (T := T) i (some x)) • (point i (some y))) ((point i (some (x • y)))) := by
+  refine funext fun k => ?_
+  simp only [CMRA.op, Store.op, get_merge, get_point]
+  split <;> simp [Option.merge]
+
+theorem point_op_point_eq [IsoFunStore T K (Option V)] {i : K} {x y : V} :
+    (point (T := T) i (some x)) • (point i (some y)) = (point i (some (x • y))) :=
+  IsoFunStore.store_eq_of_Equiv point_op_point
+
+instance {m : T} [∀ x : V, CoreId x] : CoreId m where
+  core_id i := by
+    rw [get_hmap]
+    cases Store.get m i <;> simp
+    exact core_id
+
+instance [CoreId (x : V)] : CoreId (point (T := T) i (some x)) where
+  core_id k := by
+    simp [get_hmap, get_point]
+    split <;> simp
+    exact  core_id
+
+theorem point_incN_iff {m : T} :
+    (point (T := T) i (some x)) ≼{n} m ↔ ∃ y, (get m i ≡{n}≡ some y) ∧ some x ≼{n} some y := by
+  refine ⟨fun ⟨z, Hz⟩ => ?_, fun ⟨y, Hy, z, Hz⟩ => ?_⟩
+  · specialize Hz i; revert Hz
+    simp only [CMRA.op, Store.op, get_merge, point_get_eq rfl]
+    rcases get z i with (_|v)
+    · intro _
+      exists x
+    · refine (⟨x • v, ·, ?_⟩)
+      exists v
+  · exists set m i z
+    intro j
+    simp [CMRA.op, get_merge, get_point, get_set]
+    split <;> rename_i He
+    · refine (He ▸ Hy).trans (Hz.trans ?_)
+      cases z <;> simp [CMRA.op, optionOp]
+    · simp
+
+theorem point_inc_iff {m : T} :
+    (point i (T := T) (some x)) ≼ m ↔ ∃ y, (get m i ≡ some y) ∧ some x ≼ some y := by
+  refine ⟨fun ⟨z, Hz⟩ => ?_, fun ⟨y, Hy, z, Hz⟩ => ?_⟩
+  · specialize Hz i; revert Hz
+    simp only [CMRA.op, Store.op, get_merge, point_get_eq rfl]
+    rcases get z i with (_|v)
+    · intro _
+      exists x
+    · refine (⟨x • v, ·, ?_⟩)
+      exists v
+  · exists set m i z
+    intro j
+    simp [CMRA.op, get_merge, get_point, get_set]
+    split <;> rename_i He
+    · refine (He ▸ Hy).trans (Hz.trans ?_)
+      cases z <;> simp [CMRA.op, optionOp]
+    · simp
+
+theorem exclusive_point_inc_iff {m : T} (He : Exclusive x) (Hv : ✓ m) :
+    (point i (T := T) (some x)) ≼ m ↔ (get m i ≡ some x) := by
+  refine point_inc_iff.trans ⟨fun ⟨y, Hy, Hxy⟩ => ?_, fun _ => ?_⟩
+  · suffices x ≡ y by exact Hy.trans <| this.symm
+    exact Option.eqv_of_inc_exclusive Hxy <| valid_get_valid Hv Hy
+  · exists x
+
+theorem point_inc_point_iff : (point i (T := T) (some x)) ≼ (point i (some y)) ↔ some x ≼ some y := by
+  refine point_inc_iff.trans ⟨fun ⟨z, Hz, Hxz⟩ => ?_, fun H => ?_⟩
+  · refine inc_of_inc_of_eqv Hxz ?_
+    refine .trans Hz.symm ?_
+    exact .of_eq <| point_get_eq rfl
+  · refine ⟨y, ?_, H⟩
+    exact .of_eq <| point_get_eq rfl
+
+theorem total_point_inc_point_iff [IsTotal V] : (point i (T := T) (some x)) ≼ (point i (some y)) ↔ x ≼ y :=
+  point_inc_point_iff.trans <| Option.some_inc_some_iff_isTotal
+
+theorem point_inc_point_mono (Hinc : x ≼ y) : (point (T := T) i (some x)) ≼ (point i (some y)) :=
+  point_inc_point_iff.mpr <| Option.some_inc_some_iff.mpr <| .inr Hinc
+
+instance [H : Cancelable (some x)] : Cancelable (point (T := T) i (some x)) where
+  cancelableN {n m1 m2} Hv He j := by
+    specialize Hv j; revert Hv
+    specialize He j; revert He
+    simp only [CMRA.op, Store.op, get_merge, Option.merge, get_point]
+    if He : i = j
+      then
+        simp_all only [↓reduceIte]
+        intro Hv He
+        cases _ : get m1 j <;> cases _ : get m2 j
+        all_goals apply H.cancelableN
+        all_goals simp_all [CMRA.op, Store.op, optionOp]
+      else
+        cases get m1 j <;> cases get m2 j
+        all_goals simp_all [CMRA.op, optionOp]
+
+instance {m : T} [Hid : ∀ x : V, IdFree x] [Hc : ∀ x : V, Cancelable x] : Cancelable m where
+  cancelableN {n m1 m2} Hv He i := by
+    apply cancelableN (x := get m i)
+    · specialize Hv i; revert Hv
+      simp [CMRA.op, Store.op, Heap.get_merge, optionOp]
+      cases _ : get m i <;> cases _ : get m1 i <;> simp_all
+    · specialize He i; revert He
+      simp [Heap.get_merge, CMRA.op, Store.op, optionOp]
+      cases get m i <;> cases get m1 i <;> cases get m2 i <;> simp_all [Heap.get_merge]
+
+theorem insert_op_equiv {m1 m2 : T} :
+    Equiv ((set (V := Option V) (m1 • m2) i (x • y))) (set m1 i x • set m2 i y) := by
+  refine funext fun j => ?_
+  if He : i = j
+    then
+      simp [CMRA.op, get_set_eq He, get_merge, optionOp]
+      cases x <;> cases y <;> simp_all
+    else
+      simp [CMRA.op, get_set_ne (T := T) He, get_merge]
+
+theorem insert_op_eq [IsoFunStore T K (Option V)] {m1 m2 : T} :
+    (set (V := Option V) (m1 • m2) i (x • y)) = (set m1 i x • set m2 i y) :=
+  IsoFunStore.store_eq_of_Equiv insert_op_equiv
+
+theorem disjoint_op_equiv_union {m1 m2 : T} (Hd : set_disjoint (dom m1) (dom m2)) :
+    Equiv (m1 • m2) (union m1 m2) := by
+  refine funext fun j => ?_
+  simp [CMRA.op, Store.op, Heap.get_merge]
+  rcases _ : get m1 j <;> cases _ : get m2 j <;> simp_all
+  refine (Hd j ?_).elim
+  simp_all [dom]
+
+theorem disjoint_op_eq_union [IsoFunStore T K (Option V)] {m1 m2 : T} (H : set_disjoint (dom m1) (dom m2)) :
+    m1 • m2 = Heap.union m1 m2 :=
+  IsoFunStore.store_eq_of_Equiv (disjoint_op_equiv_union H)
+
+theorem valid0_disjoint_dom {m1 m2 : T} (Hv : ✓{0} (m1 • m2)) (H : ∀ {k x}, get m1 k = some x → Exclusive x) :
+    set_disjoint (dom m1) (dom m2) := by
+  rintro k
+  simp only [dom, Option.isSome]
+  rcases HX : get m1 k with (_|x) <;> simp
+  rcases HY : get m2 k with (_|y) <;> simp
+  apply (H HX).1 y
+  simp [CMRA.op, CMRA.ValidN] at Hv; specialize Hv k; revert Hv
+  simp [Heap.get_merge, optionValidN, HX, HY]
+
+theorem valid_disjoint_dom {m1 m2 : T} (Hv : ✓ (m1 • m2)) (H : ∀ {k x}, get m1 k = some x → Exclusive x) :
+    set_disjoint (dom m1) (dom m2) :=
+  valid0_disjoint_dom (Valid.validN Hv) H
+
+theorem dom_op_union (m1 m2 : T) : dom (m1 • m2) = set_union (dom m1) (dom m2) := by
+  refine funext fun k => ?_
+  cases get m1 k <;> cases get m2 k <;> simp_all [CMRA.op, dom, set_union, get_merge]
+
+theorem inc_dom_inc {m1 m2 : T} (Hinc : m1 ≼ m2) : set_included (dom m1) (dom m2) := by
+  intro i; unfold Heap.dom
+  rcases lookup_inc.mp Hinc i with ⟨z, Hz⟩; revert Hz
+  cases get m1 i <;> cases get m2 i <;> cases z <;>
+    simp [CMRA.op, optionOp]
+
+nonrec instance [HD : CMRA.Discrete V] [Heap T K V] : Discrete T where
+  discrete_0 {_ _} H := (OFE.Discrete.discrete_0 <| H ·)
+  discrete_valid {_} := (CMRA.Discrete.discrete_valid <| · ·)
+
+end Heap
diff --git a/src/Iris/Algebra/Lib.lean b/src/Iris/Algebra/Lib.lean
new file mode 100644
index 00000000..d4c9402a
--- /dev/null
+++ b/src/Iris/Algebra/Lib.lean
@@ -0,0 +1,2 @@
+import Iris.Algebra.Lib.ClassicalHeaps
+import Iris.Algebra.Lib.FiniteHeaps
diff --git a/src/Iris/Algebra/Lib/ClassicalHeaps.lean b/src/Iris/Algebra/Lib/ClassicalHeaps.lean
new file mode 100644
index 00000000..048171c5
--- /dev/null
+++ b/src/Iris/Algebra/Lib/ClassicalHeaps.lean
@@ -0,0 +1,137 @@
+/-
+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.Algebra.Heap
+
+-- Library functions: move me
+
+/-- A set S is infinite if there exists an injection from Nat into the set of elements
+  such that S holds. -/
+def infinite (S : P → Prop) : Prop :=
+  ∃ f : Nat → P, (∀ n, S <| f n) ∧ (∀ n m : Nat, f n = f m → n = m)
+
+class InfiniteType (T : Type _) where
+  enum : Nat → T
+  enum_inj : ∀ n m : Nat, enum n = enum m → n = m
+
+
+/-- Arbitrarily changing one element of a co-infinite set yields a co-infinite set -/
+theorem cofinite_alter_cofinite {S S' : P → Prop} (p' : P) (Ha : ∀ p, p ≠ p' → S p = S' p)
+    (Hs : infinite S) : infinite S' := by
+  rcases Hs with ⟨f, HfS, Hfinj⟩
+  -- Basically, alter f so that f never hits p'.
+  rcases (Classical.em (∃ n, f n = p')) with (⟨n, H⟩|H)
+  · exists fun n' => if n' < n then f n' else f n'.succ
+    constructor
+    · intro n'
+      simp only []
+      split
+      · rw [← Ha]
+        · apply HfS
+        · rename_i Hk'
+          intro Hk
+          exact Nat.lt_irrefl (n := n) <| (Hfinj _ _ (Hk ▸ H)) ▸ Hk'
+      · rw [← Ha]
+        · apply HfS
+        · rename_i Hk'
+          intro Hk
+          have _ := (Hfinj _ _ (Hk ▸ H)) ▸ Hk'
+          simp_all
+    · intro n' m'
+      simp only []
+      split <;> split
+      · apply Hfinj
+      · intro H
+        have Hfinj' := Hfinj _ _ H
+        exfalso
+        subst Hfinj'
+        rename_i HK HK'
+        apply HK
+        exact Nat.lt_of_succ_lt HK'
+      · intro H
+        have Hfinj' := Hfinj _ _ H
+        exfalso
+        subst Hfinj'
+        rename_i HK HK'
+        apply HK
+        exact Nat.lt_of_succ_lt HK'
+      · intro H
+        exact Nat.succ_inj.mp (Hfinj n'.succ m'.succ H)
+  · exists f
+    refine ⟨?_, Hfinj⟩
+    exact fun n => (Ha _ (H ⟨n, ·⟩)) ▸ HfS n
+
+open Classical in
+/- Update a (classical) function at a point. Used to specify the correctness of stores. -/
+noncomputable def fset {K V : Type _} (f : K → V) (k : K) (v : V) : K → V :=
+  fun k' => if (k = k') then v else f k'
+
+@[simp] def cosupport (f : K → Option V) : K → Prop := ((· == false) ∘ Option.isSome ∘ f)
+
+theorem coinfinite_fset_coinfinite (f : K → Option V) (H : infinite (cosupport f)) :
+    infinite (cosupport (fset f k v)) := by
+  apply cofinite_alter_cofinite  k _ H
+  intro p Hpk
+  simp [cosupport, fset]
+  split
+  · simp_all
+  · rfl
+
+section instances
+
+noncomputable instance instClassicalStore {K V : Type _} : Store (K → V) K V where
+  get := id
+  set := fset
+  get_set_eq H := by rw [H]; simp [fset]
+  get_set_ne H := by simp_all [fset]
+
+noncomputable instance instClassicalHeap : Heap (K → Option V) K V where
+  hmap h f k := match f k with | none => none | some x => h k x
+  get_hmap := by
+    intro f t k
+    simp [Store.get, Option.bind]
+    cases h1 : t k <;> simp_all
+  empty _ := none
+  get_empty := by simp [Store.get]
+  merge op f1 f2 k :=
+    match f1 k, f2 k with
+    | some v1, some v2 => some <| op v1 v2
+    | some v1, none => some v1
+    | none, some v2 => some v2
+    | none, none => none
+  get_merge := by
+    simp [Store.get]
+    intros
+    split <;> simp_all [Option.merge]
+
+theorem coinfinte_exists_next {f : K → Option V} :
+    infinite (cosupport f) → ∃ k, f k = none := by
+  rintro ⟨enum, Henum, Henum_inj⟩
+  exists (enum 0)
+  simp [cosupport] at Henum
+  apply Henum
+
+noncomputable instance instClassicaAllocHeap : AllocHeap (K → Option V) K V where
+  toHeap := instClassicalHeap
+  notFull f := infinite <| cosupport f
+  fresh HC := Classical.choose (coinfinte_exists_next HC)
+  get_fresh {_ HC} := Classical.choose_spec (coinfinte_exists_next HC)
+
+noncomputable instance [InfiniteType K] : UnboundedHeap ( K → Option V) K V where
+  notFull_empty := by
+    simp [notFull, empty, Function.comp, infinite]
+    exists InfiniteType.enum
+    exact fun n m a => InfiniteType.enum_inj n m a
+  notFull_set_fresh {t v H} := by
+    simp only [notFull] at ⊢ H
+    apply cofinite_alter_cofinite (Hs := H) (p' := @fresh (K → Option V) K _ _ _ H)
+    intro p
+    intro Hp
+    simp [cosupport]
+    simp [Store.set, fset]
+    split <;> simp_all
+
+end instances
diff --git a/src/Iris/Algebra/Lib/FiniteHeaps.lean b/src/Iris/Algebra/Lib/FiniteHeaps.lean
new file mode 100644
index 00000000..be42de8a
--- /dev/null
+++ b/src/Iris/Algebra/Lib/FiniteHeaps.lean
@@ -0,0 +1,179 @@
+/-
+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.Algebra.Heap
+import Iris.Algebra.Lib.ClassicalHeaps
+
+/-- Heaps with intrinsically finite domain, represented as an association list.
+Keys taken to be Nat for the sake of example. -/
+
+inductive FiniteDomFunction (V : Type _)
+| empty : FiniteDomFunction V
+| set : Nat → V → FiniteDomFunction V → FiniteDomFunction V
+| remove : Nat → FiniteDomFunction V → FiniteDomFunction V
+
+open FiniteDomFunction
+
+@[simp] def FiniteDomFunction.lookup (f : FiniteDomFunction V) (k : Nat) : Option V :=
+  match f with
+  | .empty => none
+  | .set n v' rest => if n = k then some v' else rest.lookup k
+  | .remove n rest => if n = k then none else rest.lookup k
+
+@[simp] def FiniteDomFunction.update (f : FiniteDomFunction V) (k : Nat) (v : Option V) : FiniteDomFunction V :=
+  match v with
+  | some v' => f.set k v'
+  | none => f.remove k
+
+@[simp] def FiniteDomFunction.map (F : Nat → V → Option V') (f : FiniteDomFunction V)  : FiniteDomFunction V' :=
+  match f with
+  | .empty => .empty
+  | .set n v rest =>
+      match (F n v) with
+      | .some r => .set n r (rest.map F)
+      | .none => .remove n (rest.map F)
+  | .remove n rest => .remove n (rest.map F)
+
+@[simp] def FiniteDomFunction.fresh (f : FiniteDomFunction V) : Nat :=
+  match f with
+  | .empty => 0
+  | .set n _ rest => max (n + 1) rest.fresh
+  | .remove n rest => max (n + 1) rest.fresh
+
+@[simp] def FiniteDomFunction.construct (f : Nat → Option V) (N : Nat) : FiniteDomFunction V :=
+  match N with
+  | .zero => .empty
+  | .succ N' =>
+      match (f N') with
+      | some v => .set N' v (FiniteDomFunction.construct f N')
+      | none => (FiniteDomFunction.construct f N')
+
+@[simp] def FiniteDomFunction.construct_spec (f : Nat → Option V) (N : Nat) : Nat → (Option V) :=
+  fun n => if n < N then f n else none
+
+theorem FiniteDomFunction.lookup_update (f : FiniteDomFunction V):
+    (f.update k v).lookup = fset (f.lookup) k v := by
+  refine funext (fun k' => ?_)
+  cases f <;> cases v <;> simp [fset]
+
+theorem FiniteDomFunction.fresh_lookup_ge (f : FiniteDomFunction V) n :
+    f.fresh ≤ n → f.lookup n = none := by
+  induction f
+  · simp
+  · rename_i n' v' rest IH
+    intro H
+    simp at H
+    simp
+    split <;> rename_i h
+    · omega
+    · apply IH
+      omega
+  · rename_i n' rest IH
+    intro H
+    simp at H
+    simp
+    intro H'
+    apply IH
+    omega
+
+theorem FiniteDomFunction.construct_get (f : Nat → Option V) (N : Nat) :
+    lookup (construct f N) = construct_spec f N := by
+  refine funext (fun k => ?_)
+  rcases Nat.lt_or_ge k N with (HL|HG)
+  · induction N <;> simp
+    rename_i N' IH
+    split <;> rename_i h
+    · simp [h]
+      split
+      · simp_all
+      · rw [IH (by omega)]
+        simp
+        omega
+    · rw [if_pos HL]
+      if h : k < N'
+        then
+          simp [IH h]
+          intro H1
+          omega
+        else
+          have Hx : k = N' := by omega
+          simp_all
+          clear Hx
+          clear h
+          suffices (∀ N'', N' ≤ N'' → (construct f N').lookup N'' = none) by apply this _ N'.le_refl
+          induction N'
+          · simp
+          · rename_i n' IH
+            intro N'' H
+            simp
+            cases h : f n' <;> simp
+            · apply IH
+              omega
+            · split
+              · simp
+                exfalso
+                omega
+              · apply IH
+                omega
+  · simp
+    rw [if_neg (by omega)]
+    induction N <;> simp
+    rename_i N' IH
+    split
+    · simp only [lookup]
+      split; omega
+      apply IH
+      omega
+    · apply IH
+      omega
+instance FiniteDomFunction.instFiniteDomStore : Store (FiniteDomFunction V) Nat (Option V) where
+  get := lookup
+  set := update
+  get_set_eq He := by simp only [lookup_update, fset, if_pos He]
+  get_set_ne He := by simp only [lookup_update, fset, if_neg He]
+
+abbrev op_lift (op : V → V → V) (v1 v2 : Option V) : Option V :=
+  match v1, v2 with
+  | some v1, some v2 => some (op v1 v2)
+  | some v1, none => some v1
+  | none, some v2 => some v2
+  | none, none => none
+
+instance FiniteDomFunction.instFiniteDomHeap : Heap (FiniteDomFunction V) Nat V where
+  hmap h f := f.map h
+  get_hmap := by
+    intros f t k
+    induction t
+    · simp_all [empty, Store.get, map]
+    · rename_i n' v' t' IH
+      simp_all [Store.get]
+      cases h1 : f n' v' <;> simp <;> split <;> rename_i h2 <;> simp_all
+    · rename_i n' t' IH
+      simp_all [Store.get]
+      split <;> simp [Option.bind]
+  empty := .empty
+  get_empty := by intros; simp [Store.get]
+  merge op t1 t2 := construct (fun n => op_lift op (t1.lookup n) (t2.lookup n)) (max t1.fresh t2.fresh)
+  get_merge := by
+    intro op t1 t2 k
+    simp only [Store.get]
+    simp [FiniteDomFunction.construct_get]
+    simp [Option.merge, op_lift]
+    split <;> rename_i h
+    · cases t1.lookup k <;> cases t2.lookup k <;> simp_all
+    · have Ht1 : t1.fresh ≤ k := by omega
+      have Ht2 : t2.fresh ≤ k := by omega
+      rw [FiniteDomFunction.fresh_lookup_ge _ _ Ht1]
+      rw [FiniteDomFunction.fresh_lookup_ge _ _ Ht2]
+
+instance instFinitDomAllocHeap : AllocHeap (FiniteDomFunction V) Nat V where
+  notFull _ := True
+  fresh {f} _ := f.fresh
+  get_fresh {f _} := fresh_lookup_ge f f.fresh (f.fresh.le_refl)
+
+instance : UnboundedHeap (FiniteDomFunction V) Nat V where
+  notFull_empty := by simp [notFull]
+  notFull_set_fresh {t v H} := by simp [notFull]
diff --git a/src/Iris/Algebra/LocalUpdates.lean b/src/Iris/Algebra/LocalUpdates.lean
index bb09b7de..8f7c019a 100644
--- a/src/Iris/Algebra/LocalUpdates.lean
+++ b/src/Iris/Algebra/LocalUpdates.lean
@@ -116,7 +116,7 @@ theorem LocalUpdate.valid [CMRA.Discrete α] {x y x' y' : α}
 
 theorem LocalUpdate.total_valid0 [CMRA.IsTotal α] {x y x' y' : α}
     (h : ✓{0} x → ✓{0} y → y ≼{0} x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') :=
-  .valid0 fun vx0 vy0 mz => h vx0 vy0 (CMRA.incN_of_some_incN_some mz)
+  .valid0 fun vx0 vy0 mz => h vx0 vy0 (Option.some_incN_some_iff_isTotal.mp mz)
 
 theorem LocalUpdate.total_valid [CMRA.IsTotal α] [CMRA.Discrete α] {x y x' y' : α}
     (h : ✓ x → ✓ y → y ≼ x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') :=
diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index 1d6404f2..adc19eb6 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -284,6 +284,30 @@ instance [OFE α] [Leibniz α] : Leibniz (Option α) where
     | none, none, _ => rfl
     | some _, some _, h => congrArg some (Leibniz.eq_of_eqv h)
 
+instance [OFE α] [Discrete α] : Discrete (Option α) where
+  discrete_0 {x y} H :=
+    match x, y with
+    | none, none => H
+    | some _, some _ => some_eqv_some.mpr (discrete_0 H)
+
+instance OFE.Option.some.ne [OFE α] : OFE.NonExpansive (some : α → Option α) := ⟨fun _ _ _ => id⟩
+
+theorem Option.some_is_discrete [OFE α] {a : α} (Ha : DiscreteE a) : DiscreteE (some a) := by
+  constructor
+  intro y H; cases y
+  · exact H
+  · exact Ha.discrete H
+
+theorem Option.none_is_discrete [OFE α] : DiscreteE (none : Option α) := by
+  constructor
+  intro y; cases y <;> simp
+
+instance Option.merge_ne [OFE α] {op : α → α → α} [NonExpansive₂ op] :
+    NonExpansive₂ (Option.merge op) where
+  ne n x1 x2 Hx y1 y2 Hy := by
+    cases x1 <;> cases x2 <;> cases y1 <;> cases y2 <;> simp_all
+    exact NonExpansive₂.ne Hx Hy
+
 abbrev OFEFun {α : Type _} (β : α → Type _) := ∀ a, OFE (β a)
 
 instance [OFEFun (β : α → _)] : OFE ((x : α) → β x) where
@@ -349,6 +373,19 @@ theorem dist_snd {n} [OFE α] [OFE β] {x y : α × β} (h : x ≡{n}≡ y) : x.
 theorem dist_prod_ext {n} [OFE α] [OFE β] {x₁ x₂ : α} {y₁ y₂ : β}
     (ex : x₁ ≡{n}≡ x₂) (ey : y₁ ≡{n}≡ y₂) : (x₁, y₁) ≡{n}≡ (x₂, y₂) := ⟨ex, ey⟩
 
+theorem prod.is_discrete [OFE α] [OFE β] {a : α} {b : β} (Ha : DiscreteE a) (Hb : DiscreteE b) :
+    DiscreteE (a, b) := by
+  constructor
+  intro y H; refine ⟨Ha.discrete H.1, Hb.discrete H.2⟩
+
+instance [OFE α] [OFE β] [Discrete α] [Discrete β] : Discrete (α × β) where
+  discrete_0 H := by
+    constructor
+    · apply Discrete.discrete_0
+      apply H.1
+    · apply Discrete.discrete_0
+      apply H.2
+
 /-- An isomorphism between two OFEs is a pair of morphisms whose composition is equivalent to the
 identity morphism. -/
 @[ext] structure Iso (α β : Type _) [OFE α] [OFE β] where
@@ -458,6 +495,40 @@ theorem map_comp [OFE α] [OFE β] [OFE γ] {f : α -n> β} {g : β -n> γ} {c :
 
 end Chain
 
+/-- If a chain of Option is ever none, is the constant none chain. -/
+theorem chain_none_const [OFE V] {c : Chain (Option V)} (H : c n = none) :
+    c = Chain.const none := by
+  rcases c with ⟨c, Hc⟩
+  congr 1; refine funext (fun k => ?_)
+  rcases Nat.le_or_ge n k with (Hnk|Hnk)
+  · suffices c k ≡{n}≡ c n by cases _ : c k <;> simp_all
+    exact Hc Hnk
+  · suffices c k ≡{k}≡ c n by cases _ : c k <;> simp_all
+    exact (Hc Hnk).symm
+
+/-- If a chain of Option is ever some, it is the lift a chain by some. -/
+def chain_option_some [OFE V] {c : Chain (Option V)} (H : c n = some v) :
+    ∃ c' : Chain V, c = Chain.map ⟨some, OFE.Option.some.ne⟩ c' := by
+  have HVc (k) : ∃ v', c k = some v' := by
+    rcases h : c.chain k with (_|v')
+    · simp [chain_none_const h] at H
+    · exists v'
+  let c' : Chain V :=
+    ⟨fun n => Classical.choose <| HVc n,
+     by
+       intro n i Hni
+       have HR := c.cauchy Hni
+       rw [Classical.choose_spec (HVc n), Classical.choose_spec (HVc i)] at HR
+       exact HR ⟩
+  exists c'
+  rcases hcc : c with ⟨cc, Hcc⟩
+  simp only [Chain.map, Chain.mk.injEq]
+  refine funext (fun i => ?_)
+  simp only [c']
+  have Hchoose := Classical.choose_spec (HVc i)
+  rw [← Hchoose]
+  simp [hcc]
+
 /-- Complete ordered family of equivalences -/
 class IsCOFE (α : Type _) [OFE α] where
   compl : Chain α → α
@@ -788,3 +859,18 @@ instance [OFunctorContractive F] : OFunctorContractive (LaterOF F) where
     simp_all only [Dist, DistLater, Function.uncurry, OFunctor.map, laterMap]
 
 end LaterOF
+
+section subtype
+
+instance [OFE α] {P : α → Prop} : OFE { x : α // P x } where
+  Equiv := (·.val ≡ ·.val)
+  Dist n := (·.val ≡{n}≡ ·.val)
+  dist_eqv := {
+    refl x := dist_eqv.refl x.val
+    symm H := H.symm
+    trans H1 H2 := H1.trans H2
+  }
+  equiv_dist := equiv_dist
+  dist_lt := dist_lt
+
+end subtype
diff --git a/src/Iris/Algebra/Updates.lean b/src/Iris/Algebra/Updates.lean
index fda07960..b506f62e 100644
--- a/src/Iris/Algebra/Updates.lean
+++ b/src/Iris/Algebra/Updates.lean
@@ -110,7 +110,7 @@ theorem UpdateP.op {P Q R : α → Prop} {x y}
   exact ⟨z • w, pqr z w pz pw, CMRA.validN_ne (CMRA.op_opM_assoc_dist z w mz).symm vz⟩
 
 theorem UpdateP.op' {P Q : α → Prop} {x y : α} (uxp : x ~~>: P) (uyq : y ~~>: Q) :
-    x • y ~~>: λ t ↦ ∃ z w, t = (z • w : α) ∧ P z ∧ Q w :=
+    (x • y : α) ~~>: λ t ↦ ∃ z w, t = (z • w : α) ∧ P z ∧ Q w :=
   .op uxp uyq fun z w pz qw => ⟨z, w, rfl, pz, qw⟩
 
 theorem Update.op {x₁ x₂ y₁ y₂ : α} (xy₁ : x₁ ~~> y₁) (xy₂ : x₂ ~~> y₂) : x₁ • x₂ ~~> y₁ • y₂ :=