diff --git a/src/Iris/Algebra.lean b/src/Iris/Algebra.lean
index b9742cd4..55dd32e1 100644
--- a/src/Iris/Algebra.lean
+++ b/src/Iris/Algebra.lean
@@ -1,6 +1,13 @@
 import Iris.Algebra.Agree
 import Iris.Algebra.CMRA
 import Iris.Algebra.COFESolver
-import Iris.Algebra.OFE
+import Iris.Algebra.DFrac
+import Iris.Algebra.Excl
 import Iris.Algebra.Frac
+import Iris.Algebra.GenMap
+import Iris.Algebra.LocalUpdates
+import Iris.Algebra.IProp
+import Iris.Algebra.OFE
+import Iris.Algebra.Updates
+import Iris.Algebra.UPred
 import Iris.Algebra.Heap
diff --git a/src/Iris/Algebra/CMRA.lean b/src/Iris/Algebra/CMRA.lean
index 72cdb843..2efb7a56 100644
--- a/src/Iris/Algebra/CMRA.lean
+++ b/src/Iris/Algebra/CMRA.lean
@@ -94,6 +94,16 @@ class UCMRA (α : Type _) extends CMRA α where
   unit_left_id : unit • x ≡ x
   pcore_unit : pcore unit ≡ some unit
 
+class IsUnit [CMRA α] (ε : α) : Prop where
+  unit_valid : ✓ ε
+  unit_left_id : ε • x ≡ x
+  pcore_unit : CMRA.pcore ε ≡ some ε
+
+instance [UCMRA α] : IsUnit (UCMRA.unit : α) where
+  unit_valid := UCMRA.unit_valid
+  unit_left_id := UCMRA.unit_left_id
+  pcore_unit := UCMRA.pcore_unit
+
 namespace CMRA
 variable [CMRA α]
 
@@ -876,9 +886,6 @@ class RFunctorContractive (F : COFE.OFunctorPre) extends (RFunctor F) where
   map_contractive [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] :
     Contractive (Function.uncurry (@map α₁ α₂ β₁ β₂ _ _ _ _))
 
-variable (F T) in
-def RFunctor.ap [RFunctor F] [OFE T] := F T T
-
 attribute [instance] RFunctor.cmra
 
 
@@ -1034,8 +1041,8 @@ instance cmraOption : CMRA (Option α) where
     rename_i x
     rcases x1, x2, x with ⟨_|_, _|_, _|_⟩ <;> simp_all [op_right_dist]
   pcore_ne {n} x y cx H := by
-    simp only [some.injEq]; rintro rfl
-    rcases x, y with ⟨_|x, _|y⟩ <;> simp_all [Dist, Forall₂]
+    simp only [Option.some.injEq]; rintro rfl
+    rcases x, y with ⟨_|x, _|y⟩ <;> simp_all [Dist, Option.Forall₂]
     cases Hv : pcore x <;> cases Hv' : pcore y <;> simp only []
     · cases pcore_ne H.symm Hv'; simp_all
     · cases pcore_ne H Hv; simp_all
@@ -1043,7 +1050,7 @@ instance cmraOption : CMRA (Option α) where
       cases Hv.symm.trans Hw1
       exact Hw2.symm
   validN_ne {n} x y H := by
-    rcases x, y with ⟨_|_, _|_⟩ <;> simp_all [Dist, Forall₂]
+    rcases x, y with ⟨_|_, _|_⟩ <;> simp_all [Dist, Option.Forall₂]
     exact Dist.validN H |>.mp
   valid_iff_validN {x} := by
     rcases x with ⟨_|_⟩ <;> simp [valid_iff_validN]
@@ -1059,7 +1066,7 @@ instance cmraOption : CMRA (Option α) where
   pcore_op_left {x cx} := by
     rcases x, cx with ⟨_|_, _|_⟩ <;> simp_all [pcore_op_left]
   pcore_idem := by
-    rintro (_|x) <;> simp [Equiv, Forall₂]
+    rintro (_|x) <;> simp [Equiv, Option.Forall₂]
     rcases H : pcore x with _|y <;> simp
     obtain ⟨z, Hz1, Hz2⟩ := equiv_some (pcore_idem H)
     simp [Hz1, Hz2]
@@ -1396,26 +1403,3 @@ instance urFunctorContractiveOptionOF
 
 end optionOF
 
