diff --git a/src/Iris/Algebra/CMRA.lean b/src/Iris/Algebra/CMRA.lean
index 6d7070b7..f590de43 100644
--- a/src/Iris/Algebra/CMRA.lean
+++ b/src/Iris/Algebra/CMRA.lean
@@ -169,9 +169,20 @@ theorem _root_.Iris.OFE.Equiv.opM {x₁ x₂ : α} {y₁ y₂ : Option α}
     (H1 : x₁ ≡ x₂) (H2 : y₁ ≡ y₂) : x₁ •? y₁ ≡ x₂ •? y₂ :=
   equiv_dist.2 fun _ => H1.dist.opM H2.dist
 
+theorem opM_left_eqv {x y : α} (z : Option α) (e : x ≡ y) : x •? z ≡ y •? z := e.opM Equiv.rfl
+theorem opM_right_eqv (x : α) {y z : Option α} (e : y ≡ z) : x •? y ≡ x •? z := Equiv.rfl.opM e
+
+theorem opM_left_dist {n} {x y : α} (z : Option α) (e : x ≡{n}≡ y) : x •? z ≡{n}≡ y •? z :=
+  e.opM Dist.rfl
+theorem opM_right_dist {n} (x : α) {y z : Option α} (e : y ≡{n}≡ z) : x •? y ≡{n}≡ x •? z :=
+  Dist.rfl.opM e
+
 theorem op_opM_assoc (x y : α) (mz : Option α) : (x • y) •? mz ≡ x • (y •? mz) := by
   unfold op?; cases mz <;> simp [assoc, Equiv.symm]
 
+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 · _)
@@ -194,6 +205,8 @@ theorem _root_.Iris.OFE.Equiv.valid : (x : α) ≡ y → (✓ x ↔ ✓ y) := va
 theorem validN_of_le {n n'} {x : α} : n' ≤ n → ✓{n} x → ✓{n'} x :=
   fun le => le.recOn id fun  _ ih vs => ih (validN_succ vs)
 
+theorem valid0_of_validN {n} {x : α} : ✓{n} x → ✓{0} x := validN_of_le (Nat.zero_le n)
+
 theorem validN_op_right {n} {x y : α} : ✓{n} (x • y) → ✓{n} y :=
   fun v => validN_op_left (validN_of_eqv comm v)
 
@@ -203,6 +216,27 @@ theorem valid_op_right (x y : α) : ✓ (x • y) → ✓ y :=
 theorem valid_op_left {x y : α} : ✓ (x • y) → ✓ x :=
   fun v => valid_op_right y x (valid_of_eqv comm v)
 
+theorem validN_opM {x: α}{my: Option α}: ✓{n} (x •? my) → ✓{n} x :=
+  match my with
+  | none => id  | some _ => validN_op_left
+
+theorem valid_opM {x: α}{my: Option α}: ✓ (x •? my) → ✓ x :=
+  match my with
+  | none => id  | some _ => valid_op_left
+
+theorem validN_op_opM_left {n} {x y: α} {mz: Option α} : ✓{n} (x • y) •? mz → ✓{n} x •? mz :=
+  match mz with
+  | .none => validN_op_left
+  | .some z => fun h =>
+    have := calc
+      (x • y) • z ≡{n}≡ x • (y • z) := op_assocN.symm
+      _           ≡{n}≡ x • (z • y) := op_right_dist x op_commN
+      _           ≡{n}≡ (x • z) • y := op_assocN
+    validN_op_left ((Dist.validN this).mp h)
+
+theorem validN_op_opM_right {n} {x y: α} {mz: Option α} : ✓{n} (x • y) •? mz → ✓{n} y •? mz :=
+  fun h => validN_op_opM_left (validN_ne (opM_left_dist mz op_commN) h)
+
 /-! ## Core -/
 
 theorem pcore_proper {x y : α} (cx : α) (e : x ≡ y) (ps : pcore x = some cx)
@@ -377,6 +411,7 @@ theorem Included.validN {n} {x y : α} : x ≼ y → ✓{n} y → ✓{n} x := va
 
 theorem incN_of_incN_le {n n'} {x y : α} (l1 : n' ≤ n) : x ≼{n} y → x ≼{n'} y
   | ⟨z, hz⟩ => ⟨z, Dist.le hz l1⟩
+theorem inc0_of_incN {n} {x y : α} : x ≼{n} y → x ≼{0} y := incN_of_incN_le (Nat.zero_le n)
 theorem IncludedN.le {n n'} {x y : α} : n' ≤ n → x ≼{n} y → x ≼{n'} y := incN_of_incN_le
 
 theorem incN_of_incN_succ {n} {x y : α} : x ≼{n.succ} y → x ≼{n} y :=
@@ -470,6 +505,9 @@ theorem pcore_eq_core (x : α) : pcore x = some (core x) := by
 theorem op_core (x : α) : x • core x ≡ x := pcore_op_right (pcore_eq_core x)
 theorem core_op (x : α) : core x • x ≡ x := comm.trans (op_core x)
 
+theorem op_core_dist {n}(x: α) : x • core x ≡{n}≡ x := (op_core x).dist
+theorem core_op_dist {n}(x: α) : core x • x ≡{n}≡ x := (core_op x).dist
+
 theorem core_op_core {x : α} : core x • core x ≡ core x :=
   pcore_op_self (pcore_eq_core x)
 theorem validN_core {n} {x : α} (v : ✓{n} x) : ✓{n} core x := pcore_validN (pcore_eq_core x) v
@@ -591,6 +629,12 @@ theorem cancelable_iff {x₁ x₂ : α} (e : x₁ ≡ x₂) : Cancelable x₁ 
 theorem _root_.Iris.OFE.Equiv.cancelable {x₁ x₂ : α} : x₁ ≡ x₂ → (Cancelable x₁ ↔ Cancelable x₂) :=
   cancelable_iff
 
+theorem op_opM_cancel_dist {x y z: α} [Cancelable x]
+    (vxy: ✓{n} x • y) (h: x • y ≡{n}≡ (x • z) •? mw): y ≡{n}≡ z •? mw :=
+  match mw with
+  | none => cancelableN vxy h
+  | some _ => cancelableN vxy (h.trans (op_assocN.symm))
+
 end cancelableElements
 
 section idFreeElements
@@ -664,8 +708,12 @@ theorem incN_unit {n} {x : α} : unit ≼{n} x := ⟨x, unit_left_id.symm.dist
 
 theorem inc_unit {x : α} : unit ≼ x := ⟨x, unit_left_id.symm⟩
 
+theorem unit_left_id_dist {n} (x : α) : unit • x ≡{n}≡ x := unit_left_id.dist
+
 theorem unit_right_id {x : α} : x • unit ≡ x := comm.trans unit_left_id
 
+theorem unit_right_id_dist (x : α) : x • unit ≡{n}≡ x := comm.dist.trans (unit_left_id_dist x)
+
 instance unit_CoreId : CoreId (unit : α) where
   core_id := pcore_unit
 
@@ -958,25 +1006,25 @@ end DiscreteFunURF
 
 section option
 
-variable [CMRA A]
+variable [CMRA α]
 
-def optionCore (x : Option A) : Option A := x.bind CMRA.pcore
+def optionCore (x : Option α) : Option α := x.bind CMRA.pcore
 
-def optionOp (x y : Option A) : Option A :=
+def optionOp (x y : Option α) : Option α :=
   match x, y with
   | some x', some y' => some (CMRA.op x' y')
   | none, _ => y
   | _, none => x
 
-def optionValidN (n : Nat) : Option A → Prop
+def optionValidN (n : Nat) : Option α → Prop
   | some x => ✓{n} x
   | none => True
 
-def optionValid : Option A → Prop
+def optionValid : Option α → Prop
   | some x => ✓ x
   | none => True
 
-instance cmraOption : CMRA (Option A) where
+instance cmraOption : CMRA (Option α) where
   pcore x := some (optionCore x)
   op := optionOp
   ValidN := optionValidN
@@ -1037,14 +1085,168 @@ instance cmraOption : CMRA (Option A) where
     · rcases CMRA.extend Hx Hx' with ⟨mc1, mc2, _, _, _⟩
       exists some mc1, some mc2
 
-instance ucmraOption : UCMRA (Option A) where
+instance ucmraOption : UCMRA (Option α) where
   unit := none
   unit_valid := by simp [CMRA.Valid, optionValid]
   unit_left_id := by rintro ⟨⟩ <;> rfl
   pcore_unit := by rfl
 
+theorem CMRA.equiv_of_some_equiv_some {x y : α} (h: some x ≡ some y): x ≡ y := h
+theorem CMRA.dist_of_some_dist_some {n} {x y : α} (h: some x ≡{n}≡ some y): x ≡{n}≡ y := h
+
+theorem CMRA.op_some_opM_assoc (x y : α) (mz : Option α) : (x • y) •? mz ≡ x •? (some y • mz) :=
+  match mz with
+  | none   => Equiv.rfl
+  | some _ => Equiv.symm assoc
+
+theorem CMRA.op_some_opM_assoc_dist (x y : α) (mz : Option α) : (x • y) •? mz ≡{n}≡ x •? (some y • mz) :=
+  match mz with
+  | none   => Dist.rfl
+  | some _ => Dist.symm assoc.dist
+
+theorem CMRA.some_inc_some_of_dist_opM {x y : α} {mz : Option α} (h: x ≡{n}≡ y •? mz)
+    : some y ≼{n} some x :=
+  match mz with
+  | none   => ⟨none, h⟩
+  | some z => ⟨some z, h⟩
+
+theorem CMRA.inc_of_some_inc_some [CMRA.IsTotal α] {x y : α} (h: some y ≼ some x): y ≼ x :=
+  let ⟨mz, hmz⟩ := h
+  match mz with
+  | 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 : α} (h: some y ≼{n} some x): y ≼{n} x :=
+  let ⟨mz, hmz⟩ := h
+  match mz with
+  | none => ⟨core y, (CMRA.dist_of_some_dist_some hmz).trans (op_core_dist y).symm⟩
+  | some z => ⟨z, hmz⟩
+
+theorem CMRA.exists_op_some_eqv_some (x : Option α) (y : α): ∃z, x • some y ≡ some z :=
+  match x with
+  | .none => ⟨y, Equiv.rfl⟩
+  | .some w => ⟨w • y, Equiv.rfl⟩
+
+theorem CMRA.exists_op_some_dist_some {n} (x : Option α) (y : α): ∃z, x • some y ≡{n}≡ some z :=
+  (CMRA.exists_op_some_eqv_some x y).elim fun z h => ⟨z, h.dist⟩
+
+theorem not_valid_some_exclN_op_left {n} {x : α} [CMRA.Exclusive x] {y: α}
+    : ¬✓{n} (some x • some y) :=
+  fun h =>
+    have : ✓{n} x • y := h
+    absurd this (by exact CMRA.not_valid_exclN_op_left)
+
+theorem validN_op_unit {n} {x : Option α} (vx: ✓{n} x): ✓{n} x • CMRA.unit :=
+  match x with
+  | .none => vx
+  | .some _ => vx
+
 end option
 
+section unit
+
+instance cmraUnit : CMRA Unit where
+  pcore _ := some ()
+  op _ _ := ()
+  ValidN _ _ := True
+  Valid _ := True
+  op_ne.ne _ _ _ H := H
+  pcore_ne {_} _ _ z _ _ := match z with | .unit => ⟨(), rfl, OFE.Dist.rfl⟩
+  validN_ne {_} _ _ _ := id
+  valid_iff_validN := ⟨fun _ _ => .intro, fun _ => .intro⟩
+  validN_succ := id
+  validN_op_left := id
+  assoc := OFE.Equiv.rfl
+  comm := OFE.Equiv.rfl
+  pcore_op_left {x _} _ := match x with | .unit => OFE.Equiv.rfl
+  pcore_idem {_ cx} _ := match cx with | .unit => OFE.Equiv.rfl
+  pcore_op_mono _ _ := ⟨.unit, OFE.Equiv.rfl⟩
+  extend {_} x y z _ _ :=
+    match x, y, z with
+    | .unit, .unit, .unit => ⟨(), (), OFE.Equiv.rfl, OFE.Dist.rfl, OFE.Dist.rfl⟩
+
+end unit
+
+namespace Prod
+
+variable {α β : Type _} [CMRA α] [CMRA β]
+
+abbrev pcore (x : α × β) : Option (α × β) :=
+  (CMRA.pcore x.fst).bind fun a =>
+  (CMRA.pcore x.snd).bind fun b =>
+  return (a,b)
+
+abbrev op (x y : α × β) : α × β :=
+  (x.1 • y.1, x.2 • y.2)
+
+abbrev ValidN n (x : α × β) := ✓{n} x.fst ∧ ✓{n} x.snd
+
+abbrev Valid (x : α × β) := ✓ x.fst ∧ ✓ x.snd
+
+instance cmraProd : CMRA (α × β) where
+  pcore := pcore
+  op := op
+  ValidN := ValidN
+  Valid := Valid
+  op_ne {x} :=
+    {ne n y z h := dist_prod_ext (Dist.op_r $ dist_fst h) (Dist.op_r $ dist_snd h)}
+  pcore_ne {n x y cx} h ph := by
+    have ⟨cx₁, hcx₁, this⟩ := Option.bind_eq_some.mp ph
+    have ⟨cx₂, hcx₂, hcx⟩ := Option.bind_eq_some.mp this
+    have ⟨cy₁, hcy₁, hxy₁⟩ := CMRA.pcore_ne (dist_fst h) hcx₁
+    have ⟨cy₂, hcy₂, hxy₂⟩ := CMRA.pcore_ne (dist_snd h) hcx₂
+    suffices g: cx ≡{n}≡ (cy₁, cy₂) by simp [hcy₁, hcy₂, g, pcore]
+    calc
+      cx ≡{n}≡ (cx₁, cx₂) := Dist.of_eq (Option.some.inj hcx).symm
+      _  ≡{n}≡ (cy₁, cy₂) := dist_prod_ext hxy₁ hxy₂
+  validN_ne {n} x y H := fun ⟨vx1, vx2⟩ =>
+    ⟨ (Dist.validN $ dist_fst H).mp vx1, (Dist.validN $ dist_snd H).mp vx2 ⟩
+  valid_iff_validN {x} :=
+    ⟨ fun ⟨va, vb⟩ n => ⟨CMRA.Valid.validN va, CMRA.Valid.validN vb⟩,
+      fun h =>
+        ⟨ CMRA.valid_iff_validN.mpr fun n => (h n).left,
+          CMRA.valid_iff_validN.mpr fun n => (h n).right ⟩ ⟩
+  validN_succ {x n} := fun ⟨va, vb⟩ => ⟨CMRA.validN_succ va, CMRA.validN_succ vb⟩
+  validN_op_left {n x y} := fun ⟨va, vb⟩ => ⟨CMRA.validN_op_left va, CMRA.validN_op_left vb⟩
+  assoc {x y z} := ⟨CMRA.assoc, CMRA.assoc⟩
+  comm {x y} := ⟨CMRA.comm, CMRA.comm⟩
+  pcore_op_left {x cx} h :=
+    let ⟨a, ha, ho⟩ := Option.bind_eq_some.mp h
+    let ⟨b, hb, hh⟩ := Option.bind_eq_some.mp ho
+    (Option.some.inj hh) ▸ OFE.equiv_prod_ext (CMRA.pcore_op_left ha) (CMRA.pcore_op_left hb)
+  pcore_idem {x cx} h :=
+    have ⟨cx₁, hcx₁, this⟩ := Option.bind_eq_some.mp h
+    have ⟨cx₂, hcx₂, hcx⟩ := Option.bind_eq_some.mp this
+    have ⟨a, ha, ea⟩ := equiv_some (CMRA.pcore_idem hcx₁)
+    have ⟨b, hb, eb⟩ := equiv_some (CMRA.pcore_idem hcx₂)
+    suffices g: (a, b) ≡ (cx₁, cx₂) by
+      rw [Option.some.inj hcx.symm]
+      simp [ha, hb, g, pcore]
+    equiv_prod_ext ea eb
+  pcore_op_mono {x cx} h y := by
+    have ⟨cx₁, hcx₁, this⟩ := Option.bind_eq_some.mp h
+    have ⟨cx₂, hcx₂, hcx⟩ := Option.bind_eq_some.mp this
+    have ⟨cy₁, hcy₁⟩ := CMRA.pcore_op_mono hcx₁ y.fst
+    have ⟨cy₂, hcy₂⟩ := CMRA.pcore_op_mono hcx₂ y.snd
+    have ⟨a, ha, ea⟩ := equiv_some hcy₁
+    have ⟨b, hb, eb⟩ := equiv_some hcy₂
+    unfold pcore
+    rw [Option.some.inj hcx.symm, ha, hb]
+    exists (cy₁, cy₂)
+  extend {n x y₁ y₂} := fun ⟨vx₁, vx₂⟩ e =>
+    let ⟨z₁, w₁, hx₁, hz₁, hw₁⟩ := CMRA.extend vx₁ (OFE.dist_fst e)
+    let ⟨z₂, w₂, hx₂, hz₂, hw₂⟩ := CMRA.extend vx₂ (OFE.dist_snd e)
+    ⟨ (z₁, z₂), (w₁, w₂), OFE.equiv_prod_ext hx₁ hx₂,
+      OFE.dist_prod_ext hz₁ hz₂, OFE.dist_prod_ext hw₁ hw₂ ⟩
+
+theorem valid_fst {x : α × β} (h: ✓ x): ✓ x.fst := h.left
+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
+
+end Prod
+
 section optionOF
 
 variable (F : COFE.OFunctorPre)
diff --git a/src/Iris/Algebra/LocalUpdates.lean b/src/Iris/Algebra/LocalUpdates.lean
new file mode 100644
index 00000000..4ebc4a96
--- /dev/null
+++ b/src/Iris/Algebra/LocalUpdates.lean
@@ -0,0 +1,294 @@
+/-
+Copyright (c) 2025 Сухарик. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Сухарик (@suhr)
+-/
+import Iris.Algebra.CMRA
+
+namespace Iris
+
+def LocalUpdate {α: Type}[CMRA α] (x y: α × α) :=
+  ∀n mz, ✓{n} x.1 → x.1 ≡{n}≡ x.2 •? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 •? mz
+
+infixr:50 " ~l~> " => LocalUpdate
+
+namespace LocalUpdate
+
+section CMRA
+  variable [cmr: CMRA α]
+
+  -- Global Instance local_update_proper :
+  -- Proper ((≡) ==> (≡) ==> iff) (@local_update SI A).
+  -- Proof. unfold local_update. by repeat intro; setoid_subst. Qed.
+
+  theorem local_update_id (x: α × α): x ~l~> x := fun _ _ vx e => ⟨vx, e⟩
+
+  theorem local_update_left_eqv {x y: α × α} (z: α × α) (h: x ≡ y) : x ~l~> z → y ~l~> z :=
+    fun u => fun n mw v e =>
+      have e1: x.fst ≡{n}≡ y.fst := (OFE.equiv_fst h).dist
+      have := calc
+        x.fst       ≡{n}≡ y.fst       := e1
+        y.fst       ≡{n}≡ y.snd •? mw := e
+        y.snd •? mw ≡{n}≡ x.snd •? mw := CMRA.opM_left_dist mw (OFE.equiv_snd h).dist.symm
+      u n mw ((OFE.Dist.validN e1.symm).mp v) this
+
+  theorem local_update_right_eqv (x: α × α) {y z: α × α} (h: y ≡ z): x ~l~> y → x ~l~> z :=
+    fun u => fun n mw v e =>
+      let ⟨vy, e⟩ := u n mw v e
+      have e1: y.fst ≡{n}≡ z.fst := OFE.dist_fst (OFE.Equiv.dist h)
+      have := calc
+        z.fst ≡{n}≡ y.fst := e1.symm
+        _ ≡{n}≡ y.snd •? mw := e
+        _ ≡{n}≡ z.snd •? mw := CMRA.opM_left_dist mw $ OFE.dist_snd (OFE.Equiv.dist h)
+      ⟨(OFE.Dist.validN e1).mp vy, this⟩
+
+  -- Global Instance local_update_preorder : PreOrder (@local_update SI A).
+  -- Proof. split; unfold local_update; red; naive_solver. Qed.
+
+  theorem exclusive_local_update {y: α}[CMRA.Exclusive y](x x': α)(vx': ✓ x'): (x,y) ~l~> (x', x') :=
+    fun n mz vx e =>
+      have : mz = none         := CMRA.none_of_excl_valid_op ((OFE.Dist.validN e).mp vx)
+      have : x' ≡{n}≡ x' •? mz := calc
+        x' ≡{n}≡ x'   := OFE.Dist.of_eq rfl
+        _  = x' •? mz := by rw[this]; rfl
+      ⟨vx'.validN, this⟩
+
+  theorem op_local_update (x y z : α) (h : ∀ n, ✓{n} x → ✓{n} (z • x)) : (x, y) ~l~> (z • x, z • y) :=
+    fun n mz vx (e : x ≡{n}≡ y •? mz) =>
+      have g1 : ✓{n} (z • x) := h n vx
+      have g2 := calc
+        (z • x) ≡{n}≡ z • (y •? mz) := CMRA.op_right_dist z e
+        _       ≡{n}≡ (z • y) •? mz := OFE.Dist.symm (CMRA.op_opM_assoc_dist z y mz)
+      ⟨g1, g2⟩
+
+  theorem op_local_update_discrete [CMRA.Discrete α] (x y z : α)
+      (h : ✓ x → ✓ (z • x)) : (x, y) ~l~> (z • x, z • y) :=
+    fun n mz vx e =>
+      have this n (vx: ✓{n} x): ✓{n} (z • x) :=
+        CMRA.Valid.validN (h ((CMRA.valid_iff_validN' n).mpr vx))
+      op_local_update x y z this n mz vx e
+
+  theorem op_local_update_frame (x y x' y' yf : α)
+      (h : (x, y) ~l~> (x', y')) : (x, y • yf) ~l~> (x', y' • yf) :=
+    fun n mz vx e =>
+      have := h n (some yf • mz) vx
+      have := calc
+        x ≡{n}≡ (y • yf) •? mz := e
+        _ ≡{n}≡ y •? (some yf • mz) := CMRA.op_some_opM_assoc_dist y yf mz
+      have u := h n (some yf • mz) vx this
+      have := calc
+        x' ≡{n}≡ y' •? (some yf • mz) := u.2
+        _  ≡{n}≡ (y' • yf) •? mz      := (CMRA.op_some_opM_assoc_dist y' yf mz).symm
+      ⟨u.1, this⟩
+
+  theorem cancel_local_update (x y z : α) [CMRA.Cancelable x] : (x • y, x • z) ~l~> (y, z) :=
+    fun _ _ vx e => ⟨CMRA.validN_op_right vx, CMRA.op_opM_cancel_dist vx e⟩
+
+  theorem replace_local_update (x y : α) [CMRA.IdFree x] (h : ✓ y) : (x, x) ~l~> (y, y) :=
+    fun _ mz vx e =>
+      match mz with
+      | none   => ⟨CMRA.Valid.validN h, OFE.Dist.symm (OFE.Dist.of_eq rfl)⟩
+      | some _ => absurd e.symm (CMRA.id_freeN_r vx)
+
+  theorem core_id_local_update (x y z : α) [CMRA.CoreId y] (inc : y ≼ x) : (x, z) ~l~> (x, z • y) :=
+    fun n mz vx e =>
+      have g: x ≡{n}≡ (z • y) •? mz :=
+        suffices h: y • x ≡{n}≡ (z • y) •? mz
+          from (CMRA.op_core_right_of_inc inc).symm.dist.trans h
+        match mz with
+        | none =>
+          calc
+            y • x ≡{n}≡ y • z := CMRA.op_right_dist y e
+            _ ≡{n}≡ z • y := CMRA.op_commN
+        | some w =>
+          calc
+            y • x ≡{n}≡ y • (z • w) := CMRA.op_right_dist y e
+            _ ≡{n}≡ (y • z) • w := CMRA.op_assocN
+            _ ≡{n}≡ (z • y) • w := CMRA.op_left_dist w (CMRA.op_commN)
+      ⟨vx, g⟩
+
+  theorem local_update_discrete [CMRA.Discrete α] (x y x' y' : α) :
+      (x, y) ~l~> (x', y') ↔ ∀ mz, ✓ x → x ≡ y •? mz → (✓ x' ∧ x' ≡ y' •? mz) :=
+    Iff.intro
+      (fun h mz vx e =>
+        have ⟨vx', e⟩ := h 0 mz vx.validN e.dist
+        ⟨CMRA.Discrete.discrete_valid vx', OFE.discrete_0 e⟩)
+      (fun h n mz vx e =>
+        have ⟨vx', e'⟩ := h mz ((CMRA.valid_iff_validN' n).mpr vx) (OFE.discrete_n e)
+        ⟨CMRA.Valid.validN vx', e'.dist⟩)
+
+  theorem local_update_valid0 (x y x' y' : α)
+      (h: ✓{0} x → ✓{0} y → some y ≼{0} some x → (x, y) ~l~> (x', y')) :
+      (x, y) ~l~> (x', y') :=
+    fun n mz vx e =>
+      have v0y: ✓{0} y := CMRA.valid0_of_validN $ CMRA.validN_opM ((OFE.Dist.validN e).mp vx)
+      have: some y ≼{0} some x := CMRA.inc0_of_incN (CMRA.some_inc_some_of_dist_opM e)
+      have: (x, y) ~l~> (x', y') := h (CMRA.valid0_of_validN vx) v0y this
+      this n mz vx e
+
+  theorem local_update_valid [CMRA.Discrete α] (x y x' y' : α)
+      (h: ✓ x → ✓ y → some y ≼ some x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') :=
+    have h0 vx0 vy0 mz: (x, y) ~l~> (x', y') :=
+      h (CMRA.discrete_valid vx0) (CMRA.discrete_valid vy0) ((CMRA.inc_iff_incN 0).mpr mz)
+    local_update_valid0 x y x' y' h0
+
+  theorem local_update_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') :=
+    have h0 (vx0: ✓{0} x) (vy0: ✓{0} y) (mz : some y ≼{0} some x) : (x, y) ~l~> (x', y') :=
+      h vx0 vy0 (CMRA.incN_of_some_incN_some mz)
+    local_update_valid0 x y x' y' h0
+
+  theorem local_update_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') :=
+    have hs vx vy inc : (x, y) ~l~> (x', y') := h vx vy (CMRA.inc_of_some_inc_some inc)
+    local_update_valid x y x' y' hs
+end CMRA
+
+section updates_unital
+  variable [UCMRA α]
+
+  theorem local_update_unital (x y x' y' : α) :
+      (x, y) ~l~> (x', y') ↔ ∀ n z, ✓{n} x → x ≡{n}≡ y • z → (✓{n} x' ∧ x' ≡{n}≡ y' • z) where
+    mp  h n z       := h n (some z)
+    mpr h n mz vx e :=
+      match mz with
+      | none =>
+        have := h n UCMRA.unit vx (e.trans (CMRA.unit_right_id_dist y).symm)
+        ⟨this.left, this.right.trans (CMRA.unit_right_id_dist y')⟩
+      | some z => h n z vx e
+
+  theorem local_update_unital_discrete [CMRA.Discrete α] (x y x' y' : α) :
+      (x, y) ~l~> (x', y') ↔ ∀ z, ✓ x → x ≡ y • z → (✓ x' ∧ x' ≡ y' • z) where
+    mp  h z vx e :=
+      have ⟨vx', e'⟩ := h 0 (some z) (CMRA.Valid.validN vx) e.dist
+      ⟨CMRA.discrete_valid vx', OFE.discrete_0 e'⟩
+    mpr h :=
+      have h' n z vnx e : (✓{n} x' ∧ x' ≡{n}≡ y' • z) :=
+        have ⟨vx', e'⟩ := h z ((CMRA.valid_iff_validN' n).mpr vnx) (OFE.discrete_n e)
+        ⟨CMRA.Valid.validN vx', OFE.Equiv.dist e'⟩
+      (local_update_unital x y x' y').mpr h'
+
+  theorem cancel_local_update_unit (x y : α) [CMRA.Cancelable x] :
+      (x • y, x) ~l~> (y, UCMRA.unit) :=
+    have e : (x • y, x • UCMRA.unit) ≡ (x • y, x) :=
+      OFE.equiv_prod_ext OFE.Equiv.rfl (CMRA.unit_right_id)
+    local_update_left_eqv _ e (cancel_local_update x y UCMRA.unit)
+
+end updates_unital
+
+section updates_unit
+
+  theorem unit_local_update (x y x' y' : Unit) : (x, y) ~l~> (x', y') :=
+    match x, y, x', y' with
+    | .unit, .unit, .unit, .unit => local_update_id ((), ())
+
+end updates_unit
+
+section updates_discrete_fun
+
+  theorem discrete_fun_local_update {α : Type} (β : α → Type _) [∀ x, UCMRA (β x)]
+      (f g f' g' : ∀ x, β x) (h : ∀ x : α, (f x, g x) ~l~> (f' x, g' x))
+      : (f, g) ~l~> (f', g') :=
+    fun n mz vx e =>
+      have g₁ : ✓{n} f' := fun x =>
+        match mz with
+        | .none => (h x n .none (vx x) (e x)).left
+        | .some z => (h x n (.some (z x)) (vx x) (e x)).left
+      have g₂ : f' ≡{n}≡ g' •? mz := fun x =>
+        match mz with
+        | .none => (h x n .none (vx x) (e x)).right
+        | .some z => (h x n (.some (z x)) (vx x) (e x)).right
+      ⟨g₁, g₂⟩
+
+end updates_discrete_fun
+
+section updates_product
+  variable [CMRA α] [CMRA β]
+
+  theorem prod_local_update
+      {x y x' y' : α × β} (hl: (x.1, y.1) ~l~> (x'.1, y'.1)) (hr: (x.2, y.2) ~l~> (x'.2, y'.2))
+      : (x, y) ~l~> (x', y') :=
+    fun n mz vx e =>
+      match mz with
+      | .none =>
+        have ⟨v₁, e₁⟩ := hl n .none vx.left e.left
+        have ⟨v₂, e₂⟩ := hr n .none vx.right e.right
+        ⟨⟨v₁, v₂⟩, ⟨e₁, e₂⟩⟩
+      | .some z =>
+        have ⟨v₁, e₁⟩ := hl n (.some z.fst) vx.left e.left
+        have ⟨v₂, e₂⟩ := hr n (.some z.snd) vx.right e.right
+        ⟨⟨v₁, v₂⟩, ⟨e₁, e₂⟩⟩
+
+  theorem prod_local_update'
+      {x1 y1 x1' y1' : α} {x2 y2 x2' y2' : β}
+      (hl: (x1, y1) ~l~> (x1', y1')) (hr: (x2, y2) ~l~> (x2', y2'))
+      : ((x1, x2), (y1, y2)) ~l~> ((x1', x2'), (y1', y2')) :=
+    prod_local_update hl hr
+
+  theorem prod_local_update_1
+      (x1 y1 x1' y1' : α) (x2 y2 : β) (h: (x1, y1) ~l~> (x1', y1'))
+      : ((x1, x2), (y1, y2)) ~l~> ((x1', x2), (y1', y2)) :=
+    prod_local_update' h (local_update_id (x2, y2))
+
+  theorem prod_local_update_2
+      (x1 y1 : α) (x2 y2 x2' y2' : β) (h: (x2, y2) ~l~> (x2', y2'))
+      : ((x1, x2), (y1, y2)) ~l~> ((x1, x2'), (y1, y2')) :=
+    prod_local_update' (local_update_id (x1, y1)) h
+
+end updates_product
+
+section updates_option
+  theorem option_local_update {α : Type} [CMRA α]
+      {x y x' y' : α} (h: (x, y) ~l~> (x', y')) : (some x, some y) ~l~> (some x', some y') :=
+    fun n mz vx e =>
+      match mz with
+      | .none           => h n .none vx e
+      | .some .none     => have ⟨vx, e⟩ := h n .none vx e;  ⟨vx, e⟩
+      | .some (.some z) => have ⟨vx, e⟩ := h n (.some z) vx e;  ⟨vx, e⟩
+
+  theorem option_local_update_none {α : Type} [UCMRA α]
+      {x x' y' : α} (h: (x, UCMRA.unit) ~l~> (x', y')): (some x, none) ~l~> (some x', some y') :=
+    fun n mz vx e =>
+      match mz with
+      | .none           => False.elim e
+      | .some .none     => False.elim e
+      | .some (.some z) =>
+        have e: x ≡{n}≡ z := e
+        have ⟨vx, e⟩ := h n (.some z) vx (e.trans (CMRA.unit_left_id_dist z).symm)
+        ⟨vx, e⟩
+
+  theorem alloc_option_local_update {α : Type} [CMRA α]
+      {x : α} (y : Option α) (vx: ✓ x): (none, y) ~l~> (some x, some x) :=
+    fun n mz _ e =>
+      match mz with
+      | .none           => ⟨CMRA.Valid.validN vx, OFE.Dist.of_eq rfl⟩
+      | .some .none     => ⟨CMRA.Valid.validN vx, OFE.Dist.of_eq rfl⟩
+      | .some (.some z) =>
+        have ⟨_, hw⟩ := CMRA.exists_op_some_dist_some (n := n) y z
+        False.elim (e.trans hw)
+
+  theorem delete_option_local_update {α : Type} [CMRA α]
+      (x : Option α) (y : α) [CMRA.Exclusive y] :
+      (x, some y) ~l~> (none, none) :=
+    fun n mz vx e =>
+      match mz with
+      | .none           => ⟨True.intro, OFE.Dist.of_eq rfl⟩
+      | .some .none     => ⟨True.intro, OFE.Dist.of_eq rfl⟩
+      | .some (.some z) =>
+        have : ✓{n} some y • some z := (OFE.Dist.validN e).mp vx
+        absurd this not_valid_some_exclN_op_left
+
+  theorem delete_option_local_update_cancelable {α : Type} [CMRA α]
+      (mx : Option α) [CMRA.Cancelable mx] : (mx, mx) ~l~> (none, none) :=
+    fun n mz vx e =>
+      match mz with
+      | .none           => ⟨True.intro, OFE.Dist.of_eq rfl⟩
+      | .some .none     => ⟨True.intro, OFE.Dist.of_eq rfl⟩
+      | .some (.some z) =>
+        have : CMRA.unit ≡{n}≡ some z :=
+          CMRA.cancelableN (validN_op_unit vx) ((CMRA.unit_right_id_dist mx).trans e)
+        ⟨True.intro, this⟩
+
+end updates_option
+
+end LocalUpdate
diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index 41230250..461d26e7 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -229,6 +229,14 @@ instance [OFE α] : OFE (Option α) where
   equiv_dist {x y} := by cases x <;> cases y <;> simp [Option.Forall₂]; apply equiv_dist
   dist_lt {_ x y _} := by cases x <;> cases y <;> simp [Option.Forall₂]; apply dist_lt
 
+instance [OFE α][OFE.Discrete α]: OFE.Discrete (Option α) where
+  discrete_0 {mx my} e :=
+    match mx, my with
+    | none,   none   => e
+    | none,   some _ => e
+    | some _, none   => e
+    | some x, some y => show x ≡ y from discrete_0 e
+
 @[simp] theorem some_eqv_some [OFE α] {x y : α} : (some x ≡ some y) ↔ x ≡ y := .rfl
 @[simp] theorem not_some_eqv_none [OFE α] {x : α} : ¬some x ≡ none := id
 @[simp] theorem not_none_eqv_some [OFE α] {x : α} : ¬none ≡ some x := id
@@ -304,6 +312,16 @@ instance [OFE α] [OFE β] : OFE (α × β) where
   equiv_dist {_ _} := by simp [equiv_dist, forall_and]
   dist_lt h1 h2 := ⟨dist_lt h1.1 h2, dist_lt h1.2 h2⟩
 
+def equiv_fst [OFE α] [OFE β] {x y: α × β} (h: x ≡ y): x.fst ≡ y.fst := h.left
+def equiv_snd [OFE α] [OFE β] {x y: α × β} (h: x ≡ y): x.snd ≡ y.snd := h.right
+def equiv_prod_ext [OFE α] [OFE β] {x₁ x₂: α} {y₁ y₂: β}
+    (ex: x₁ ≡ x₂) (ey: y₁ ≡ y₂): (x₁, y₁) ≡ (x₂, y₂) := ⟨ex, ey⟩
+
+def dist_fst {n} [OFE α] [OFE β] {x y: α × β} (h: x ≡{n}≡ y): x.fst ≡{n}≡ y.fst := h.left
+def dist_snd {n} [OFE α] [OFE β] {x y: α × β} (h: x ≡{n}≡ y): x.snd ≡{n}≡ y.snd := h.right
+def 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⟩
+
 /-- 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
   hom : α -n> β
diff --git a/src/Iris/Algebra/Updates.lean b/src/Iris/Algebra/Updates.lean
new file mode 100644
index 00000000..e55fc433
--- /dev/null
+++ b/src/Iris/Algebra/Updates.lean
@@ -0,0 +1,304 @@
+/-
+Copyright (c) 2025 Сухарик. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Сухарик (@suhr)
+-/
+import Iris.Algebra.CMRA
+
+namespace Iris
+
+def UpdateP [CMRA α] (x : α) (P : α → Prop) := ∀ n mz,
+  ✓{n} (x •? mz) → ∃ y, P y ∧ ✓{n} (y •? mz)
+infixr:50 " ~~>: " => UpdateP
+
+def Update [CMRA α] (x y : α) := ∀ n mz,
+  ✓{n} (x •? mz) → ✓{n} (y •? mz)
+infixr:50 " ~~> " => Update
+
+section updates
+
+variable [CMRA α] [CMRA β] (f : α → β) (g : β → α)
+
+-- (* Global Instance cmra_updateP_proper :
+--   Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP SI A).
+-- Proof. Admitted. *)
+
+-- (* Global Instance cmra_update_proper :
+--   Proper ((≡) ==> (≡) ==> iff) (@cmra_update SI A).
+-- Proof. Admitted. *)
+
+theorem UpdateP.equiv_left {P : α → Prop} {x y: α} (e: x ≡ y) (u: x ~~>: P): y ~~>: P :=
+  fun n mz v => u n mz (CMRA.validN_ne (CMRA.opM_left_dist mz e.symm.dist) v)
+
+theorem Update.equiv_left {x y z: α} (e: x ≡ y) (u: x ~~> z): y ~~> z :=
+  fun n mz v => u n mz (CMRA.validN_ne (CMRA.opM_left_dist mz e.symm.dist) v)
+
+theorem Update.equiv_right {x y z: α} (e: y ≡ z) (u: x ~~> y): x ~~> z :=
+  fun n mz v => CMRA.validN_ne (CMRA.opM_left_dist mz e.dist) (u n mz v)
+
+instance [CMRA α] : Trans OFE.Equiv UpdateP UpdateP (α := α) where
+  trans e u := UpdateP.equiv_left e.symm u
+
+instance [CMRA α] : Trans OFE.Equiv Update Update (α := α) where
+  trans e u := Update.equiv_left (id (OFE.Equiv.symm e)) u
+
+instance [CMRA α] : Trans Update OFE.Equiv Update (α := α) where
+  trans u e := Update.equiv_right e u
+
+
+theorem Update.of_updateP {x y: α} (h: x ~~>: (y = ·)): x ~~> y :=
+  fun n mz v => let ⟨_, e, v⟩ := (h n mz v);  e ▸ v
+
+theorem UpdateP.of_update {x y: α} (h: x ~~> y): x ~~>: (y = ·) :=
+  fun n mz v => ⟨y, rfl, h n mz v⟩
+
+theorem UpdateP.id (P : α → Prop) x (h: P x): x ~~>: P :=
+  fun _ _ v => ⟨x, h, v⟩
+
+theorem Update.id (x : α): x ~~> x := fun _ _ h => h
+
+theorem Update.trans {x y z: α} (uxy: x ~~> y) (uyz: y ~~> z) : x ~~> z :=
+  fun n mz v => uyz n mz (uxy n mz v)
+
+theorem UpdateP.trans (P Q : α → Prop) x (ux: x ~~>: P) (upq : ∀ y, P y → y ~~>: Q)
+    : x ~~>: Q :=
+  fun n mz v => let ⟨y, py, vy⟩ := ux n mz v;  upq y py n mz vy
+
+theorem Update.transP {Q : α → Prop} {x y} (uxy: x ~~> y) (uyq: y ~~>: Q) : x ~~>: Q :=
+  fun n mz v => uyq n mz (uxy n mz v)
+
+theorem UpdateP.weaken (P Q : α → Prop) x (uxp: x ~~>: P) (pq: ∀ y, P y → Q y)
+    : x ~~>: Q :=
+  fun n mz v => let ⟨y, py, vy⟩ := uxp n mz v;  ⟨y, pq y py, vy⟩
+
+theorem Update.exclusive {x y: α} [CMRA.Exclusive x] (vy: ✓ y): x ~~> y :=
+  fun _ _ P => (CMRA.none_of_excl_valid_op P) ▸ CMRA.Valid.validN vy
+
+instance [CMRA α] : Trans Update Update Update (α := α) where
+  trans := Update.trans
+
+instance [CMRA α] : Trans Update UpdateP UpdateP (α := α) where
+  trans := Update.transP
+
+-- (** Updates form a preorder. *)
+-- (** We set this rewrite relation's cost above the stdlib's
+--   ([impl], [iff], [eq], ...) and [≡] but below [⊑].
+--   [eq] (at 100) < [≡] (at 150) < [cmra_update] (at 170) < [⊑] (at 200) *)
+
+-- (* Global Instance cmra_update_rewrite_relation :
+--   RewriteRelation (@cmra_update SI A) | 170 := {}. *)
+
+-- (* Global Instance cmra_update_preorder : PreOrder (@cmra_update SI A).
+-- Proof. Admitted. *)
+
+-- (* Global Instance cmra_update_proper_update :
+--   Proper (flip cmra_update ==> cmra_update ==> impl) (@cmra_update SI A).
+-- Proof. Admitted. *)
+
+-- (* Global Instance cmra_update_flip_proper_update :
+--   Proper (cmra_update ==> flip cmra_update ==> flip impl) (@cmra_update SI A).
+-- Proof. Admitted. *)
+
+theorem UpdateP.op {P Q R : α → Prop} {x y}
+    (uxp: x ~~>: P) (uyq: y ~~>: Q) (pqr: ∀z w, P z → Q w → R (z • w))
+    : x • y ~~>: R :=
+  fun n mz v =>
+    have e₁: (x • y) •? mz ≡{n}≡ y •? some (x •? mz) :=
+      (CMRA.opM_left_dist mz CMRA.op_commN).trans (CMRA.op_opM_assoc_dist _ _ mz)
+    let ⟨w, pw, vw⟩ := uyq n (some (x •? mz)) (CMRA.validN_ne e₁ v)
+    have e₂: w •? some (x •? mz) ≡{n}≡ x •? some (w •? mz) := calc
+      w •? some (x •? mz) ≡{n}≡ (w • x) •? mz       := (CMRA.op_opM_assoc_dist w x mz).symm
+      _                   ≡{n}≡ (x • w) •? mz       := (CMRA.opM_left_dist mz CMRA.op_commN)
+      _                   ≡{n}≡ x •? some (w •? mz) := CMRA.op_opM_assoc_dist x w mz
+    let ⟨z, pz, vz⟩ := uxp n (some (w •? mz)) (CMRA.validN_ne e₂ vw)
+    ⟨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 :=
+  UpdateP.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₂ :=
+  Update.of_updateP $
+    UpdateP.op (UpdateP.of_update xy₁) (UpdateP.of_update xy₂)
+      fun _ _ ez ew => ez ▸ ew ▸ rfl
+
+-- (* Global Instance cmra_update_op_proper :
+--   Proper (cmra_update ==> cmra_update ==> cmra_update) (op (A:=A)).
+-- Proof. Admitted. *)
+
+-- (* Global Instance cmra_update_op_flip_proper :
+--   Proper (flip cmra_update ==> flip cmra_update ==> flip cmra_update) (op (A:=A)).
+-- Proof. Admitted. *)
+
+
+-- (* Global Instance cmra_update_op_proper :
+--   Proper (cmra_update ==> cmra_update ==> cmra_update) (op (A:=A)).
+-- Proof. Admitted. *)
+
+-- (* Global Instance cmra_update_op_flip_proper :
+--   Proper (flip cmra_update ==> flip cmra_update ==> flip cmra_update) (op (A:=A)).
+-- Proof. Admitted. *)
+
+
+theorem Update.op_l (x y : α) : x • y ~~> x := fun _ _ => CMRA.validN_op_opM_left
+
+theorem Update.op_r (x y : α) : x • y ~~> y := fun _ _ => CMRA.validN_op_opM_right
+
+theorem Update.included (x y : α) : x ≼ y → y ~~> x :=
+  fun ⟨z, ez⟩ => Update.equiv_left ez.symm (Update.op_l x z)
+
+theorem Update.valid0 (x y : α) : (✓{0} x → x ~~> y) → x ~~> y :=
+  fun h n mz v => h (CMRA.valid0_of_validN (CMRA.validN_opM v)) n mz v
+
+-- Frame preserving updates for total and discete CMRAs
+
+theorem UpdateP.total [CMRA.IsTotal α] (x : α) (P : α → Prop)
+    : x ~~>: P ↔ ∀ (n : Nat) (z : α), ✓{n} (x • z) → ∃ y, P y ∧ ✓{n} (y • z) where
+  mp uxp := fun n z v => uxp n (some z) v
+  mpr h := fun n mz v =>
+    match mz with
+    | .none =>
+      let ⟨y, py, vy⟩ := h n (CMRA.core x) (CMRA.validN_ne (CMRA.op_core_dist x).symm v)
+      ⟨y, py, CMRA.validN_op_opM_left vy⟩
+    | .some z => h n z v
+
+theorem Update.total [CMRA.IsTotal α] (x y : α)
+    : x ~~> y ↔ ∀ (n : Nat) (z : α), ✓{n} (x • z) → ✓{n} (y • z) where
+  mp uxy := fun n z v => uxy n (some z) v
+  mpr h := fun n mz v =>
+    match mz with
+    | .none =>
+      CMRA.validN_op_opM_left $ h n (CMRA.core x) (CMRA.validN_ne (CMRA.op_core_dist x).symm v)
+    | .some z => h n z v
+
+
+theorem UpdateP.discrete [CMRA.Discrete α] (x : α) (P : α → Prop)
+    : x ~~>: P ↔ ∀ (mz : Option α), ✓ (x •? mz) → ∃ y, P y ∧ ✓ (y •? mz) where
+  mp uxp := fun mz v =>
+    let ⟨y, py, vy⟩ := uxp 0 mz (CMRA.Valid.validN v)
+    ⟨y, py, CMRA.discrete_valid vy⟩
+  mpr h := fun n mz v =>
+    let ⟨y, py, vy⟩ := h mz ((CMRA.valid_iff_validN' n).mpr v)
+    ⟨y, py, CMRA.Valid.validN vy⟩
+
+theorem Update.discrete [CMRA.Discrete α] (x y : α)
+    : x ~~> y ↔ ∀ (mz : Option α), ✓ (x •? mz) → ✓ (y •? mz) where
+  mp uxp := fun mz v => CMRA.discrete_valid $ uxp 0 mz (CMRA.Valid.validN v)
+  mpr h := fun n mz v => CMRA.Valid.validN $ h mz ((CMRA.valid_iff_validN' n).mpr v)
+
+theorem UpdateP.discrete_total [CMRA.Discrete α] [CMRA.IsTotal α] (x : α) (P : α → Prop)
+    : x ~~>: P ↔ ∀ (z : α), ✓ (x • z) → ∃ y, P y ∧ ✓ (y • z) where
+  mp uxp := fun z vz =>
+    let ⟨y, py, vy⟩ := (UpdateP.total x P).mp uxp 0 z (CMRA.Valid.validN vz)
+    ⟨y, py, CMRA.discrete_valid vy⟩
+  mpr h :=
+    have this n z (v: ✓{n} x • z): ∃ y, P y ∧ ✓{n} (y • z) :=
+      let ⟨y, py, vy⟩ := h z ((CMRA.valid_iff_validN' n).mpr v)
+      ⟨y, py, CMRA.Valid.validN vy⟩
+    (UpdateP.total x P).mpr this
+
+theorem Update.discrete_total [CMRA.Discrete α] [CMRA.IsTotal α] (x y : α)
+    : x ~~> y ↔ ∀ (z : α), ✓ (x • z) → ✓ (y • z) where
+  mp uxp := fun z vz =>
+    CMRA.discrete_valid $ (Update.total x y).mp uxp 0 z (CMRA.Valid.validN vz)
+  mpr h :=
+    have this n z (v: ✓{n} x • z): ✓{n} (y • z) :=
+      CMRA.Valid.validN $ h z ((CMRA.valid_iff_validN' n).mpr v)
+    (Update.total x y).mpr this
+
+-- (** * Transport *)
+-- Section cmra_transport.
+--   Context {SI : sidx} {A B : cmra} (H : A = B).
+--   Notation T := (cmra_transport H).
+--   Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x :
+--     x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q.
+--   Proof. Admitted.
+
+--   Lemma cmra_transport_updateP' (P : A → Prop) x :
+--     x ~~>: P → T x ~~>: λ y, ∃ y', y = cmra_transport H y' ∧ P y'.
+--   Proof. Admitted.
+
+-- End cmra_transport.
+
+/-! ## Isomorphism -/
+theorem UpdateP.iso {P : β → Prop} {Q : α → Prop} {y : β}
+    (gf : ∀ x, g (f x) ≡ x)
+    (g_op : ∀ y1 y2, g (y1 • y2) ≡ g y1 • g y2)
+    (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y)
+    (uyp: y ~~>: P)
+    (pq: ∀ y', P y' → Q (g y'))
+    : g y ~~>: Q :=
+  fun n mz v =>
+    have : ✓{n} y •? Option.map f mz :=
+      match mz with
+      | .none => (g_validN n _).mp v
+      | .some z =>
+        have : g y • z ≡ g (y • f z) :=
+          (CMRA.op_right_eqv _ (gf z).symm).trans (g_op y (f z)).symm
+        (g_validN n _).mp (CMRA.validN_ne this.dist v)
+    have ⟨x, px, vx⟩ := uyp n (mz.map f) this
+    have : g (x •? Option.map f mz) ≡ g x •? mz :=
+      match mz with
+      | .none => OFE.Equiv.rfl
+      | .some z => (g_op x (f z)).trans (CMRA.op_right_eqv (g x) (gf z))
+    ⟨g x, pq x px, CMRA.validN_ne this.dist ((g_validN n _).mpr vx)⟩
+
+theorem UpdateP.iso' (P : β → Prop) (y : β)
+    (gf : ∀ x, g (f x) ≡ x)
+    (g_op : ∀ y1 y2, g (y1 • y2) ≡ g y1 • g y2)
+    (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y)
+    (uyp: y ~~>: P)
+    : g y ~~>: λ x ↦ ∃ y, x = g y ∧ P y :=
+  UpdateP.iso f g gf g_op g_validN uyp (fun z pz => ⟨z, rfl, pz⟩)
+
+/-! ## Lift -/
+theorem Update.lift_updateP (x y : β)
+    (H : ∀ P, x ~~>: P → g x ~~>: λ a' ↦ ∃ b', a' = g b' ∧ P b')
+    (uxy: x ~~> y)
+    : g x ~~> g y :=
+  Update.of_updateP fun n mz v =>
+    have ⟨z, hz, vz⟩ := H _ (UpdateP.of_update uxy) n mz v
+    have hz : z = g y := by simp at hz ⊢; exact hz
+    ⟨z, hz.symm, vz⟩
+
+/-! ## Product -/
+theorem UpdateP.prod {P : α → Prop} {Q : β → Prop} {R : α × β → Prop} {x : α × β}
+    (uxp: x.fst ~~>: P) (uxq: x.snd ~~>: Q) (pq: ∀ a b, P a → Q b → R (a, b))
+    : x ~~>: R :=
+  fun n mz v =>
+    match mz with
+    | .none =>
+      have ⟨y₁, py, vy₁⟩ := uxp n .none (Prod.validN_fst v)
+      have ⟨y₂, qy, vy₂⟩ := uxq n .none (Prod.validN_snd v)
+      ⟨(y₁, y₂), pq y₁ y₂ py qy, ⟨vy₁, vy₂⟩⟩
+    | .some z =>
+      have ⟨y₁, py, vy₁⟩ := uxp n (.some z.fst) (Prod.validN_fst v)
+      have ⟨y₂, qy, vy₂⟩ := uxq n (.some z.snd) (Prod.validN_snd v)
+      ⟨(y₁, y₂), pq y₁ y₂ py qy, ⟨vy₁, vy₂⟩⟩
+
+theorem UpdateP.prod' (P : α → Prop) (Q : β → Prop) (x : α × β)
+    (uxp: x.fst ~~>: P) (uxq: x.snd ~~>: Q) : x ~~>: λ y ↦ P (y.fst) ∧ Q (y.snd) :=
+  UpdateP.prod uxp uxq (fun _ _ px qy => ⟨px, qy⟩)
+
+theorem Update.prod (x : α × β) (uxy₁: x.fst ~~> y.fst) (uxy₂: x.snd ~~> y.snd) : x ~~> y :=
+  Update.of_updateP $
+    UpdateP.prod (UpdateP.of_update uxy₁) (UpdateP.of_update uxy₂)
+      (fun _ _ ya yb => Prod.ext ya yb)
+
+/-! ## Option -/
+theorem UpdateP.option {P : α → Prop} {Q : Option α → Prop} {x : α}
+    (uxp: x ~~>: P) (pq: ∀ y, P y → Q (some y)) : some x ~~>: Q :=
+  fun n mz v =>
+    match mz with
+    | .none           => let ⟨w, pw, vw⟩ := uxp n .none v;  ⟨w, pq w pw, vw⟩
+    | .some .none     => let ⟨w, pw, vw⟩ := uxp n .none v;  ⟨w, pq w pw, vw⟩
+    | .some (.some z) => let ⟨w, pw, vw⟩ := uxp n (.some z) v;  ⟨w, pq w pw, vw⟩
+
+theorem UpdateP.option' (P : α → Prop) (x : α) (uxp: x ~~>: P)
+    : some x ~~>: Option.rec False P :=
+  UpdateP.option uxp (fun _ py => py)
+
+theorem Update.option (x y : α) (uxy: x ~~> y): some x ~~> some y :=
+  Update.of_updateP $
+    UpdateP.option (UpdateP.of_update uxy) (fun _ => congrArg some)