-section GenMap
-
-/-
-The OFE over gmaps is eqivalent to a non-depdenent discrete function to an `Option` type with a
-`Leibniz` OFE.
-In this setting, the CMRA is always unital, and as a consquence the oFunctors do not require
-unitality in order to act as a `URFunctor(Contractive)`.
--/
-
-variable (α β : Type _) [UCMRA β] [Leibniz β]
-
-abbrev GenMap := α → Option β
-
--- #synth CMRA (Option β)
--- #synth CMRA (α -d> (Option β))
--- #synth UCMRA (α -d> (Option β))
--- The synthesized UMRA here has unit (fun x => ε) = (fun x => none).
--- For us, this is equivalent to the Rocq-iris unit ∅.
-
-abbrev GenMapOF (C : Type _) (F : COFE.OFunctorPre) :=
-  DiscreteFunOF fun (_ : C) => OptionOF F
-
-end GenMap
diff --git a/src/Iris/Algebra/GenMap.lean b/src/Iris/Algebra/GenMap.lean
new file mode 100644
index 00000000..767a657b
--- /dev/null
+++ b/src/Iris/Algebra/GenMap.lean
@@ -0,0 +1,440 @@
+/-
+Copyright (c) 2025 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+import Iris.Algebra.OFE
+import Iris.Algebra.CMRA
+import Iris.Algebra.Updates
+
+namespace Iris
+open OFE
+
+section GenMap
+
+/- The OFE over gmaps is eqivalent to a non-depdenent discrete function to an `Option` type with a
+`Leibniz` OFE of keys, and an infinite number of unallocated elements.
+
+In this setting, the CMRA is always unital, and as a consquence the oFunctors do not require
+unitality in order to act as a `URFunctor(Contractive)`.
+
+GenMap is only intended to be used in the construction of the core IProp model. It is a stripped-down
+version of the generic heap constructions, which you should use instead. -/
+
+def alter [DecidableEq α] (f : α → β) (a : α) (b : β) : α → β :=
+  fun a' => if a = a' then b else f a'
+
+structure Enum (P : α → Prop) (enum : Nat → α) : Prop where
+  inc {n} : P (enum n)
+  inj {n m} : enum n = enum m → n = m
+
+def Poke [DecidableEq α] (enum : Nat → α) (n : Nat) : Nat → α :=
+  fun n' => if n' < n then enum n' else enum (n' + 1)
+
+def Infinite (P : α → Prop) : Prop := ∃ e, Enum P e
+
+def IsFree {β : α → Type _} (f : (a : α) → Option (β a)) : α → Prop := fun a => f a = none
+
+set_option grind.warning false
+theorem alter_isFree_infinite [DecidableEq α] {f : α → Option β} (H : Infinite (IsFree f)) :
+    Infinite (IsFree (alter f a b)) := by
+  rcases H with ⟨enum, Henum_inc, Henum_inj⟩
+  rcases Classical.em (∃ n₀, enum n₀ = a) with (⟨n₀, Hin⟩|Hout)
+  · refine ⟨Poke enum n₀, @fun n => ?_, @fun n m => ?_⟩
+    · simp [alter, IsFree]; split <;> rename_i h <;> revert h <;> simp [Poke]
+      · split <;> intro H <;> specialize Henum_inj (Hin ▸ H) <;> omega
+      · split <;> refine fun _ => Henum_inc
+    · simp [Poke]
+      split <;> split
+      all_goals intro H <;> specialize Henum_inj H <;> grind
+  · refine ⟨enum, @fun n => ?_, @fun n m Heq => ?_⟩
+    · simp only [not_exists] at Hout; specialize Hout n
+      simp only [IsFree, alter] at ⊢
+      split
+      · rename_i h; exact (Hout h.symm).elim
+      · exact Henum_inc
+    · exact Henum_inj Heq
+
+theorem Infinite.mono {P Q : α → Prop} (H : Infinite P) (Hmono : ∀ a, P a → Q a) : Infinite Q := by
+  rcases H with ⟨enum, Henum_inc, Henum_inj⟩
+  exact ⟨enum, Hmono (enum _) Henum_inc, Henum_inj⟩
+
+theorem Infinite.Nat_True : Infinite fun (_ : Nat) => True := ⟨id, trivial, id⟩
+
+section GenMapImpl
+
+-- abbrev GenMap := { f : α → Option β // Infinite (IsFree f) }
+structure GenMap (α β : Type _) where
+  car : α → Option β
+
+instance : CoeFun (GenMap α β) (fun _ => α → Option β) where
+  coe := GenMap.car
+
+nonrec def GenMap.alter [DecidableEq α] (g : GenMap α β) (a : α) (b : Option β) : GenMap α β where
+  car := alter g.car a b
+
+section OFE
+variable (α β : Type _) [OFE β]
+
+instance GenMap_instOFE : OFE (GenMap α β) where
+  Equiv := (·.car ≡ ·.car)
+  Dist n := (·.car ≡{n}≡ ·.car)
+  dist_eqv.refl _ := Dist.of_eq rfl
+  dist_eqv.symm := Dist.symm
+  dist_eqv.trans := Dist.trans
+  equiv_dist := equiv_dist
+  dist_lt := Dist.lt
+end OFE
+
+section CMRA
+
+variable (α β : Type _) [CMRA β]
+
+-- NB. Could use actual subtypes, but I will first attempt to do the subtyping on validity alone
+-- May make the OFunctors simpler because I just need to point them to GenMap instead
+-- of writing something new.
+-- Seems that the alter and alloc updates are still provable?
+instance instCMRA_GenMap : CMRA (GenMap α β) where
+  pcore x := Option.map GenMap.mk <| CMRA.pcore x.car
+  op x y := GenMap.mk (x.car • y.car)
+  ValidN n x := ✓{n} x.car ∧ (Infinite (IsFree x.car))
+  Valid x := ✓ x.car ∧ (Infinite (IsFree x.car))
+  op_ne.ne {_ _ _} H := CMRA.op_ne (α := α → Option β) |>.ne H
+  pcore_ne {n x y cx} H Hm := by
+    have Hm' : (CMRA.pcore x.car) = some cx.car := by
+      rcases h : (CMRA.pcore x.car)
+      · simp_all [h]
+      · simp_all [h]
+        rw [← Hm]
+    have H' : x.car ≡{n}≡ y.car := by exact H
+    rcases CMRA.pcore_ne H' Hm' with ⟨cy', Hcy'1, Hcy'2⟩
+    exact ⟨⟨cy'⟩, by simp [Hcy'1], Hcy'2⟩
+  validN_ne {n x y H} := by
+    refine fun ⟨Hv, ⟨e, Hf, Hi⟩⟩ => ⟨Dist.validN H |>.mp Hv, ?_⟩
+    refine ⟨e, @fun n => ?_, Hi⟩
+    specialize H (e n); specialize @Hf n; revert H Hf
+    cases _ : x.car (e n) <;> cases _ : y.car (e n) <;>
+    simp_all [IsFree, OFE.Dist, Option.Forall₂]
+  valid_iff_validN {x} := by
+    refine ⟨fun ⟨Hv, Hi⟩ n => ⟨Hv.validN, Hi⟩, fun H => ⟨?_, H 0 |>.2⟩⟩
+    exact CMRA.valid_iff_validN.mpr (H · |>.1)
+  validN_succ {x n} := fun ⟨Hv, Hi⟩ => ⟨CMRA.validN_succ Hv, Hi⟩
+  validN_op_left {n x y} := by
+    simp; rintro Hv Hf
+    refine ⟨CMRA.validN_op_left Hv, ?_⟩
+    refine Infinite.mono Hf (fun a => ?_)
+    simp [IsFree, CMRA.op, optionOp]
+    cases _ : x.car a <;> cases _ : y.car a  <;> simp
+  assoc {x y z} a := by
+    cases _ : x.car a <;> cases _ : y.car a <;> cases _ : z.car a <;>
+      simp_all [CMRA.op, OFE.Equiv, Option.Forall₂, optionOp]
+    exact CMRA.assoc
+  comm {x y} a := by
+    cases _ : x.car a <;> cases _ : y.car a <;>
+      simp_all [CMRA.op, OFE.Equiv, Option.Forall₂, optionOp]
+    exact CMRA.comm
+  pcore_op_left {x cx} H := by
+    rcases x with ⟨x⟩; rcases cx with ⟨cx⟩
+    have _ := CMRA.pcore_op_left (x := x) (cx := cx)
+    simp_all [OFE.Equiv]
+  pcore_idem {x cx} H := by
+    rcases x with ⟨x⟩; rcases cx with ⟨cx⟩
+    simp_all [OFE.Equiv, Option.Forall₂, Option.map]
+    apply CMRA.pcore_idem (x := x) (cx := cx)
+    simp [CMRA.pcore, H]
+  pcore_op_mono {x cx} := by
+    rcases x with ⟨x⟩; rcases cx with ⟨cx⟩; simp
+    refine fun H ⟨y⟩ => ?_
+    rcases CMRA.pcore_op_mono (x := x) (cx := cx) H y with ⟨cy, Hcy⟩
+    refine ⟨.mk cy, Hcy⟩
+  extend {n x y1 y2} := by
+    rintro ⟨Hv, _⟩ H
+    rcases CMRA.extend Hv H with ⟨z1, z2, _, _, _⟩
+    exists .mk z1
+    exists .mk z2
+
+instance instUCMRA_GenMap : UCMRA (GenMap Nat β) where
+  unit := GenMap.mk <| UCMRA.unit
+  unit_valid := ⟨fun _ => trivial, ⟨id, rfl, id⟩⟩
+  unit_left_id := by simp [CMRA.op, UCMRA.unit, optionOp]
+  pcore_unit := by simp [CMRA.pcore, UCMRA.unit, CMRA.core, optionCore]
+
+theorem GenMap.alter_valid [DecidableEq α] {g : GenMap α β} (Hb : ✓{n} b) (Hg : ✓{n} g) :
+    ✓{n} g.alter a b := by
+  rcases g with ⟨g⟩ <;> simp [GenMap.alter]
+  rcases Hg with ⟨Hv, Hi⟩
+  refine ⟨fun _ => ?_, alter_isFree_infinite Hi⟩
+  simp [Iris.alter] <;> split
+  · exact Hb
+  · exact Hv _
+
+theorem GenMap.valid_exists_fresh {g : GenMap α β} (Hv : ✓{n} g) : ∃ a : α, g.car a = none := by
+  rcases Hv with ⟨_, e, He_inc, _⟩
+  exact ⟨e 0, He_inc⟩
+
+end CMRA
+
+section OFunctors
+open COFE
+
+abbrev GenMapOF (C : Type _) (F : OFunctorPre) : OFunctorPre :=
+  fun A B _ _ => GenMap C (F A B)
+
+abbrev GenMap.lift [OFE α] [OFE β] (f : α -n> β) : GenMap T α -n> GenMap T β where
+  f g := .mk fun t => Option.map f (g.car t)
+  ne.ne {n x1 x2} H γ := by
+    specialize H γ
+    simp [Option.map]
+    split <;> split <;> simp_all
+    exact NonExpansive.ne H
+
+instance GenMapOF_instOFunctor (F : OFunctorPre) [OFunctor F] :
+    OFunctor (GenMapOF Nat F) where
+  cofe {A B _ _} := GenMap_instOFE Nat (F A B)
+  map f₁ f₂ := GenMap.lift <| OFunctor.map (F := F) f₁ f₂
+  map_ne.ne {n x1 x2} Hx {y1 y2} Hy k γ := by
+    simp only [OFE.Dist, Option.Forall₂, Option.map]
+    cases _ : k.car γ <;> simp
+    exact OFunctor.map_ne.ne Hx Hy _
+  map_id {α β _ _} x γ := by
+    simp only [Option.map]
+    cases _ : x.car γ <;> simp
+    exact OFunctor.map_id _
+  map_comp _ _ _ _ x γ := by
+    simp only [Option.map]
+    cases _ : x.car γ <;> simp
+    exact OFunctor.map_comp _ _ _ _ _
+
+-- TODO: Cleanup
+instance GenMapOF_instURFunctor (F : COFE.OFunctorPre) [RFunctor F] :
+    URFunctor (GenMapOF Nat F) where
+  map f g := {
+    toHom := GenMap.lift <| COFE.OFunctor.map f g
+    validN {n x} hv := by
+      rcases hv with ⟨hv, ⟨e, Hf, Hi⟩⟩
+      refine ⟨fun z => ?_, ⟨e, @fun n => ?_, Hi⟩⟩
+      · cases h : x.car z <;> simp [Option.map, CMRA.ValidN, optionValidN, h]
+        rename_i _ α₁ α₂ β₁ β₂ _ _ _ _ v
+        let Hvalid := @(URFunctor.map (F := OptionOF F) f g).validN n v
+        simp [CMRA.ValidN, optionValidN, h, URFunctor.map] at Hvalid
+        specialize Hvalid ?_
+        · specialize hv z
+          simp [CMRA.ValidN, optionValidN] at hv
+          simp [h] at hv
+          exact hv
+        exact Hvalid
+      · specialize @Hf n
+        simp [IsFree, Option.map] at Hf ⊢
+        simp [Hf]
+    pcore x γ := by
+      let Hcore := @(URFunctor.map (F := OptionOF F) f g).pcore (x.car γ)
+      simp [Option.map] at Hcore ⊢
+      cases h : (x.car γ) <;> simp [CMRA.core, Option.getD, optionCore] at Hcore ⊢
+      rename_i v
+      simp [OFE.Equiv, Option.Forall₂, URFunctor.map, Option.bind, h, optionCore, OFunctor.map, optionMap, Option.map] at Hcore
+      cases h' : CMRA.pcore v
+      · simp_all [h']
+        cases h'' : CMRA.pcore ((OFunctor.map f g).f v) <;> simp_all
+        simp_all [RFunctor.toOFunctor]
+      · simp_all [h']
+        cases h'' : CMRA.pcore ((OFunctor.map f g).f v) <;> simp_all [RFunctor.toOFunctor]
+    op z x γ := by
+      let Hop := @(URFunctor.map (F := OptionOF F) f g).op (z.car γ) (x.car γ)
+      simp [Option.map, RFunctor.toOFunctor, optionCore, CMRA.op, optionOp, Option.bind,
+           URFunctor.map] at Hop ⊢
+      cases h : z.car γ <;> cases h' : x.car γ <;> simp
+      simp [h, h'] at Hop
+      simp_all [OFunctor.map, optionMap, RFunctor.toOFunctor]
+  }
+  map_ne.ne := COFE.OFunctor.map_ne.ne
+  map_id := COFE.OFunctor.map_id
+  map_comp := COFE.OFunctor.map_comp
+
+instance GenMapOF_instURFC (F : COFE.OFunctorPre) [HURF : RFunctorContractive F] :
+    URFunctorContractive (GenMapOF Nat F) where
+  map_contractive.1 h x n := by
+    rename_i n x' y'
+    let Heqv := @(URFunctorContractive.map_contractive (F := OptionOF F)).1 _ x' y' h (x.car n)
+    simp [Function.uncurry, URFunctor.map, Option.map] at Heqv ⊢
+    cases h : x.car n <;> simp
+    rw [h] at Heqv
+    exact Heqv
+
+end OFunctors
+
+section updates
+
+-- Which gmap updates do we need?
+
+end updates
+
+
+/-
+Lemma insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
+  x ~~>: P →
+  (∀ y, P y → Q (<[i:=y]>m)) →
+  <[i:=x]>m ~~>: Q.
+Proof.
+  intros Hx%option_updateP' HP; apply cmra_total_updateP=> n mf Hm.
+  destruct (Hx n (Some (mf !! i))) as ([y|]&?&?); try done.
+  { by generalize (Hm i); rewrite lookup_op; simplify_map_eq. }
+  exists (<[i:=y]> m); split; first by auto.
+  intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm.
+  destruct (decide (i = j)); simplify_map_eq/=; auto.
+Qed.
+Lemma insert_updateP' (P : A → Prop) m i x :
+  x ~~>: P → <[i:=x]>m ~~>: λ m', ∃ y, m' = <[i:=y]>m ∧ P y.
+Proof. eauto using insert_updateP. Qed.
+Lemma insert_update m i x y : x ~~> y → <[i:=x]>m ~~> <[i:=y]>m.
+Proof. rewrite !cmra_update_updateP; eauto using insert_updateP with subst. Qed.
+
+Lemma singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x :
+  x ~~>: P → (∀ y, P y → Q {[ i := y ]}) → {[ i := x ]} ~~>: Q.
+Proof. apply insert_updateP. Qed.
+Lemma singleton_updateP' (P : A → Prop) i x :
+  x ~~>: P → {[ i := x ]} ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
+Proof. apply insert_updateP'. Qed.
+Lemma singleton_update i (x y : A) : x ~~> y → {[ i := x ]} ~~> {[ i := y ]}.
+Proof. apply insert_update. Qed.
+
+Lemma delete_update m i : m ~~> delete i m.
+Proof.
+  apply cmra_total_update=> n mf Hm j; destruct (decide (i = j)); subst.
+  - move: (Hm j). rewrite !lookup_op lookup_delete_eq left_id.
+    apply cmra_validN_op_r.
+  - move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
+Qed.
+
+
+
+
+
+Section freshness.
+  Local Set Default Proof Using "Type*".
+  Context `{!Infinite K}.
+  Lemma alloc_updateP_strong_dep (Q : gmap K A → Prop) (I : K → Prop) m (f : K → A) :
+    pred_infinite I →
+    (∀ i, m !! i = None → I i → ✓ (f i)) →
+    (∀ i, m !! i = None → I i → Q (<[i:=f i]>m)) → m ~~>: Q.
+  Proof.
+    move=> /(pred_infinite_set I (C:=gset K)) HP ? HQ.
+    apply cmra_total_updateP. intros n mf Hm.
+    destruct (HP (dom (m ⋅ mf))) as [i [Hi1 Hi2]].
+    assert (m !! i = None).
+    { eapply not_elem_of_dom. revert Hi2.
+      rewrite dom_op not_elem_of_union. naive_solver. }
+    exists (<[i:=f i]>m); split.
+    - by apply HQ.
+    - rewrite insert_singleton_op //.
+      rewrite -assoc -insert_singleton_op; last by eapply not_elem_of_dom.
+    apply insert_validN; [apply cmra_valid_validN|]; auto.
+  Qed.
+  Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : K → Prop) m x :
+    pred_infinite I →
+    ✓ x → (∀ i, m !! i = None → I i → Q (<[i:=x]>m)) → m ~~>: Q.
+  Proof.
+    move=> HP ? HQ. eapply (alloc_updateP_strong_dep _ _ _ (λ _, x)); eauto.
+  Qed.
+  Lemma alloc_updateP (Q : gmap K A → Prop) m x :
+    ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
+  Proof.
+    move=>??.
+    eapply (alloc_updateP_strong _ (λ _, True));
+    eauto using pred_infinite_True.
+  Qed.
+  Lemma alloc_updateP_cofinite (Q : gmap K A → Prop) (J : gset K) m x :
+    ✓ x → (∀ i, m !! i = None → i ∉ J → Q (<[i:=x]>m)) → m ~~>: Q.
+  Proof.
+    eapply alloc_updateP_strong.
+    apply (pred_infinite_set (C:=gset K)).
+    intros E. exists (fresh (J ∪ E)).
+    apply not_elem_of_union, is_fresh.
+  Qed.
+
+  (* Variants without the universally quantified Q, for use in case that is an evar. *)
+  Lemma alloc_updateP_strong_dep' m (f : K → A) (I : K → Prop) :
+    pred_infinite I →
+    (∀ i, m !! i = None → I i → ✓ (f i)) →
+    m ~~>: λ m', ∃ i, I i ∧ m' = <[i:=f i]>m ∧ m !! i = None.
+  Proof. eauto using alloc_updateP_strong_dep. Qed.
+  Lemma alloc_updateP_strong' m x (I : K → Prop) :
+    pred_infinite I →
+    ✓ x → m ~~>: λ m', ∃ i, I i ∧ m' = <[i:=x]>m ∧ m !! i = None.
+  Proof. eauto using alloc_updateP_strong. Qed.
+  Lemma alloc_updateP' m x :
+    ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
+  Proof. eauto using alloc_updateP. Qed.
+  Lemma alloc_updateP_cofinite' m x (J : gset K) :
+    ✓ x → m ~~>: λ m', ∃ i, i ∉ J ∧ m' = <[i:=x]>m ∧ m !! i = None.
+  Proof. eauto using alloc_updateP_cofinite. Qed.
+End freshness.
+
+Lemma alloc_unit_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) u i :
+  ✓ u → LeftId (≡) u (⋅) →
+  u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
+Proof.
+  intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
+  destruct (Hx n (gf !! i)) as (y&?&Hy).
+  { move:(Hg i). rewrite !left_id.
+    case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
+    intros; by apply cmra_valid_validN. }
+  exists {[ i := y ]}; split; first by auto.
+  intros i'; destruct (decide (i' = i)) as [->|].
+  - rewrite lookup_op lookup_singleton_eq.
+    move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
+  - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
+Qed.
+Lemma alloc_unit_singleton_updateP' (P: A → Prop) u i :
+  ✓ u → LeftId (≡) u (⋅) →
+  u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
+Proof. eauto using alloc_unit_singleton_updateP. Qed.
+Lemma alloc_unit_singleton_update (u : A) i (y : A) :
+  ✓ u → LeftId (≡) u (⋅) → u ~~> y → (∅:gmap K A) ~~> {[ i := y ]}.
+Proof.
+  rewrite !cmra_update_updateP;
+    eauto using alloc_unit_singleton_updateP with subst.
+Qed.
+-/
+
+-- def GenMapOF (C : Type _) (F : C → COFE.OFunctorPre) : COFE.OFunctorPre :=
+--   fun A B => { f : (c : C) → OptionOF (F c) A B // Infinite (IsFree f) }
+
+-- TODO: CMRA instances, updates for alloc + modify, urFunctor instance for when F is always an rFunctor
+-- Functor merges
+--    urFunctorOptionOF [RFunctor F] : URFunctor (OptionOF F) where
+-- instance urFunctorContractiveOptionOF [RFunctorContractive F] : URFunctorContractive (OptionOF F) where
+--    DiscreteFunOF_URFC {C} (F : C → COFE.OFunctorPre) [HURF : ∀ c, URFunctorContractive (F c)] :
+-- So it should expect ∀ c, (RFunctorContractive c)
+
+-- instance instURFunctor_GenMapOF {F : C → COFE.OFunctorPre} [∀ c, RFunctorContractive (F c)] :
+--     URFunctor (GenMapOF C F) :=
+--   sorry
+
+end GenMapImpl
+
+end GenMap
+--
+--
+-- -- TODO: Move to a new file
+--
+-- section Functions
+--
+-- variable {α : Type _} {β : α → Type _} [∀ x, UCMRA (β x)]
+--
+-- -- Updates for base CMRA's
+--
+-- theorem singleton_updateP_empty [DecidableEq α] {x : α} {P : β x → Prop} {Q : (∀ x, β x) → Prop} :
+--   (UCMRA.unit ~~>: P) →
+--   (∀ y2 : β x, P y2 → Q (fun a' => if h : a' = x then h ▸ y2 else UCMRA.unit)) →
+--   (UCMRA.unit ~~>: Q) := sorry
+--
+--
+-- -- (P : {x : α} → β x → Prop)
+-- --     (Q : ((a : α) → Option (β a)) → Prop) : True := sor
+--   -- (UCMRA.unit ~~>: P) → (∀ y2 : β x, P y2 → Q (alter (fun _ => UCMRA.unit) x y2)) := sorry
+-- --
+-- --         (P : β x → Prop) (Q : ((a : α) → Option (β a)) → Prop) :
+-- --     (ε ~~>: P) → (∀ y2 : β x, P y2 → Q (singleton x y2)) → ε ~~>: Q := sorry
+-- --   Proof.
+--
+-- end Functions
diff --git a/src/Iris/Algebra/IProp.lean b/src/Iris/Algebra/IProp.lean
index dd5b718b..743ded04 100644
--- a/src/Iris/Algebra/IProp.lean
+++ b/src/Iris/Algebra/IProp.lean
@@ -7,43 +7,52 @@ Authors: Markus de Medeiros
 import Iris.Algebra.CMRA
 import Iris.Algebra.OFE
 import Iris.Algebra.UPred
+import Iris.Algebra.GenMap
 import Iris.Algebra.COFESolver
 import Init.Data.Vector
 
 namespace Iris
 
-def GFunctors := Array COFE.OFunctorPre
+open COFE
+
+abbrev GType := Nat
 
-def GId (FF : GFunctors) : Type _ := Fin FF.size
+def BundledGFunctors := GType → Σ F : OFunctorPre, RFunctorContractive F
 
-instance (FF : GFunctors) : GetElem GFunctors (GId FF) COFE.OFunctorPre (fun _ _ => True) where
-  getElem _ x _ := (show Array _ from FF)[x.1]
+def BundledGFunctors.default : BundledGFunctors := fun _ => ⟨COFE.constOF Unit, by infer_instance⟩
 
-abbrev IsGFunctors (G : GFunctors) := ∀ (i : GId G), RFunctorContractive G[i]
+def BundledGFunctors.set (GF : BundledGFunctors) (i : Nat) (FB : Σ F, RFunctorContractive F) :
+    BundledGFunctors :=
+  fun j => if j = i then FB else GF j
 
-def SubG (FF₁ FF₂ : GFunctors) : Prop :=
-  ∀ i : GId FF₁, ∃ j : GId FF₂, FF₁[i] = FF₂[j]
+abbrev GName := Nat
 
-def GName := LeibnizO Nat
+abbrev IResF (GF : BundledGFunctors) : OFunctorPre :=
+  DiscreteFunOF (fun i => GenMapOF GName (GF i).fst)
 
-abbrev IResF (FF : GFunctors) : COFE.OFunctorPre :=
-  DiscreteFunOF (fun i : GId FF => GenMapOF GName FF[i])
+instance (GF : BundledGFunctors) (i : GName) : RFunctorContractive ((GF i).fst) := (GF i).snd
 
 section IProp
-open COFE
 
-variable (FF : GFunctors) [IG : IsGFunctors FF]
+variable (GF : BundledGFunctors)
 
-def iPrePropO : Type _ := OFunctor.Fix (UPredOF (IResF FF))
+def IPre : Type _ := OFunctor.Fix (UPredOF (IResF GF))
 
-instance : COFE (iPrePropO FF) := inferInstanceAs (COFE (OFunctor.Fix _))
+instance : COFE (IPre GF) := inferInstanceAs (COFE (OFunctor.Fix _))
 
-def IResUR : Type := (i : GId FF) → GName → Option (FF[i] (iPrePropO FF) (iPrePropO FF))
+def IResUR : Type := (i : GType) → GenMap Nat (GF i |>.fst (IPre GF) (IPre GF))
 
-instance : UCMRA (IResUR FF) :=
-  ucmraDiscreteFunO (β := fun (i : GId FF) => GName → Option (FF[i] (iPrePropO FF) (iPrePropO FF)))
+instance : UCMRA (IResUR GF) :=
+  ucmraDiscreteFunO (β := fun (i : GType) => GenMap GName (GF i |>.fst (IPre GF) (IPre GF)))
 
-abbrev IProp := UPred (IResUR FF)
+abbrev IProp := UPred (IResUR GF)
+
+def IProp.unfold : IProp GF -n> IPre GF :=
+  OFE.Iso.hom <| OFunctor.Fix.iso (F := (UPredOF (IResF GF)))
+
+def IProp.fold : IPre GF -n> IProp GF :=
+  OFE.Iso.inv <| OFunctor.Fix.iso (F := (UPredOF (IResF GF)))
 
 end IProp
+
 end Iris
diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index f44b0327..4a95a745 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -670,6 +670,11 @@ def optionMap {α β : Type _} [OFE α] [OFE β] (f : α -n> β) : Option α -n>
   rintro _ ⟨⟩ ⟨⟩ H <;> simp_all [Dist, Option.Forall₂]
   exact f.ne.ne H
 
+theorem Option.map_forall₂ {α β : Type _} [OFE α] [OFE β] (f : α → β) [hf : OFE.NonExpansive f]
+    {o1 o2 : Option α} (h : o1 ≡ o2) : o1.map f ≡ o2.map f := by
+  cases o1 <;> cases o2 <;> simp_all []
+  exact hf.eqv h
+
 end Option
 
 section OptionOF
@@ -873,3 +878,8 @@ instance [OFE α] {P : α → Prop} : OFE { x : α // P x } where
   dist_lt := dist_lt
 
 end subtype
+
+theorem OFE.cast_dist [Iα : OFE α] [Iβ : OFE β] {x y : α}
+    (Ht : α = β) (HIt : Iα = Ht ▸ Iβ)  (H : x ≡{n}≡ y) :
+    (Ht ▸ x) ≡{n}≡ (Ht ▸ y) := by
+  subst Ht; subst HIt; exact H
diff --git a/src/Iris/Algebra/UPred.lean b/src/Iris/Algebra/UPred.lean
index 3bf7f0b4..6890ff20 100644
--- a/src/Iris/Algebra/UPred.lean
+++ b/src/Iris/Algebra/UPred.lean
@@ -81,7 +81,7 @@ instance [URFunctor F] : COFE.OFunctor (UPredOF F) where
   map_id _ _ z _ := uPred_proper <| URFunctor.map_id z
   map_comp f g f' g' _ _ H _ := uPred_proper <| URFunctor.map_comp g' f' g f H
 
-instance [URFunctorContractive F] : COFE.OFunctorContractive (UPredOF F) where
+instance instUPredOFunctorContractive [URFunctorContractive F] : COFE.OFunctorContractive (UPredOF F) where
   map_contractive.1 {_ x y} HKL _ _ _ Hn _ := by
     refine uPred_ne <| (URFunctorContractive.map_contractive.1
       (x := (x.snd, x.fst)) (y := (y.snd, y.fst)) ?_ _).le Hn
diff --git a/src/Iris/BI/DerivedLaws.lean b/src/Iris/BI/DerivedLaws.lean
index 8913e26b..b76e8ba9 100644
--- a/src/Iris/BI/DerivedLaws.lean
+++ b/src/Iris/BI/DerivedLaws.lean
@@ -1470,6 +1470,12 @@ theorem persistent_and_sep_1 [BI PROP] {P Q : PROP} :
   | TCOr.l => persistent_and_affinely_sep_l_1.trans (sep_mono_l affinely_elim)
   | TCOr.r => persistent_and_affinely_sep_r_1.trans (sep_mono_r affinely_elim)
 
+theorem persistent_entails_r [BI PROP] {P Q : PROP} [Persistent Q] (H : P ⊢ Q) : P ⊢ Q ∗ P :=
+  (and_intro H .rfl).trans persistent_and_sep_1
+
+theorem persistent_entails_l [BI PROP] {P Q : PROP} [Persistent Q] (H : P ⊢ Q) : P ⊢ P ∗ Q :=
+  (and_intro .rfl H).trans persistent_and_sep_1
+
 theorem absorbingly_intuitionistically [BI PROP] {P : PROP} : <absorb> □ P ⊣⊢ <pers> P :=
   ⟨(absorbingly_mono persistently_of_intuitionistically).trans absorbingly_persistently.1,
    and_self.2.trans <| persistently_and_intuitionistically_sep_r.1.trans <| sep_mono_l true_intro⟩
diff --git a/src/Iris/Examples/IProp.lean b/src/Iris/Examples/IProp.lean
new file mode 100644
index 00000000..8760310c
--- /dev/null
+++ b/src/Iris/Examples/IProp.lean
@@ -0,0 +1,58 @@
+/-
+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.IProp
+import Iris.Algebra.Agree
+
+namespace Iris.Examples
+open Iris.BI COFE
+
+section Example1
+
+abbrev F0 : OFunctorPre := constOF (Agree (LeibnizO String))
+
+variable {GF} [E0 : ElemG GF F0]
+
+private theorem autoverse : ⊢
+    (|==> ∃ (γ : GName), iOwn (F := F0) γ (toAgree ⟨"Paul Durham"⟩) : IProp GF) := by
+  apply iOwn_alloc
+  exact fun _ => trivial
+
+example : ⊢ |==> ∃ (γ0 γ1 : GName) (s0 s1 : String),
+    iOwn (E := E0) γ0 (toAgree ⟨s0⟩) ∗
+    iOwn (E := E0) γ1 (toAgree ⟨s1⟩) := by
+  let v0 : F0.ap (IProp GF) := toAgree ⟨"string0"⟩
+  let v1 : F0.ap (IProp GF) := toAgree ⟨"string1"⟩
+
+  -- Allocate the resources
+  refine emp_sep.mpr.trans <| (sep_mono (iOwn_alloc v1 (fun _ => trivial)) .rfl).trans ?_
+  refine emp_sep.mpr.trans <| (sep_mono (iOwn_alloc v0 (fun _ => trivial)) .rfl).trans ?_
+
+  -- Eliminate the bupds (by hand, until iMod is implemented)
+  refine BIUpdate.frame_r.trans ?_
+  refine BIUpdate.mono (sep_mono .rfl BIUpdate.frame_r) |>.trans ?_
+  refine BIUpdate.mono bupd_frame_l |>.trans ?_
+  refine BIUpdate.trans.trans ?_
+  refine BIUpdate.mono ?_
+
+  -- Complete the Iris proof
+  istart
+  iintro ⟨⟨γ0, Hγ0⟩, ⟨γ1, Hγ1⟩, -⟩
+  iexists γ0
+  iexists γ1
+  iexists "string0"
+  iexists "string1"
+  isplitl [Hγ0]
+  · iexact Hγ0
+  · iexact Hγ1
+
+
+end Example1
+
+
+end Iris.Examples
diff --git a/src/Iris/Examples/Resources.lean b/src/Iris/Examples/Resources.lean
index b3f26e50..d7f67c99 100644
--- a/src/Iris/Examples/Resources.lean
+++ b/src/Iris/Examples/Resources.lean
@@ -7,19 +7,18 @@ import Iris.BI
 import Iris.ProofMode
 import Iris.Algebra.IProp
 import Iris.Instances.UPred.Instance
+import Iris.Instances.IProp.Instance
 import Iris.Algebra.Agree
 
 namespace Iris.Examples
-open Iris.BI
+open Iris.BI COFE
 
 section no_resources
 
-abbrev FF0 : GFunctors := #[]
-
-local instance : IsGFunctors FF0 := nofun
+variable [UCMRA M]
 
 -- A proof with no resources
-example (P Q : IProp FF0) : P ∗ Q ⊢ ⌜True⌝ := by
+example (P Q : UPred M) : P ∗ Q ⊢ ⌜True⌝ := by
   iintro ⟨HP, HQ⟩
   ipure_intro
   trivial
@@ -32,27 +31,16 @@ end no_resources
 
 section const_agree
 
-abbrev FF1 : GFunctors := #[COFE.constOF (Agree (LeibnizO String))]
-abbrev γ : GId FF1 := ⟨0, Nat.zero_lt_succ _⟩
-theorem HγE  (i : GId FF1) : i = γ := by unfold γ; cases i; congr; apply Nat.lt_one_iff.mp; trivial
-theorem HγLookup : FF1[γ] = COFE.constOF (Agree (LeibnizO String)) := rfl
-local instance : IsGFunctors FF1 := fun i => by rw [HγE i, HγLookup]; infer_instance
-
-@[simp]
-def MyAg (S : String) : Agree (LeibnizO String) := ⟨[⟨S⟩], by simp⟩
+abbrev γ : GType := 1
 
 @[simp]
-def MyR (S : String) : IResUR FF1 := fun i _ => some (HγE i ▸ MyAg S)
+def MyAg (S : String) : (Option (Agree (LeibnizO String))) := some ⟨[⟨S⟩], by simp⟩
 
-theorem MyR_always_invalid (S₁ S₂ : String) (Hne : S₁ ≠ S₂) (n : Nat) : ¬✓{n} MyR S₁ • MyR S₂ := by
-  simp [CMRA.op, CMRA.ValidN]
-  exists γ, ⟨0⟩
-  rw [← HγE ⟨Nat.zero, Nat.le.refl⟩]
-  simp [instIsGFunctorsFF1, CMRA.ValidN, CMRA.op, Agree.op, Agree.validN,
-        instCOFELeibnizO, COFE.ofDiscrete, OFE.ofDiscrete]
-  exact fun a => id (Ne.symm Hne)
+theorem MyR_always_invalid (S₁ S₂ : String) (Hne : S₁ ≠ S₂) (n : Nat) : ¬✓{n} MyAg S₁ • MyAg S₂ := by
+  simp only [CMRA.ValidN, CMRA.op, MyAg, optionValidN, optionOp]
+  exact (Hne <| LeibnizO.dist_inj <| Agree.toAgree_op_validN_iff_dist.mp ·)
 
-def AgreeString (S : String) : IProp FF1 := UPred.ownM (MyR S)
+def AgreeString (S : String) : UPred (Option (Agree (LeibnizO String))) := UPred.ownM (MyAg S)
 
 example : AgreeString "I <3 iris-lean!" ⊢ (AgreeString "I don't :<" -∗ False) := by
   iintro H H2
@@ -63,4 +51,5 @@ example : AgreeString "I <3 iris-lean!" ⊢ (AgreeString "I don't :<" -∗ False
   apply MyR_always_invalid; simp       -- Simplify
 
 end const_agree
+
 end Iris.Examples
diff --git a/src/Iris/Instances/IProp.lean b/src/Iris/Instances/IProp.lean
new file mode 100644
index 00000000..0e63032b
--- /dev/null
+++ b/src/Iris/Instances/IProp.lean
@@ -0,0 +1 @@
+import Iris.Instances.IProp.Instance
diff --git a/src/Iris/Instances/IProp/Instance.lean b/src/Iris/Instances/IProp/Instance.lean
new file mode 100644
index 00000000..e8586542
--- /dev/null
+++ b/src/Iris/Instances/IProp/Instance.lean
@@ -0,0 +1,797 @@
+/-
+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, Zongyuan Liu
+-/
+
+import Iris.BI
+import Iris.Algebra
+import Iris.Instances.UPred
+namespace Iris
+
+-- TODO: Cleanup namespaces and variables for each section
+
+open COFE
+
+/-- Apply an OFunctor at a fixed type -/
+abbrev COFE.OFunctorPre.ap (F : OFunctorPre) (T : Type _) [OFE T] :=
+  F T T
+
+/-- Apply a list of OFunctors at a fixed type and index -/
+abbrev BundledGFunctors.api (FF : BundledGFunctors) (τ : GType) (T : Type _) [OFE T] :=
+  FF τ |>.fst |>.ap T
+
+/-- Transport an OFunctorPre application along equality of the OFunctorPre.  -/
+def TranspAp {F1 F2 : OFunctorPre} (H : F1 = F2) {T} [OFE T] : F1.ap T = F2.ap T :=
+  congrArg (OFunctorPre.ap · T) H
+
+section TranspAp
+
+variable [RF₁ : RFunctorContractive F₁] [RF₂ : RFunctorContractive F₂] [OFE T]
+
+theorem OFE.transpAp_eqv_mp (h_fun : F₁ = F₂) (h_inst : HEq RF₁ RF₂) {x y : F₁.ap T} (H : x ≡{n}≡ y) :
+    (TranspAp h_fun).mp x ≡{n}≡ (TranspAp h_fun).mp y := by
+  cases h_fun; cases eq_of_heq h_inst; exact H
+
+theorem OFE.transpAp_op_mp (h_fun : F₁ = F₂) (h_inst : HEq RF₁ RF₂) {x y : F₁ T T} :
+    (TranspAp h_fun).mp (x • y) ≡ (TranspAp h_fun).mp x • (TranspAp h_fun).mp y := by
+  cases h_fun; cases eq_of_heq h_inst; rfl
+
+theorem OFE.transpAp_pcore_mp (h_fun : F₁ = F₂) (h_inst : HEq RF₁ RF₂) {x : F₁ T T} :
+    (CMRA.pcore x).map (TranspAp h_fun).mp ≡ CMRA.pcore ((TranspAp h_fun).mp x) := by
+  cases h_fun; cases eq_of_heq h_inst
+  simp [Equiv, Option.Forall₂]
+  cases CMRA.pcore x <;> simp [Equiv.rfl]
+
+theorem OFE.transpAp_validN_mp (h_fun : F₁ = F₂) (h_inst : HEq RF₁ RF₂) {x : F₁ T T} (H : ✓{n} x) :
+    ✓{n} ((TranspAp h_fun).mp x) := by
+  cases h_fun; cases eq_of_heq h_inst; exact H
+
+theorem OFE.validN_transpAp_mp (h_fun : F₁ = F₂) (h_inst : HEq RF₁ RF₂) {x : F₁ T T}
+    (H : ✓{n} ((TranspAp h_fun).mp x)) : ✓{n} x := by
+  cases h_fun; cases eq_of_heq h_inst; exact H
+
+end TranspAp
+
+section ElemG
+
+class ElemG (FF : BundledGFunctors) (F : OFunctorPre) [RFunctorContractive F] where
+  τ : GType
+  transp : FF τ = ⟨F, ‹_›⟩
+
+open OFE
+
+variable [I : RFunctorContractive F]
+
+def ElemG.TranspMap  (E : ElemG GF F) T [OFE T] : (GF E.τ).fst = F :=
+  Sigma.mk.inj E.transp |>.1
+
+def ElemG.TranspClass (E : ElemG GF F) T [OFE T] : HEq (GF E.τ).snd I :=
+  Sigma.mk.inj E.transp |>.2
+
+def ElemG.Bundle  (E : ElemG GF F) [OFE T] : F.ap T → GF.api E.τ T :=
+  TranspAp (E.TranspMap T) |>.mpr
+
+def ElemG.Unbundle  (E : ElemG GF F) [OFE T] : GF.api E.τ T → F.ap T :=
+  TranspAp (E.TranspMap T) |>.mp
+
+theorem ElemG.Bundle_Unbundle  (E : ElemG GF F) [OFE T] (x : GF.api E.τ T) :
+    E.Bundle (E.Unbundle x) ≡ x := by simp [Bundle, Unbundle]
+
+theorem ElemG.Unbundle_Bundle (E : ElemG GF F) [OFE T] (x : F.ap T) :
+    E.Unbundle (E.Bundle x) ≡ x := by simp [Bundle, Unbundle]
+
+instance ElemG.Bundle.ne {E : ElemG GF F} [OFE T] :
+    OFE.NonExpansive (E.Bundle (T := T)) where
+  ne {_ _ _} := OFE.transpAp_eqv_mp (E.TranspMap T).symm (E.TranspClass T).symm
+
+instance ElemG.Unbundle.ne {E : ElemG GF F} [OFE T] :
+    OFE.NonExpansive (E.Unbundle (T := T)) where
+  ne {_ _ _} H := OFE.transpAp_eqv_mp (E.TranspMap T) (E.TranspClass T) H
+
+end ElemG
+
+section Fold
+
+open Iris COFE UPred
+
+variable {FF : BundledGFunctors}
+
+/-- Isorecursive unfolding for each projection of FF. -/
+def IProp.unfoldi : FF.api τ (IProp FF) -n> FF.api τ (IPre FF) :=
+  OFunctor.map (IProp.fold FF) (IProp.unfold FF)
+
+/-- Isorecursive folding for each projection of FF. -/
+def IProp.foldi : FF.api τ (IPre FF) -n> FF.api τ (IProp FF) :=
+  OFunctor.map (IProp.unfold FF) (IProp.fold FF)
+
+theorem IProp.unfoldi_foldi (x : FF.api τ (IPre FF)) : unfoldi (foldi x) ≡ x := by
+  refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm ?_
+  refine .trans ?_ (OFunctor.map_id (F := FF τ |>.fst) x)
+  apply OFunctor.map_ne.eqv <;> intro _ <;> simp [IProp.unfold, IProp.fold]
+
+theorem IProp.foldi_unfoldi (x : FF.api τ (IProp FF)) : foldi (unfoldi x) ≡ x := by
+  refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm ?_
+  refine .trans ?_ (OFunctor.map_id (F := FF τ |>.fst) x)
+  apply OFunctor.map_ne.eqv <;> intro _ <;> simp [IProp.unfold, IProp.fold]
+
+theorem IProp.foldi_op (x y : FF.api τ (IPre FF)) : foldi (x • y) ≡ foldi x • foldi y :=
+  RFunctor.map (IProp.unfold FF) (IProp.fold FF) |>.op _ _
+
+theorem IProp.foldi_validN {n : Nat} (x : FF.api τ (IPre FF)) (H : ✓{n} x) : ✓{n} (foldi x) :=
+  RFunctor.map (IProp.unfold FF) (IProp.fold FF) |>.validN H
+
+theorem IProp.unfoldi_validN {n : Nat} (x : FF.api τ (IProp FF)) (H : ✓{n} x) : ✓{n} (unfoldi x) :=
+  RFunctor.map (IProp.fold FF) (IProp.unfold FF) |>.validN H
+
+theorem IProp.validN_foldi {n : Nat} (x : FF.api τ (IPre FF)) (H : ✓{n} (foldi x)) : ✓{n} x :=
+  CMRA.validN_ne (IProp.unfoldi_foldi x).dist (IProp.unfoldi_validN _ H)
+
+theorem IProp.validN_unfoldi {n : Nat} (x : FF.api τ (IProp FF)) (H : ✓{n} (unfoldi x)) : ✓{n} x :=
+  CMRA.validN_ne (IProp.foldi_unfoldi x).dist (IProp.foldi_validN _ H)
+
+end Fold
+
+section iSingleton
+
+open IProp OFE UPred
+
+def iSingleton {GF} F [RFunctorContractive F] [E : ElemG GF F] (γ : GName) (v : F.ap (IProp GF)) : IResUR GF :=
+  fun τ' => ⟨fun γ' => if H : (τ' = E.τ ∧ γ' = γ) then some (H.1 ▸ (unfoldi (E.Bundle v))) else none⟩
+
+variable {GF F} [RFunctorContractive F] [E : ElemG GF F]
+
+theorem IResUR_op_eval (c1 c2 : IResUR GF) : (c1 • c2) τ' γ' = (c1 τ' γ') • (c2 τ' γ') := by
+  simp [CMRA.op, optionOp]
+
+instance : OFE.NonExpansive (iSingleton F γ (GF := GF))  where
+  ne {n x1 x2} H τ' γ' := by
+    simp [iSingleton]
+    split <;> try rfl
+    rename_i h; rcases h with ⟨h1, h2⟩; subst h1; subst h2; simp
+    exact NonExpansive.ne (NonExpansive.ne H)
+
+theorem iSingleton_op  (x y : F.ap (IProp GF)) : (iSingleton F γ x) • iSingleton F γ y ≡ iSingleton F γ (x • y) := by
+  intro τ' γ'
+  simp [iSingleton, CMRA.op, optionOp]
+  by_cases H : (τ' = ElemG.τ GF F ∧ γ' = γ) <;> simp [H]
+  rcases H with ⟨h1, h2⟩; subst h1 h2; simp [unfoldi]
+  refine ((RFunctor.map (fold GF) (unfold GF)).op (E.Bundle x) (E.Bundle y)).symm.trans ?_
+  refine NonExpansive.eqv (.symm ?_)
+  exact transpAp_op_mp (E.TranspMap <| F.ap (IProp GF)).symm (E.TranspClass <| F.ap (IProp GF)).symm
+
+-- Helper lemmas for iSingleton validity and freedom properties
+
+-- iSingleton is free at all keys except γ
+theorem iSingleton_free_at_ne (γ : GName) (v : F.ap (IProp GF)) (γ' : GName) (h : γ' ≠ γ) :
+    (iSingleton F γ v E.τ).car γ' = none := by
+  simp [iSingleton, h]
+
+-- TODO: One use
+-- iSingleton at a single key has infinitely many free keys
+theorem iSingleton_infinite_free (γ : GName) (v : F.ap (IProp GF)) :
+    Infinite (IsFree (iSingleton F γ v E.τ).car) := by
+  refine ⟨Poke id γ, ?_, ?_⟩
+  · intro n
+    simp [IsFree, Poke]
+    split
+    · rename_i h; exact iSingleton_free_at_ne γ v n (Nat.ne_of_lt h)
+    · rename_i h; exact iSingleton_free_at_ne γ v (n + 1) (Nat.ne_of_gt (Nat.lt_succ_of_le (Nat.ge_of_not_lt h)))
+  · intro n m; simp [Poke]; split <;> split <;> omega
+
+-- TODO: One use
+-- iSingleton at τ' ≠ E.τ is the unit
+theorem iSingleton_ne_eq_unit  (γ : GName) (v : F.ap (IProp GF)) (τ' : GType) (h : τ' ≠ E.τ) :
+    (iSingleton F γ v τ').car = (UCMRA.unit : GenMap Nat _).car := by
+  ext γ'; simp [iSingleton, h]
+
+-- Composing with iSingleton preserves freedom at keys ≠ γ
+theorem iSingleton_op_ne_free  (γ : GName) (v : F.ap (IProp GF))
+    (m : GenMap GName (GF.api E.τ (IPre GF))) (γ' : GName) (h_ne : γ' ≠ γ) (h_free : m.car γ' = none) :
+    ((iSingleton F γ v E.τ) • m).car γ' = none := by
+  simp [CMRA.op, optionOp, iSingleton, h_ne, h_free]
+
+-- TODO: Single use
+-- Composing with iSingleton preserves infinite free keys
+theorem iSingleton_op_isFree_infinite (γ : GName) (v : F.ap (IProp GF))
+    (m : GenMap GName (GF.api E.τ (IPre GF))) (h_inf : Infinite (IsFree m.car)) :
+    Infinite (IsFree ((iSingleton F γ v E.τ) • m).car) := by
+  rcases h_inf with ⟨enum, h_enum_free, h_enum_inj⟩
+  by_cases h_gamma_in : ∃ n₀, enum n₀ = γ
+  · -- If γ appears in enum, use Poke to skip it
+    rcases h_gamma_in with ⟨n₀, h_n₀⟩
+    refine ⟨Poke enum n₀, ?_, ?_⟩
+    · intro n
+      simp [Poke]
+      apply iSingleton_op_ne_free
+      · split <;> intro H' <;> have _ := h_enum_inj (h_n₀ ▸ H') <;> omega
+      · split <;> apply h_enum_free
+    · intro n m h_eq; simp [Poke] at h_eq
+      split at h_eq <;> split at h_eq
+      all_goals have _ := h_enum_inj h_eq; omega
+  · -- If γ not in enum, all enumerated keys remain free
+    refine ⟨enum, ?_, h_enum_inj⟩
+    intro n; simp [IsFree]
+    apply iSingleton_op_ne_free
+    · intro heq; exact h_gamma_in ⟨n, heq⟩
+    · exact h_enum_free
+
+-- TODO: Single use
+-- Helper lemma: unfoldi ∘ E.Bundle preserves CoreId
+theorem unfoldi_Bundle_coreId {a : F.ap (IProp GF)} [CMRA.CoreId a] :
+    CMRA.CoreId (unfoldi (E.Bundle a)) := by
+  constructor
+  -- Strategy: Use that both Bundle and RFunctor.map preserve pcore
+  simp only [unfoldi, OFunctor.map]
+  letI : RFunctor (GF E.τ).fst := (GF E.τ).snd.toRFunctor
+  have bundle_coreId : CMRA.CoreId (E.Bundle a) := by
+    constructor
+    calc CMRA.pcore (E.Bundle a)
+      ≡ (CMRA.pcore a).map E.Bundle := by
+          apply OFE.Equiv.symm
+          apply OFE.transpAp_pcore_mp (E.TranspMap (F.ap (IProp GF))).symm (E.TranspClass (F.ap (IProp GF))).symm
+      _ ≡ (some a).map E.Bundle := by
+        have : CMRA.pcore a ≡ some a := CMRA.CoreId.core_id
+        rcases h : CMRA.pcore a with (_ | ca)
+        · rw [h] at this; simp [] at this
+        · rw [h] at this; simp [Option.map] at this ⊢
+          exact OFE.NonExpansive.eqv this
+      _ ≡ some (E.Bundle a) := by simp [Option.map, OFE.Equiv.rfl]
+  calc CMRA.pcore ((RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f (E.Bundle a))
+    ≡ (CMRA.pcore (E.Bundle a)).map (RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f :=
+      (RFunctor.map (IProp.fold GF) (IProp.unfold GF)).pcore (E.Bundle a) |>.symm
+    _ ≡ (some (E.Bundle a)).map (RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f := by
+      have : CMRA.pcore (E.Bundle a) ≡ some (E.Bundle a) := bundle_coreId.core_id
+      rcases h : CMRA.pcore (E.Bundle a) with (_ | c)
+      · rw [h] at this; simp [] at this
+      · rw [h] at this; simp [Option.map] at this ⊢
+        exact OFE.NonExpansive.eqv this
+    _ ≡ some ((RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f (E.Bundle a)) := by
+      simp [Option.map, OFE.Equiv.rfl]
+
+instance {a : F.ap (IProp GF)} [CMRA.CoreId a] : CMRA.CoreId (iSingleton F γ a) where
+  core_id τ' γ' := by
+    simp only [iSingleton, CMRA.core, CMRA.pcore, Option.getD, Option.map]
+    split
+    · rename_i h; cases h.1
+      exact unfoldi_Bundle_coreId.core_id
+    · rfl
+
+end iSingleton
+
+
+def iOwn {GF F} [RFunctorContractive F] [E : ElemG GF F] (γ : GName) (v : F.ap (IProp GF)) : IProp GF :=
+  UPred.ownM <| iSingleton F γ v
+
+section iOwn
+
+open IProp OFE UPred BI
+
+variable {GF F} [RFunctorContractive F] [E : ElemG GF F]
+
+instance iOwn_ne : NonExpansive (iOwn τ : F.ap (IProp GF) → IProp GF) where
+  ne {n x1 x2} H := by unfold iOwn; exact NonExpansive.ne (NonExpansive.ne H)
+
+theorem iOwn_op {a1 a2 : F.ap (IProp GF)} : iOwn γ (a1 • a2) ⊣⊢ iOwn γ a1 ∗ iOwn γ a2 :=
+  UPred.ownM_eqv (iSingleton_op _ _).symm |>.trans (UPred.ownM_op _ _)
+
+theorem iOwn_mono {a1 a2 : F.ap (IProp GF)} (H : a2 ≼ a1) : iOwn γ a1 ⊢ iOwn γ a2 := by
+  rcases H with ⟨ac, Hac⟩
+  rintro n x Hv ⟨clos, Hclos⟩
+  -- Basically the heaps proof, want some other lemmas
+  refine ⟨iSingleton F γ ac • clos, Hclos.trans <| fun τ' γ' => ?_⟩
+  refine .trans ?_ CMRA.op_assocN.symm
+  rw [IResUR_op_eval]
+  unfold iSingleton
+  simp
+  split
+  · rename_i h; rcases h with ⟨rfl, rfl⟩
+    refine Dist.op_l ?_
+    have h3 : E.Bundle a1 ≡{n}≡ E.Bundle a2 • E.Bundle ac := by
+      refine (NonExpansive.ne Hac.dist).trans ?_
+      exact transpAp_op_mp (E.TranspMap (F.ap (IProp GF))).symm (E.TranspClass (F.ap (IProp GF))).symm |>.dist
+    refine (NonExpansive.ne h3).trans ?_
+    exact (RFunctor.map (fold GF) (unfold GF)).op _ _ |>.dist
+  · simp [CMRA.op, optionOp]
+
+theorem iOwn_cmraValid {a : F.ap (IProp GF)} : iOwn γ a ⊢ UPred.cmraValid a := by
+  refine (UPred.ownM_valid _).trans ?_
+  refine UPred.valid_entails (fun n H => ?_)
+  rcases H E.τ with ⟨h_valid, _⟩
+  apply validN_transpAp_mp (E.TranspMap (F.ap (IProp GF))).symm (E.TranspClass (F.ap (IProp GF))).symm
+  apply validN_unfoldi
+  have h_at_γ := h_valid γ
+  simp [iSingleton] at h_at_γ; trivial
+
+theorem iOwn_cmraValid_op {a1 a2 : F.ap (IProp GF)} : iOwn γ a1 ∗ iOwn γ a2 ⊢ UPred.cmraValid (a1 • a2) :=
+  iOwn_op.mpr.trans iOwn_cmraValid
+
+theorem iOwn_valid_r {a : F.ap (IProp GF)} : iOwn γ a ⊢ iOwn γ a ∗ UPred.cmraValid a :=
+  BI.persistent_entails_l iOwn_cmraValid
+
+theorem iOwn_valid_l {a : F.ap (IProp GF)} : iOwn γ a ⊢ UPred.cmraValid a ∗ iOwn γ a :=
+  BI.persistent_entails_r iOwn_cmraValid
+
+instance {a : F.ap (IProp GF)} [CMRA.CoreId a] : BI.Persistent (iOwn γ a) where
+  persistent := by
+    simp [iOwn]
+    refine (UPred.persistently_ownM_core _).trans ?_
+    refine persistently_mono ?_
+    refine equiv_iff.mp ?_ |>.mp
+    refine NonExpansive.eqv ?_
+    apply CMRA.core_eqv_self
+
+/-
+theorem iOwn_alloc_strong_dep {f : GName → F.ap (IProp GF)} {P : GName → Prop}
+    (HI : Infinite P) (Hf_valid : ∀ γ, P γ → ✓ (f γ)) :
+    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ iOwn γ (f γ) := by
+  refine .trans (Q := iprop(|==> ∃ m : IResUR GF, ⌜∃ γ, P γ ∧ m = iSingleton _ γ (f γ)⌝ ∧ UPred.ownM m)) ?_ ?_
+-/
+
+theorem iOwn_alloc_dep (f : GName → F.ap (IProp GF)) (Ha : ∀ γ, ✓ (f γ)) :
+    ⊢ |==> ∃ γ, iOwn γ (f γ) := by
+  unfold iOwn
+  refine .trans (Q := iprop(|==> ∃ m : IResUR GF, ⌜∃ γ, m = iSingleton _ γ (f γ)⌝ ∧ UPred.ownM m)) ?_ ?_
+  · refine .trans (UPred.ownM_unit _) <| BI.intuitionistically_elim.trans ?_
+    refine UPred.bupd_ownM_updateP _ _ ?_
+    -- Prove: (UCMRA.unit : IResUR GF) ~~>: (fun m => ∃ γ, m = iSingleton F γ (f γ))
+    intro n mz Hv
+    -- Pick a fresh γ from the frame
+    -- Easy case: no frame
+    cases mz with
+    | none =>
+      -- Just pick γ = 0
+      let γ := 0
+      refine ⟨iSingleton F γ (f γ), ⟨γ, rfl⟩, ?_⟩
+      simp [CMRA.op?]
+      intro τ'
+      by_cases h_tau : τ' = E.τ
+      · subst h_tau
+        refine ⟨?_, iSingleton_infinite_free γ (f γ)⟩
+        intro γ'
+        unfold iSingleton
+        simp [CMRA.ValidN, optionValidN]
+        by_cases h_gamma : γ' = γ
+        · simp [h_gamma]
+          apply unfoldi_validN
+          apply transpAp_validN_mp (E.TranspMap <| F.ap (IProp GF)).symm (E.TranspClass <| F.ap (IProp GF)).symm
+          exact (Ha γ).validN
+        · simp [h_gamma]
+      · unfold iSingleton
+        simp [h_tau]
+        exact (UCMRA.unit_valid : ✓ (UCMRA.unit : GenMap Nat _)).validN
+    | some mz' =>
+      -- Pick a fresh γ from mz' E.τ
+      have h_valid_E := Hv E.τ
+      simp [CMRA.op?] at h_valid_E
+      rcases h_valid_E with ⟨h_pointwise, h_inf⟩
+      -- The frame at E.τ after composing with unit equals mz' at E.τ
+      have h_unit_op : (UCMRA.unit : IResUR GF) E.τ • mz' E.τ ≡ mz' E.τ := by
+        intro k
+        simp [CMRA.op, UCMRA.unit, optionOp]
+      -- Extract a free key using GenMap.valid_exists_fresh
+      have h_valid_mz : ✓{n} (mz' E.τ) := CMRA.validN_ne h_unit_op.dist ⟨h_pointwise, h_inf⟩
+      have ⟨γ, h_free_γ⟩ := @GenMap.valid_exists_fresh _ _ _ _ _ h_valid_mz
+      refine ⟨iSingleton F γ (f γ), ⟨γ, rfl⟩, ?_⟩
+      -- Show ✓{n} iSingleton F γ (f γ) •? some mz'
+      simp [CMRA.op?]
+      intro τ'
+      by_cases h_tau : τ' = E.τ
+      · subst h_tau
+        refine ⟨?_, ?_⟩
+        · -- Pointwise validity
+          intro γ'
+          simp [CMRA.op]
+          by_cases h_gamma : γ' = γ
+          · -- At the allocated key γ
+            subst h_gamma
+            unfold iSingleton at *
+            rw [h_free_γ]
+            simp [CMRA.ValidN, optionValidN]
+            apply unfoldi_validN
+            apply transpAp_validN_mp (E.TranspMap <| F.ap (IProp GF)).symm (E.TranspClass <| F.ap (IProp GF)).symm
+            exact (Ha γ').validN
+          · -- At other keys
+            unfold iSingleton
+            simp [h_gamma]
+            -- Validity from the frame
+            have := h_pointwise γ'
+            simp [CMRA.op, UCMRA.unit, optionOp] at this
+            exact this
+        · -- Infinite free keys
+          have h_inf_mz' : Infinite (IsFree (mz' E.τ).car) := by
+            apply Infinite.mono h_inf
+            intro k h_free
+            simp [IsFree, CMRA.op, UCMRA.unit, optionOp] at h_free ⊢
+            exact h_free
+          exact iSingleton_op_isFree_infinite γ (f γ) (mz' E.τ) h_inf_mz'
+      · -- τ' ≠ E.τ
+        have h_singleton_eq_unit : (iSingleton F γ (f γ) τ').car = (UCMRA.unit : GenMap Nat _).car := by
+          ext γ'
+          unfold iSingleton
+          simp [h_tau]
+        have h_frame_valid := Hv τ'
+        simp [CMRA.op?] at h_frame_valid
+        have h_eq : (iSingleton F γ (f γ) • mz') τ' ≡ (UCMRA.unit : IResUR GF) τ' • mz' τ' := by
+          intro k
+          simp [CMRA.op, h_singleton_eq_unit, UCMRA.unit]
+        exact CMRA.validN_ne h_eq.symm.dist h_frame_valid
+  · refine BIUpdate.mono ?_
+    refine BI.exists_elim (fun m => ?_)
+    refine BI.pure_elim (φ := ∃ γ, m = iSingleton F γ (f γ)) BI.and_elim_l ?_
+    refine fun ⟨γ, Hm⟩ => BI.and_elim_r' ?_
+    refine BI.exists_intro' γ ?_
+    rw [Hm]
+    exact .rfl
+
+theorem iOwn_alloc (a : F.ap (IProp GF)) : ✓ a → ⊢ |==> ∃ γ, iOwn γ a :=
+  fun Ha => iOwn_alloc_dep _ (fun _ => Ha)
+
+theorem iOwn_updateP {P γ a} (Hupd : a ~~>: P) : iOwn γ a ⊢ |==> ∃ a' : F.ap (IProp GF), ⌜P a'⌝ ∗ iOwn γ a' := by
+  refine .trans (Q := iprop(|==> ∃ m, ⌜ ∃ a', m = (iSingleton F γ a') ∧ P a' ⌝ ∧ UPred.ownM m)) ?_ ?_
+  · apply UPred.bupd_ownM_updateP
+    -- NB. The rest of this case is singleton_updateP
+    intro n mz Hv
+    cases mz with
+    | none =>
+      have h_a_valid : ✓{n} a := by
+        refine CMRA.validN_ne (ElemG.Unbundle_Bundle E a).dist ?_
+        refine transpAp_validN_mp (E.TranspMap <| F.ap (IProp GF)) (E.TranspClass <| F.ap (IProp GF)) ?_
+        refine CMRA.validN_ne (foldi_unfoldi (E.Bundle a)).dist ?_
+        refine foldi_validN (unfoldi (E.Bundle a)) ?_
+        have h_at_gamma : ✓{n} (((iSingleton F γ a) E.τ).car γ) := (Hv E.τ).1 γ
+        simp [iSingleton] at h_at_gamma
+        exact h_at_gamma
+      obtain ⟨a', Ha'_P, Ha'_valid⟩ := Hupd n none (by simp [CMRA.op?]; exact h_a_valid)
+      refine ⟨iSingleton F γ a', ⟨a', rfl, Ha'_P⟩, fun τ' => ?_⟩
+      simp [CMRA.op?]
+      by_cases h_tau : τ' = E.τ
+      · subst h_tau
+        refine ⟨fun γ' => ?_, ?_⟩
+        · simp [iSingleton]
+          by_cases h_gamma : γ' = γ <;> simp [h_gamma, CMRA.ValidN, optionValidN]
+          refine unfoldi_validN (E.Bundle a') ?_
+          apply transpAp_validN_mp (E.TranspMap <| F.ap (IProp GF)).symm (E.TranspClass <| F.ap (IProp GF)).symm
+          exact Ha'_valid
+        · refine ⟨Poke id γ, ?_, ?_⟩
+          · intro _; simp [IsFree, iSingleton, Poke]; split <;> omega
+          · intro _ _; simp [Poke]; split <;> split <;> omega
+      · simp [iSingleton, h_tau]
+        apply UCMRA.unit_valid.validN
+
+    | some mz' =>
+      -- With frame case
+      cases h_mz_gamma : (mz' E.τ).car γ with
+      | none =>
+        have h_a_valid : ✓{n} a := by
+          apply CMRA.validN_ne (ElemG.Unbundle_Bundle E a).dist
+          apply transpAp_validN_mp (E.TranspMap <| F.ap (IProp GF)) (E.TranspClass <| F.ap (IProp GF))
+          refine CMRA.validN_ne (foldi_unfoldi (E.Bundle a)).dist ?_
+          refine foldi_validN (unfoldi (E.Bundle a)) ?_
+          have h_at_gamma : ✓{n} ((((iSingleton F γ a) • mz') E.τ).car γ) := (Hv E.τ).1 γ
+          simp [iSingleton, CMRA.op, h_mz_gamma] at h_at_gamma
+          exact h_at_gamma
+        obtain ⟨a', Ha'_P, Ha'_valid⟩ := Hupd n none (by simp [CMRA.op?]; exact h_a_valid)
+        refine ⟨iSingleton F γ a', ⟨a', rfl, Ha'_P⟩, ?_⟩
+        simp [CMRA.op?]
+        intro τ'
+        by_cases h_tau : τ' = E.τ
+        · subst h_tau
+          refine ⟨?_, ?_⟩
+          · intro γ'
+            simp [CMRA.op]
+            by_cases h_gamma : γ' = γ
+            · simp [h_gamma, iSingleton, h_mz_gamma]
+              refine IProp.unfoldi_validN (E.Bundle a') ?_
+              apply OFE.transpAp_validN_mp (E.TranspMap <| F.ap (IProp GF)).symm (E.TranspClass <| F.ap (IProp GF)).symm
+              exact Ha'_valid
+            · simp [h_gamma, iSingleton]
+              have h := (Hv E.τ).1 γ'
+              simp [CMRA.op, iSingleton, h_gamma, optionOp, CMRA.op?] at h
+              exact h
+          · have h_frame_inf := Hv E.τ
+            simp [CMRA.op?] at h_frame_inf
+            rcases h_frame_inf with ⟨_, h_inf⟩
+            apply Infinite.mono h_inf (fun k h_free => ?_)
+            simp [IsFree, CMRA.op, iSingleton, optionOp] at h_free ⊢
+            by_cases h_k : k = γ <;> simp_all []
+        · have h_frame_valid := Hv τ'
+          simp [CMRA.op?, CMRA.op, iSingleton, h_tau] at h_frame_valid ⊢
+          exact h_frame_valid
+      | some v =>
+        have h_a_valid : ✓{n} (a • E.Unbundle (IProp.foldi v)) := by
+          have h_valid_at_tau : ✓{n} ((iSingleton F γ a •? some mz') E.τ) := Hv E.τ
+          simp [CMRA.op?] at h_valid_at_tau
+          rcases h_valid_at_tau with ⟨h_pointwise, _⟩
+          have h_at_gamma : ✓{n} ((((iSingleton F γ a) • mz') E.τ).car γ) := h_pointwise γ
+          simp [iSingleton, CMRA.op, h_mz_gamma]  at h_at_gamma
+          have h_foldi_hom := (RFunctor.map (IProp.unfold GF) (IProp.fold GF)).op
+              ((RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f (E.Bundle a)) v
+          have h_comp : (RFunctor.map (IProp.unfold GF) (IProp.fold GF)).toHom.f
+              ((RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f (E.Bundle a)) ≡ E.Bundle a := by
+            refine .trans (OFunctor.map_comp (F := GF E.τ |>.fst) ..).symm ?_
+            refine .trans ?_ (OFunctor.map_id (F := GF E.τ |>.fst) (E.Bundle a))
+            apply OFunctor.map_ne.eqv <;> intro _ <;> simp [IProp.unfold, IProp.fold]
+          apply CMRA.validN_ne (ElemG.Unbundle_Bundle E a).op_l.dist
+          apply CMRA.validN_ne (OFE.transpAp_op_mp (E.TranspMap ((GF (ElemG.τ GF F)).fst.ap (IPre GF))) (E.TranspClass ((GF (ElemG.τ GF F)).fst.ap (IPre GF)))).dist
+          apply OFE.transpAp_validN_mp (E.TranspMap (F.ap (IProp GF))) (E.TranspClass (F.ap (IProp GF)))
+          apply CMRA.validN_ne (h_comp.op_l).dist
+          apply CMRA.validN_ne h_foldi_hom.dist
+          apply IProp.foldi_validN _ h_at_gamma
+        obtain ⟨a', Ha'_P, Ha'_valid⟩ := Hupd n (some (E.Unbundle (IProp.foldi v))) (by simp [CMRA.op?]; exact h_a_valid)
+        refine ⟨iSingleton F γ a', ⟨a', rfl, Ha'_P⟩, ?_⟩
+        simp [CMRA.op?]
+        intro τ'
+        by_cases h_tau : τ' = E.τ
+        · subst h_tau
+          refine ⟨?_, ?_⟩
+          · intro γ'
+            simp [CMRA.op]
+            by_cases h_gamma : γ' = γ
+            · simp [h_gamma, iSingleton, h_mz_gamma, CMRA.ValidN, optionValidN]
+              simp [CMRA.op?] at Ha'_valid
+              have h_bundle_foldi_v : ✓{n} (E.Bundle a' • foldi v) := by
+                apply CMRA.validN_ne (ElemG.Bundle_Unbundle E (foldi v)).op_r.dist
+                apply CMRA.validN_ne (OFE.transpAp_op_mp (E.TranspMap (F.ap (IProp GF))).symm (E.TranspClass (F.ap (IProp GF))).symm |>.dist)
+                apply OFE.transpAp_validN_mp (E.TranspMap (F.ap (IProp GF))).symm (E.TranspClass (F.ap (IProp GF))).symm
+                apply Ha'_valid
+              simp [IProp.unfoldi, IProp.foldi] at h_bundle_foldi_v ⊢
+              have h_unfoldi_op := (RFunctor.map (IProp.fold GF) (IProp.unfold GF)).op (E.Bundle a') ((RFunctor.map (IProp.unfold GF) (IProp.fold GF)).toHom.f v)
+              have h_after_unfoldi : ✓{n} ((RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f (E.Bundle a') •
+                  (RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f ((RFunctor.map (IProp.unfold GF) (IProp.fold GF)).toHom.f v)) := by
+                apply CMRA.validN_ne h_unfoldi_op.dist
+                exact IProp.unfoldi_validN _ h_bundle_foldi_v
+              have h_unfoldi_foldi := IProp.unfoldi_foldi v
+              apply CMRA.validN_ne (h_unfoldi_foldi.op_r).dist
+              exact h_after_unfoldi
+            · simp [h_gamma, iSingleton]
+              have h_frame_valid := Hv E.τ
+              simp [CMRA.op?] at h_frame_valid
+              rcases h_frame_valid with ⟨h_pointwise, _⟩
+              have h_at_gamma' := h_pointwise γ'
+              simp [CMRA.op, iSingleton, h_gamma, optionOp] at h_at_gamma'
+              exact h_at_gamma'
+          · have h_frame_inf := Hv E.τ
+            simp [CMRA.op?] at h_frame_inf
+            rcases h_frame_inf with ⟨_, h_inf⟩
+            apply Infinite.mono h_inf
+            intro k h_free
+            simp [IsFree, CMRA.op, iSingleton, optionOp] at h_free ⊢
+            by_cases h_k : k = γ <;> simp_all
+        · have h_frame_valid := Hv τ'
+          simp [CMRA.op?, CMRA.op, iSingleton, h_tau] at h_frame_valid ⊢
+          exact h_frame_valid
+  · refine BIUpdate.mono (BI.exists_elim (fun m => BI.pure_elim_l (fun ⟨a', Hm, HP⟩ => ?_)))
+    subst Hm
+    exact BI.exists_intro' a' (BI.persistent_entails_r (BI.pure_intro HP))
+
+theorem iOwn_update {γ} {a a' : F.ap (IProp GF)} (Hupd : a ~~> a') : iOwn γ a ⊢ |==> iOwn γ a' := by
+  refine .trans (iOwn_updateP <| UpdateP.of_update Hupd) ?_
+  refine BIUpdate.mono ?_
+  refine BI.exists_elim (fun m => ?_)
+  refine BI.pure_elim (a' = m) BI.sep_elim_l ?_
+  rintro rfl
+  exact BI.sep_elim_r
+
+-- Helper lemmas for iOwn_unit
+
+-- Bundle preserves unit structure
+theorem ElemG.Bundle_unit {GF F} [RFunctorContractive F] (E : ElemG GF F)
+    {ε : F.ap (IProp GF)} [IsUnit ε] :
+    IsUnit (E.Bundle ε) := by
+  refine { unit_valid := ?_, unit_left_id := ?_, pcore_unit := ?_ }
+  · -- Validity: use Bundle_validN
+    refine CMRA.valid_iff_validN.mpr fun n => ?_
+    apply transpAp_validN_mp (E.TranspMap <| F.ap (IProp GF)).symm (E.TranspClass <| F.ap (IProp GF)).symm
+    apply IsUnit.unit_valid.validN
+  · -- Left identity: Strategy: apply Unbundle to both sides, use that ε is unit, then Bundle back
+    intro x
+    have h1 : E.Unbundle (E.Bundle ε • x) ≡ E.Unbundle x := by
+      calc E.Unbundle (E.Bundle ε • x)
+        _ ≡ E.Unbundle (E.Bundle ε) • E.Unbundle x := by
+          apply transpAp_op_mp (E.TranspMap <| F.ap (IProp GF)) (E.TranspClass <| F.ap (IProp GF))
+        _ ≡ ε • E.Unbundle x := (ElemG.Unbundle_Bundle E ε).op_l
+        _ ≡ E.Unbundle x := IsUnit.unit_left_id
+    calc E.Bundle ε • x
+      ≡ E.Bundle (E.Unbundle (E.Bundle ε • x)) := (ElemG.Bundle_Unbundle E _).symm
+      _ ≡ E.Bundle (E.Unbundle x) := OFE.NonExpansive.eqv h1
+      _ ≡ x := ElemG.Bundle_Unbundle E x
+  · -- Pcore
+    calc CMRA.pcore (E.Bundle ε)
+      ≡ (CMRA.pcore ε).map E.Bundle := by
+            symm
+            apply transpAp_pcore_mp (E.TranspMap <| F.ap (IProp GF)).symm (E.TranspClass <| F.ap (IProp GF)).symm
+      _ ≡ Option.map E.Bundle (some ε) := by
+         rename_i unit
+         have := unit.pcore_unit
+         rcases eqn: CMRA.pcore ε
+         · rw [eqn] at this; simp [] at this
+         · rw [eqn] at this; simp [Option.map] at this ⊢
+           exact NonExpansive.eqv this
+      _ ≡ E.Bundle ε := by rfl
+
+-- unfoldi preserves unit structure
+theorem IProp.unfoldi_unit {τ : GType} {x : GF.api τ (IProp GF)} [IsUnit x] :
+IsUnit (unfoldi x) := by
+  refine { unit_valid := ?_, unit_left_id := ?_, pcore_unit := ?_ }
+  · -- Validity
+    refine CMRA.valid_iff_validN.mpr fun n => IProp.unfoldi_validN x IsUnit.unit_valid.validN
+  · -- Left identity: unfoldi x • y ≡ y
+    intro y
+    have h : foldi (unfoldi x • y) ≡ foldi y := by
+      calc foldi (unfoldi x • y)
+        _ ≡ foldi (unfoldi x) • foldi y := foldi_op _ _
+        _ ≡ x • foldi y := (foldi_unfoldi x).op_l
+        _ ≡ foldi y := IsUnit.unit_left_id
+    calc unfoldi x • y
+      _ ≡ unfoldi (foldi (unfoldi x • y)) := (IProp.unfoldi_foldi _).symm
+      _ ≡ unfoldi (foldi y) := OFE.NonExpansive.eqv h
+      _ ≡ y := IProp.unfoldi_foldi y
+  · -- pcore_unit
+    simp only [unfoldi, OFunctor.map]
+    letI : RFunctor (GF τ).fst := (GF τ).snd.toRFunctor
+    calc CMRA.pcore ((RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f x)
+      _ ≡ (CMRA.pcore x).map (RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f :=
+        (RFunctor.map (IProp.fold GF) (IProp.unfold GF)).pcore x |>.symm
+      _ ≡ (some x).map (RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f :=
+        Option.map_forall₂ _ IsUnit.pcore_unit
+      _ ≡ some ((RFunctor.map (IProp.fold GF) (IProp.unfold GF)).toHom.f x) := by
+        simp [Option.map, OFE.Equiv.rfl]
+
+theorem unit_op_eq {GF : BundledGFunctors} (τ : GType) (m : GenMap GName (GF.api τ (IPre GF))) :
+    ((UCMRA.unit : IResUR GF) τ) • m ≡ m := by
+  simp [OFE.Equiv, CMRA.op, UCMRA.unit, optionOp, Option.Forall₂]
+  intro k; cases m.car k <;> simp [OFE.Equiv.rfl]
+
+theorem unfoldi_bundle_unit {GF F} [RFunctorContractive F] (E : ElemG GF F)
+    {ε : F.ap (IProp GF)} [IsUnit ε] : IsUnit (IProp.unfoldi (E.Bundle ε)) :=
+  haveI : IsUnit (E.Bundle ε) := ElemG.Bundle_unit E
+  IProp.unfoldi_unit
+
+-- Helper: validity of unfoldi (Bundle ε) at level n
+theorem unfoldi_bundle_validN {GF F} [RFunctorContractive F] (E : ElemG GF F)
+    {ε : F.ap (IProp GF)} [IsUnit ε] (n : Nat) : ✓{n} (IProp.unfoldi (E.Bundle ε)) := by
+  simp [IProp.unfoldi]
+  refine (RFunctor.map (IProp.fold GF) (IProp.unfold GF)).validN ?_
+  apply OFE.transpAp_validN_mp (E.TranspMap <| F.ap (IProp GF)).symm (E.TranspClass <| F.ap (IProp GF)).symm
+  apply IsUnit.unit_valid.validN
+
+-- Helper: extract validity of element at key from unit-composed frame
+theorem extract_frame_validN {GF : BundledGFunctors} (τ : GType) (n : Nat)
+    (mz' : IResUR GF)
+    (h_valid : ✓{n} ((UCMRA.unit : IResUR GF) τ • mz' τ).car)
+    (γ : GName) (v : GF.api τ (IPre GF)) (h_at : (mz' τ).car γ = some v) :
+    ✓{n} v := by
+  have := h_valid γ
+  simp [CMRA.op, UCMRA.unit, optionOp, CMRA.ValidN, optionValidN, h_at] at this
+  exact this
+
+theorem iOwn_unit {γ} {ε : F.ap (IProp GF)} [Hε : IsUnit ε] : ⊢ |==> iOwn γ ε := by
+  unfold iOwn
+  refine .trans (UPred.ownM_unit _) ?_
+  refine BI.intuitionistically_elim.trans ?_
+  have Hupd : (UCMRA.unit : IResUR GF) ~~>: (iSingleton F γ ε = ·) := by
+    intro n mz Hv
+    refine ⟨iSingleton F γ ε, rfl, ?_⟩
+    -- Show ✓{n} (iSingleton F γ ε •? mz)
+    intro τ'
+    by_cases Heq : τ' = E.τ
+    · 
+      subst Heq
+      refine ⟨?_, ?_⟩
+      · 
+        intro γ'
+        unfold iSingleton
+        simp [CMRA.op?, CMRA.ValidN, optionValidN]
+        cases mz with
+        | none =>
+          simp []
+          by_cases h_key : γ' = γ
+          · simp [h_key]; exact unfoldi_bundle_validN E n
+          · simp [h_key]
+        | some mz' =>
+          simp [CMRA.op, optionOp]
+          have Hv' := Hv E.τ
+          simp [CMRA.op?] at Hv'
+          rcases Hv' with ⟨h_valid, _⟩
+          by_cases h_key : γ' = γ
+          · 
+            simp [h_key]
+            rcases h_at : (mz' E.τ).car γ with (⟨⟩ | v)
+            · simp []; exact unfoldi_bundle_validN E n
+            · simp []
+              haveI h_unit : IsUnit (IProp.unfoldi (E.Bundle ε)) := unfoldi_bundle_unit E
+              have h_v_valid := extract_frame_validN E.τ n mz' h_valid γ v h_at
+              exact CMRA.validN_ne h_unit.unit_left_id.dist.symm h_v_valid
+          · 
+            simp [h_key]
+            rcases h_at : (mz' E.τ).car γ' with (⟨⟩ | v)
+            · trivial
+            · simp []; exact extract_frame_validN E.τ n mz' h_valid γ' v h_at
+      · cases mz with
+        | none => exact iSingleton_infinite_free γ ε
+        | some mz' =>
+          have ⟨_, h_inf⟩ := Hv E.τ; simp [CMRA.op?] at h_inf
+          have h_inf_mz : Infinite (IsFree (mz' E.τ).car) := by
+            apply Infinite.mono h_inf
+            intro k h_free; simp [IsFree, CMRA.op, UCMRA.unit, optionOp] at h_free ⊢; exact h_free
+          exact iSingleton_op_isFree_infinite γ ε (mz' E.τ) h_inf_mz
+    · 
+      have h_is_unit := iSingleton_ne_eq_unit γ ε τ' Heq
+      cases mz with
+      | none =>
+        simp [CMRA.op?]
+        show ✓{n} (⟨fun γ' => if _ : τ' = E.τ ∧ γ' = γ then _ else none⟩ : GenMap Nat _)
+        simp [Heq]
+        exact (UCMRA.unit_valid : ✓ (UCMRA.unit : GenMap Nat ((GF τ').fst (IPre GF) (IPre GF)))).validN
+      | some mz' =>
+        have Hv' := Hv τ'; simp [CMRA.op?] at Hv'
+        have h_eq : ((UCMRA.unit : IResUR GF) • mz') τ' ≡ (iSingleton F γ ε •? some mz') τ' := by
+          simp only [CMRA.op?, CMRA.op, h_is_unit, OFE.Equiv]
+          intro k
+          simp [UCMRA.unit, optionOp, Option.Forall₂]
+          cases (mz' τ').car k <;> simp [OFE.Equiv.rfl]
+        exact CMRA.validN_ne h_eq.dist Hv'
+
+  refine .trans (UPred.bupd_ownM_updateP _ _ Hupd) ?_
+  refine BIUpdate.mono ?_
+  refine BI.exists_elim (fun y => ?_)
+  refine BI.pure_elim (iSingleton F γ ε = y) BI.and_elim_l ?_
+  rintro rfl
+  exact BI.and_elim_r
+
+
+
+/-
+(** ** Allocation *)
+(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
+   assertion. However, the map_updateP_alloc does not suffice to show this. *)
+Lemma own_alloc_strong_dep (f : gname → A) (P : gname → Prop) :
+  pred_infinite P →
+  (∀ γ, P γ → ✓ (f γ)) →
+  ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ own γ (f γ).
+Proof.
+  intros HPinf Hf.
+  rewrite -(bupd_mono (∃ m, ⌜∃ γ, P γ ∧ m = iRes_singleton γ (f γ)⌝ ∧ uPred_ownM m)%I).
+  - rewrite /bi_emp_valid (ownM_unit emp).
+    apply bupd_ownM_updateP, (discrete_fun_singleton_updateP_empty _ (λ m, ∃ γ,
+      m = {[ γ := inG_unfold (cmra_transport inG_prf (f γ)) ]} ∧ P γ));
+      [|naive_solver].
+    apply (alloc_updateP_strong_dep _ P _ (λ γ,
+      inG_unfold (cmra_transport inG_prf (f γ)))); [done| |naive_solver].
+    intros γ _ ?.
+    by apply (cmra_morphism_valid inG_unfold), cmra_transport_valid, Hf.
+  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
+    by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
+Qed.
+Lemma own_alloc_cofinite_dep (f : gname → A) (G : gset gname) :
+  (∀ γ, γ ∉ G → ✓ (f γ)) → ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ own γ (f γ).
+Proof.
+  intros Ha.
+  apply (own_alloc_strong_dep f (λ γ, γ ∉ G))=> //.
+  apply (pred_infinite_set (C:=gset gname)).
+  intros E. set (γ := fresh (G ∪ E)).
+  exists γ. apply not_elem_of_union, is_fresh.
+Qed.
+Lemma own_alloc_dep (f : gname → A) :
+  (∀ γ, ✓ (f γ)) → ⊢ |==> ∃ γ, own γ (f γ).
+Proof.
+  intros Ha. rewrite /bi_emp_valid (own_alloc_cofinite_dep f ∅) //; [].
+  apply bupd_mono, exist_mono=>?. apply: sep_elim_r.
+Qed.
+
+Lemma own_alloc_strong a (P : gname → Prop) :
+  pred_infinite P →
+  ✓ a → ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ own γ a.
+Proof. intros HP Ha. eapply (own_alloc_strong_dep (λ _, a)); eauto. Qed.
+Lemma own_alloc_cofinite a (G : gset gname) :
+  ✓ a → ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ own γ a.
+Proof. intros Ha. eapply (own_alloc_cofinite_dep (λ _, a)); eauto. Qed.
+Lemma own_alloc a : ✓ a → ⊢ |==> ∃ γ, own γ a.
+Proof. intros Ha. eapply (own_alloc_dep (λ _, a)); eauto. Qed.
+-/
+
+
+
+end iOwn
+end Iris
diff --git a/src/Iris/Instances/UPred/Instance.lean b/src/Iris/Instances/UPred/Instance.lean
index 3ee48c68..c4b30ac5 100644
--- a/src/Iris/Instances/UPred/Instance.lean
+++ b/src/Iris/Instances/UPred/Instance.lean
@@ -423,6 +423,9 @@ theorem ownM_op (m1 m2 : M) : ownM (m1 • m2) ⊣⊢ ownM m1 ∗ ownM m2 := by
       _ ≡{n}≡ (m1 • m2) • (w2 • w1) := CMRA.assoc.dist
       _ ≡{n}≡ (m1 • m2) • (w1 • w2) := CMRA.comm.op_r.dist
 
+theorem ownM_eqv {m1 m2 : M} (H : m1 ≡ m2) : ownM m1 ⊣⊢ ownM m2 :=
+  ⟨fun _ _ _ => (CMRA.incN_iff_left H.dist).mp, fun _ _ _ => (CMRA.incN_iff_left H.dist).mpr⟩
+
 theorem ownM_always_invalid_elim (m : M) (H : ∀ n, ¬✓{n} m) : (cmraValid m : UPred M) ⊢ False :=
   fun n _ _ => H n
 
@@ -456,6 +459,14 @@ theorem later_soundness : iprop(True ⊢ ▷ P) → iprop((True : UPred M) ⊢ P
 theorem persistently_ownM_core (a : M) : ownM a ⊢ <pers> ownM (CMRA.core a) :=
   fun _ _ _ H => CMRA.core_incN_core H
 
+instance : Persistent (ownM (CMRA.core a) : UPred M) where
+  persistent := by
+    refine .trans (persistently_ownM_core _) ?_
+    refine persistently_mono ?_
+    refine equiv_iff.mp ?_ |>.mp
+    refine OFE.NonExpansive.eqv ?_
+    exact CMRA.core_idem a
+
 theorem bupd_ownM_updateP (x : M) (Φ : M → Prop) :
   (x ~~>: Φ) → ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ ownM y := by
   intro Hup n x2 Hv ⟨x3, Hx⟩ k yf Hk Hyf
@@ -488,6 +499,9 @@ theorem cmraValid_entails [CMRA A] [CMRA B] {a : A} {b : B} (Hv : ∀ n, ✓{n}
     (cmraValid a : UPred M) ⊢ cmraValid b :=
   fun _ _ _ H => Hv _ H
 
+instance [CMRA A] {a : A} : Persistent (UPred.cmraValid a : UPred M) where
+  persistent := fun _ _ _ a => a
+
 instance : BIAffine (UPred M) := ⟨by infer_instance⟩
 
 -- TODO: Port derived lemmas