diff --git a/PORTING.md b/PORTING.md
index 8d7045bf..4e2a8e48 100644
--- a/PORTING.md
+++ b/PORTING.md
@@ -17,7 +17,11 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] Updates
   - [x] Functors
 - [ ] `big_op.v`
-  - TBD (Zongyuan?)
+  - [x] Lists
+  - [x] Maps
+  - [ ] Sets
+  - [ ] Multisets
+  - [ ] Homomorphisms
 - [ ] `cmra.v`
   - [x] Lemmas
   - [ ] Total CMRA construction
@@ -72,7 +76,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `max_prefix_list.v` 
   - [ ] Lemmas
   - [ ] Functors
-- [ ] `monoid.v`
+- [x] `monoid.v`
 - [ ] `mra.v`
 - [x] `numbers.v`
 - [ ]  `ofe.v`
@@ -430,5 +434,3 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] `language.v`
   - [ ] `ectx_language.v`
   - [ ] `ectxi_language.v`
-
-
diff --git a/src/Iris/Algebra/BigOp.lean b/src/Iris/Algebra/BigOp.lean
new file mode 100644
index 00000000..698f39a6
--- /dev/null
+++ b/src/Iris/Algebra/BigOp.lean
@@ -0,0 +1,698 @@
+/-
+Copyright (c) 2026 Zongyuan Liu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zongyuan Liu
+-/
+import Iris.Algebra.Monoid
+import Iris.Std.List
+import Iris.Std.PartialMap
+
+namespace Iris.Algebra
+
+/-! # Big Operators
+
+This file defines big operators (fold operations) at the abstract OFE level.
+These are parameterized by a monoid operation and include theorems about their properties.
+-/
+
+open OFE
+open Iris.Std
+
+def bigOpL {M : Type u} {A : Type v} [OFE M] (op : M → M → M) {unit : M} [MonoidOps op unit]
+    (Φ : Nat → A → M) (l : List A) : M :=
+  match l with
+  | [] => unit
+  | x :: xs => op (Φ 0 x) (bigOpL op (fun n => Φ (n + 1)) xs)
+
+def bigOpM {M : Type u} [OFE M] (op : M → M → M) {unit : M} [MonoidOps op unit]
+{K : Type _} {V : Type _} (Φ : K → V → M) {M' : Type _ → Type _} [LawfulFiniteMap M' K]
+(m : M' V) : M :=
+  bigOpL op (fun _ kv => Φ kv.1 kv.2) (toList (K := K) m)
+
+/-- Big op over list with index: `[^ op list] k ↦ x ∈ l, P` -/
+scoped syntax atomic("[^") term " list]" ident " ↦ " ident " ∈ " term ", " term : term
+/-- Big op over list without index: `[^ op list] x ∈ l, P` -/
+scoped syntax atomic("[^") term " list]" ident " ∈ " term ", " term : term
+
+/-- Big op over map with key: `[^ op map] k ↦ x ∈ m, P` -/
+scoped syntax atomic("[^") term " map]" ident " ↦ " ident " ∈ " term ", " term : term
+/-- Big op over map without key: `[^ op map] x ∈ m, P` -/
+scoped syntax atomic("[^") term " map]" ident " ∈ " term ", " term : term
+
+scoped macro_rules
+  | `([^ $o list] $k ↦ $x ∈ $l, $P) => `(bigOpL $o (fun $k $x => $P) $l)
+  | `([^ $o list] $x ∈ $l, $P) => `(bigOpL $o (fun _ $x => $P) $l)
+  | `([^ $o map] $k ↦ $x ∈ $m, $P) => `(bigOpM $o (fun $k $x => $P) $m)
+  | `([^ $o map] $x ∈ $m, $P) => `(bigOpM $o (fun _ $x => $P) $m)
+
+namespace BigOpL
+
+variable {M : Type _} {A : Type _} [OFE M] {op : M → M → M} {unit : M} [MonoidOps op unit]
+
+@[simp] theorem nil (Φ : Nat → A → M) :
+    ([^ op list] k ↦ x ∈ ([] : List A), Φ k x) = unit := rfl
+
+@[simp] theorem cons (Φ : Nat → A → M) (a : A) (as : List A) :
+    ([^ op list] k ↦ x ∈ a :: as, Φ k x) = op (Φ 0 a) ([^ op list] k ↦ x ∈ as, Φ (k + 1) x) := rfl
+
+@[simp] theorem singleton (Φ : Nat → A → M) (a : A) :
+    ([^ op list] k ↦ x ∈ [a], Φ k x) ≡ Φ 0 a := by
+  simp only [cons, nil]; exact MonoidOps.op_right_id _
+
+theorem congr {Φ Ψ : Nat → A → M} {l : List A}
+    (h : ∀ i x, l[i]? = some x → Φ i x ≡ Ψ i x) :
+    ([^ op list] k ↦ x ∈ l, Φ k x) ≡ ([^ op list] k ↦ x ∈ l, Ψ k x) := by
+  induction l generalizing Φ Ψ with
+  | nil => exact Equiv.rfl
+  | cons y ys ih =>
+    simp only [cons]
+    apply MonoidOps.op_proper (h 0 y rfl)
+    exact ih fun i x hget => h (i + 1) x hget
+
+theorem congr_dist {Φ Ψ : Nat → A → M} {l : List A} {n : Nat}
+    (h : ∀ i x, l[i]? = some x → Φ i x ≡{n}≡ Ψ i x) :
+    ([^ op list] k ↦ x ∈ l, Φ k x) ≡{n}≡ ([^ op list] k ↦ x ∈ l, Ψ k x) := by
+  induction l generalizing Φ Ψ with
+  | nil => exact Dist.rfl
+  | cons y ys ih =>
+    simp only [cons]
+    apply MonoidOps.op_ne_dist (h 0 y rfl)
+    exact ih fun i x hget => h (i + 1) x hget
+
+/-- Congruence when the functions are equivalent on all indices. -/
+theorem congr_forall {Φ Ψ : Nat → A → M} {l : List A}
+    (h : ∀ i x, Φ i x ≡ Ψ i x) :
+    ([^ op list] k ↦ x ∈ l, Φ k x) ≡ ([^ op list] k ↦ x ∈ l, Ψ k x) :=
+  congr (fun i x _ => h i x)
+
+theorem append (Φ : Nat → A → M) (l₁ l₂ : List A) :
+    ([^ op list] k ↦ x ∈ l₁ ++ l₂, Φ k x) ≡
+      op ([^ op list] k ↦ x ∈ l₁, Φ k x) ([^ op list] k ↦ x ∈ l₂, Φ (k + l₁.length) x) := by
+  induction l₁ generalizing Φ with
+  | nil => simp only [nil]; exact (MonoidOps.op_left_id _).symm
+  | cons x xs ih =>
+    simp only [List.cons_append, cons, List.length_cons]
+    apply (MonoidOps.op_congr_r (ih _)).trans
+    simp only [show ∀ n, n + xs.length + 1 = n + (xs.length + 1) from by omega]
+    exact (MonoidOps.op_assoc _ _ _).symm
+
+theorem snoc (Φ : Nat → A → M) (l : List A) (a : A) :
+    ([^ op list] k ↦ x ∈ l ++ [a], Φ k x) ≡ op ([^ op list] k ↦ x ∈ l, Φ k x) (Φ l.length a) := by
+  have := append (op := op) Φ l [a]
+  simp only [cons, nil, Nat.zero_add] at this
+  refine this.trans ?_
+  exact MonoidOps.op_congr_r (MonoidOps.op_right_id _)
+
+theorem const_unit (l : List A) :
+    ([^ op list] _x ∈ l, unit) ≡ unit := by
+  induction l with
+  | nil => exact Equiv.rfl
+  | cons _ _ ih =>
+    simp only [cons]
+    refine (MonoidOps.op_left_id _).trans ?_
+    exact ih
+
+theorem op_distrib (Φ Ψ : Nat → A → M) (l : List A) :
+    ([^ op list] k ↦ x ∈ l, op (Φ k x) (Ψ k x)) ≡
+      op ([^ op list] k ↦ x ∈ l, Φ k x) ([^ op list] k ↦ x ∈ l, Ψ k x) := by
+  induction l generalizing Φ Ψ with
+  | nil => simp only [nil]; exact Equiv.symm (MonoidOps.op_left_id _)
+  | cons x xs ih =>
+    simp only [cons]
+    refine (MonoidOps.op_congr_r (ih _ _)).trans ?_
+    exact MonoidOps.op_op_swap
+
+theorem map {B : Type v} (h : A → B) (Φ : Nat → B → M) (l : List A) :
+    ([^ op list] k ↦ x ∈ l.map h, Φ k x) ≡ ([^ op list] k ↦ x ∈ l, Φ k (h x)) := by
+  induction l generalizing Φ with
+  | nil => exact Equiv.rfl
+  | cons x xs ih =>
+    simp only [List.map_cons, cons]
+    exact MonoidOps.op_proper Equiv.rfl (ih _)
+
+theorem closed (P : M → Prop) (Φ : Nat → A → M) (l : List A)
+    (hunit : P unit)
+    (hop : ∀ x y, P x → P y → P (op x y))
+    (hf : ∀ i x, l[i]? = some x → P (Φ i x)) :
+    P ([^ op list] k ↦ x ∈ l, Φ k x) := by
+  induction l generalizing Φ with
+  | nil => exact hunit
+  | cons y ys ih =>
+    simp only [cons]
+    exact hop _ _ (hf 0 y rfl) (ih _ fun i x hget => hf (i + 1) x hget)
+
+theorem perm (Φ : A → M) {l₁ l₂ : List A} (hp : l₁.Perm l₂) :
+    ([^ op list] x ∈ l₁, Φ x) ≡ ([^ op list] x ∈ l₂, Φ x) := by
+  induction hp with
+  | nil => exact Equiv.rfl
+  | cons _ _ ih => simp only [cons]; exact MonoidOps.op_congr_r ih
+  | swap _ _ _ => simp only [cons]; exact MonoidOps.op_swap_inner (unit := unit)
+  | trans _ _ ih1 ih2 => exact Equiv.trans ih1 ih2
+
+theorem take_drop (Φ : Nat → A → M) (l : List A) (n : Nat) :
+    ([^ op list] k ↦ x ∈ l, Φ k x) ≡
+      op ([^ op list] k ↦ x ∈ l.take n, Φ k x) ([^ op list] k ↦ x ∈ l.drop n, Φ (n + k) x) := by
+  by_cases hn : n ≤ l.length
+  · have := append (op := op) Φ (l.take n) (l.drop n)
+    simp only [List.take_append_drop, List.length_take_of_le hn, Nat.add_comm] at this
+    exact this
+  · simp only [Nat.not_le] at hn
+    simp only [List.drop_eq_nil_of_le (Nat.le_of_lt hn)
+             , List.take_of_length_le (Nat.le_of_lt hn), nil]
+    exact Equiv.symm (MonoidOps.op_right_id _)
+
+theorem filter_map {B : Type v} (h : A → Option B) (Φ : B → M) (l : List A) :
+    ([^ op list] x ∈ l.filterMap h, Φ x) ≡
+      ([^ op list] x ∈ l, (h x).elim unit Φ) := by
+  induction l with
+  | nil => exact Equiv.rfl
+  | cons x xs ih =>
+    simp only [List.filterMap_cons]
+    cases hx : h x <;> simp only [hx, Option.elim, cons]
+    · exact Equiv.trans ih (Equiv.symm (MonoidOps.op_left_id _))
+    · exact MonoidOps.op_congr_r ih
+
+theorem bind {B : Type v} (h : A → List B) (Φ : B → M) (l : List A) :
+    ([^ op list] x ∈ l.flatMap h, Φ x) ≡
+      ([^ op list] x ∈ l, [^ op list] y ∈ h x, Φ y) := by
+  induction l with
+  | nil => exact Equiv.rfl
+  | cons x xs ih =>
+    simp only [List.flatMap_cons, cons]
+    refine (append _ _ _).trans ?_
+    exact MonoidOps.op_congr_r ih
+
+theorem gen_proper_2 {B : Type v} (R : M → M → Prop)
+    (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B)
+    (hunit : R unit unit)
+    (hop : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b'))
+    (hlen : l₁.length = l₂.length)
+    (hf : ∀ i, ∀ x y, l₁[i]? = some x → l₂[i]? = some y → R (Φ i x) (Ψ i y)) :
+    R ([^ op list] k ↦ x ∈ l₁, Φ k x) ([^ op list] k ↦ x ∈ l₂, Ψ k x) := by
+  induction l₁ generalizing l₂ Φ Ψ with
+  | nil =>
+    cases l₂ with
+    | nil => simp only [nil]; exact hunit
+    | cons _ _ => simp at hlen
+  | cons x xs ih =>
+    cases l₂ with
+    | nil => simp at hlen
+    | cons y ys =>
+      simp only [List.length_cons, Nat.add_right_cancel_iff] at hlen
+      simp only [cons]
+      exact hop _ _ _ _ (hf 0 x y rfl rfl)
+        (ih _ _ _ hlen fun i a b ha hb => hf (i + 1) a b ha hb)
+
+theorem gen_proper (R : M → M → Prop)
+    (Φ Ψ : Nat → A → M) (l : List A)
+    (hR_refl : ∀ x, R x x)
+    (hR_op : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b'))
+    (hf : ∀ k y, l[k]? = some y → R (Φ k y) (Ψ k y)) :
+    R ([^ op list] k ↦ x ∈ l, Φ k x) ([^ op list] k ↦ x ∈ l, Ψ k x) := by
+  apply gen_proper_2 R Φ Ψ l l (hR_refl unit) hR_op rfl
+  intro k x y hx hy; rw [hx] at hy; cases hy; exact hf k x hx
+
+theorem ext {Φ Ψ : Nat → A → M} {l : List A}
+    (h : ∀ i x, l[i]? = some x → Φ i x = Ψ i x) :
+    ([^ op list] k ↦ x ∈ l, Φ k x) = ([^ op list] k ↦ x ∈ l, Ψ k x) :=
+  gen_proper (· = ·) _ _ _ (fun _ => rfl) (fun _ _ _ _ ha hb => ha ▸ hb ▸ rfl) h
+
+theorem proper_2 [OFE A] (Φ Ψ : Nat → A → M) (l₁ l₂ : List A)
+    (hlen : l₁.length = l₂.length)
+    (hf : ∀ (k : Nat) (y₁ y₂ : A), l₁[k]? = some y₁ → l₂[k]? = some y₂ → Φ k y₁ ≡ Ψ k y₂) :
+    ([^ op list] k ↦ x ∈ l₁, Φ k x) ≡ ([^ op list] k ↦ x ∈ l₂, Ψ k x) :=
+  gen_proper_2 (· ≡ ·) Φ Ψ l₁ l₂ Equiv.rfl (fun _ _ _ _ => MonoidOps.op_proper) hlen hf
+
+theorem zipIdx (Φ : A × Nat → M) (n : Nat) (l : List A) :
+    ([^ op list] x ∈ l.zipIdx n, Φ x) ≡
+      ([^ op list] k ↦ x ∈ l, Φ (x, n + k)) := by
+  induction l generalizing n with
+  | nil => simp only [nil]; exact Equiv.rfl
+  | cons x xs ih =>
+    simp only [cons, Nat.add_zero]
+    exact MonoidOps.op_proper Equiv.rfl
+      ((ih (n + 1)).trans (congr_forall fun i _ => by simp [Nat.add_assoc, Nat.add_comm 1 i]))
+
+theorem zipIdxInt (Φ : A × Int → M) (n : Int) (l : List A) :
+    ([^ op list] x ∈ Std.List.zipIdxInt l n, Φ x) ≡
+      ([^ op list] k ↦ x ∈ l, Φ (x, n + (k : Int))) := by
+  unfold Std.List.zipIdxInt
+  suffices ∀ m, bigOpL op (fun _ => Φ) (l.mapIdx (fun i v => (v, (i : Int) + m))) ≡
+                bigOpL op (fun i x => Φ (x, m + (i : Int))) l from this n
+  intro m
+  induction l generalizing m with
+  | nil => simp only [List.mapIdx, nil]; exact Equiv.rfl
+  | cons x xs ih =>
+    simp only [List.mapIdx_cons, cons]
+    apply MonoidOps.op_proper
+    · show Φ (x, (0 : Int) + m) ≡ Φ (x, m + (0 : Int))
+      rw [Int.zero_add, Int.add_zero]
+    · rw [show (List.mapIdx (fun i v => (v, ↑(i + 1) + m)) xs) =
+              (List.mapIdx (fun i v => (v, ↑i + (m + 1))) xs) from by
+        apply List.ext_getElem (by simp only [List.length_mapIdx])
+        intro n hn1 hn2
+        simp only [List.getElem_mapIdx]; congr 1; omega]
+      apply (ih (m + 1)).trans
+      apply congr_forall fun i _ => ?_
+      rw [show m + 1 + (i : Int) = m + ((i + 1 : Nat) : Int) from by omega]
+
+theorem sep_zipWith {B C : Type _}
+    (f : A → B → C) (g1 : C → A) (g2 : C → B)
+    (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B)
+    (hg1 : ∀ x y, g1 (f x y) = x)
+    (hg2 : ∀ x y, g2 (f x y) = y)
+    (hlen : l₁.length = l₂.length) :
+    ([^ op list] k ↦ c ∈ List.zipWith f l₁ l₂, op (Φ k (g1 c)) (Ψ k (g2 c))) ≡
+      op ([^ op list] k ↦ x ∈ l₁, Φ k x) ([^ op list] k ↦ x ∈ l₂, Ψ k x) := by
+  induction l₁ generalizing l₂ Φ Ψ with
+  | nil =>
+    cases l₂ with
+    | nil => simp only [List.zipWith_nil_left, nil]; exact Equiv.symm (MonoidOps.op_left_id _)
+    | cons _ _ => simp at hlen
+  | cons x xs ih =>
+    cases l₂ with
+    | nil => simp at hlen
+    | cons y ys =>
+      simp only [List.length_cons, Nat.add_right_cancel_iff] at hlen
+      simp only [List.zipWith_cons_cons, cons, hg1, hg2]
+      refine (MonoidOps.op_congr_r (ih _ _ _ hlen)).trans ?_
+      exact MonoidOps.op_op_swap
+
+/-- Big op over zipped list with separated functions. -/
+theorem sep_zip {B : Type v} (Φ : Nat → A → M) (Ψ : Nat → B → M) (l₁ : List A) (l₂ : List B)
+    (hlen : l₁.length = l₂.length) :
+    ([^ op list] k ↦ xy ∈ l₁.zip l₂, op (Φ k xy.1) (Ψ k xy.2)) ≡
+      op ([^ op list] k ↦ x ∈ l₁, Φ k x) ([^ op list] k ↦ x ∈ l₂, Ψ k x) := by
+  simp only [List.zip]
+  exact sep_zipWith (op := op) _ _ _ _ _ _ _ (fun _ _ => rfl) (fun _ _ => rfl) hlen
+
+variable {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂]
+variable {op₁ : M₁ → M₁ → M₁} {op₂ : M₂ → M₂ → M₂} {unit₁ : M₁} {unit₂ : M₂}
+variable [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂]
+variable {B : Type w}
+
+/-- Monoid homomorphisms distribute over big ops. -/
+theorem hom {R : M₂ → M₂ → Prop} {f : M₁ → M₂}
+    (hom : MonoidHomomorphism op₁ op₂ unit₁ unit₂ R f)
+    (Φ : Nat → B → M₁) (l : List B) :
+    R (f ([^ op₁ list] k ↦ x ∈ l, Φ k x)) ([^ op₂ list] k ↦ x ∈ l, f (Φ k x)) := by
+  induction l generalizing Φ with
+  | nil => simp only [nil]; exact hom.map_unit
+  | cons x xs ih =>
+    simp only [cons]
+    apply hom.rel_trans (hom.homomorphism _ _)
+    exact hom.op_proper (hom.rel_refl _) (ih _)
+
+/-- Weak monoid homomorphisms distribute over non-empty big ops. -/
+theorem hom_weak {R : M₂ → M₂ → Prop} {f : M₁ → M₂}
+    (hom : WeakMonoidHomomorphism op₁ op₂ unit₁ unit₂ R f)
+    (Φ : Nat → B → M₁) (l : List B) (hne : l ≠ []) :
+    R (f ([^ op₁ list] k ↦ x ∈ l, Φ k x)) ([^ op₂ list] k ↦ x ∈ l, f (Φ k x)) := by
+  induction l generalizing Φ with
+  | nil => exact absurd rfl hne
+  | cons x xs ih =>
+    simp only [cons]
+    cases xs with
+    | nil =>
+      simp only [nil]
+      haveI : NonExpansive f := hom.f_ne
+      apply (hom.rel_proper (NonExpansive.eqv (MonoidOps.op_right_id _))
+        (MonoidOps.op_right_id _)).mpr
+      exact hom.rel_refl _
+    | cons y ys =>
+      apply hom.rel_trans (hom.homomorphism _ _)
+      exact hom.op_proper (hom.rel_refl _) (ih _ (List.cons_ne_nil y ys))
+
+end BigOpL
+
+namespace BigOpM
+
+open scoped PartialMap
+
+variable {M : Type u} [OFE M] {op : M → M → M} {unit : M} [MonoidOps op unit]
+variable {M' : Type _ → Type _} {K : Type _} {V : Type _}
+variable [LawfulFiniteMap M' K]
+
+theorem equiv (Φ : K → V → M) (m₁ m₂ : M' V)
+    (h : m₁ ≡ₘ m₂) :
+    ([^ op map] k ↦ x ∈ m₁, Φ k x) ≡ ([^ op map] k ↦ x ∈ m₂, Φ k x) := by
+  simp only [bigOpM]
+  exact BigOpL.perm _ (LawfulFiniteMap.toList_perm_of_get?_eq h)
+
+@[simp] theorem empty (Φ : K → V → M) :
+    ([^ op map] k ↦ x ∈ (∅ : M' V), Φ k x) = unit := by
+  show bigOpL op _ (toList (∅ : M' V)) = unit
+  rw [show toList (K := K) (∅ : M' V) = [] from toList_empty]; rfl
+
+theorem insert (Φ : K → V → M) (m : M' V) (i : K) (x : V) :
+    get? m i = none →
+    ([^ op map] k ↦ v ∈ PartialMap.insert m i x, Φ k v) ≡
+      op (Φ i x) ([^ op map] k ↦ v ∈ m, Φ k v) := by
+  intro hi
+  simp only [bigOpM]
+  exact BigOpL.perm _ (LawfulFiniteMap.toList_insert (v := x) hi)
+
+theorem delete (Φ : K → V → M) (m : M' V) (i : K) (x : V) :
+    get? m i = some x →
+    ([^ op map] k ↦ v ∈ m, Φ k v) ≡
+      op (Φ i x) ([^ op map] k ↦ v ∈ PartialMap.delete m i, Φ k v) := by
+  intro hi
+  apply (BigOpM.equiv Φ m _ (fun k => (LawfulPartialMap.insert_delete_cancel hi k).symm)).trans
+  exact insert Φ (PartialMap.delete m i) _ _ (get?_delete_eq rfl)
+
+theorem gen_proper_2 [DecidableEq K] {A : Type _} {B : Type _} (R : M → M → Prop)
+    (Φ : K → A → M) (Ψ : K → B → M) (m1 : M' A) (m2 : M' B)
+    (hR_sub : ∀ x y, x ≡ y → R x y)
+    (hR_equiv : Equivalence R)
+    (hR_op : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b'))
+    (hfg : ∀ k,
+      match get? m1 k, get? m2 k with
+      | some y1, some y2 => R (Φ k y1) (Ψ k y2)
+      | none, none => True
+      | _, _ => False) :
+    R ([^ op map] k ↦ x ∈ m1, Φ k x) ([^ op map] k ↦ x ∈ m2, Ψ k x) := by
+  let P1 : M' A → Prop := fun m1' => ∀ (m2' : M' B) (Φ' : K → A → M) (Ψ' : K → B → M),
+      (∀ k, match get? m1' k, get? m2' k with
+        | some y1, some y2 => R (Φ' k y1) (Ψ' k y2)
+        | none, none => True
+        | _, _ => False) →
+      R ([^ op map] k ↦ x ∈ m1', Φ' k x) ([^ op map] k ↦ x ∈ m2', Ψ' k x)
+  suffices h : P1 m1 from h m2 Φ Ψ hfg
+  apply LawfulFiniteMap.induction_on (K := K) (P := P1)
+  · intro m₁ m₂ heq hP m2' Φ' Ψ' hfg'
+    apply hR_equiv.trans (hR_sub _ _ (BigOpM.equiv Φ' m₁ m₂ heq).symm)
+    exact hP m2' Φ' Ψ' (fun k => by rw [heq k]; exact hfg' k)
+  · show P1 (∅ : M' A)
+    intro m2' Φ' Ψ' hfg'
+    let P2 : M' B → Prop := fun m2'' => ∀ (Φ'' : K → A → M) (Ψ'' : K → B → M),
+        (∀ k, match get? (∅ : M' A) k, get? m2'' k with
+          | some y1, some y2 => R (Φ'' k y1) (Ψ'' k y2)
+          | none, none => True
+          | _, _ => False) →
+        R ([^ op map] k ↦ x ∈ (∅ : M' A), Φ'' k x) ([^ op map] k ↦ x ∈ m2'', Ψ'' k x)
+    suffices h2 : P2 m2' from h2 Φ' Ψ' hfg'
+    apply LawfulFiniteMap.induction_on (K := K) (P := P2)
+    · intro m₁ m₂ heq hP Φ'' Ψ'' hfg''
+      apply hR_equiv.trans (hP Φ'' Ψ'' (fun k => by rw [heq k]; exact hfg'' k))
+      exact hR_sub _ _ (BigOpM.equiv Ψ'' m₁ m₂ heq)
+    · show P2 (∅ : M' B)
+      intro _ _ _
+      show R ([^ op map] k ↦ x ∈ (∅ : M' A), _) ([^ op map] k ↦ x ∈ (∅ : M' B), _)
+      rw [empty, empty]; exact hR_sub unit unit Equiv.rfl
+    · intro k _ _ _ _ Φ'' Ψ'' hfg''
+      have := hfg'' k
+      rw [show get? (∅ : M' A) k = none from get?_empty k, get?_insert_eq rfl] at this
+      exact this.elim
+  · intro k x1 m1' hm1'k IH m2' Φ' Ψ' hfg'
+    have hfg_k := hfg' k
+    rw [get?_insert_eq rfl] at hfg_k
+    cases hm2k : get? m2' k with
+    | none => rw [hm2k] at hfg_k; cases hfg_k
+    | some x2 =>
+      rw [hm2k] at hfg_k
+      refine hR_equiv.trans (hR_sub _ _ (insert Φ' m1' k x1 hm1'k)) ?_
+      apply hR_equiv.trans _ (hR_sub _ _ (Equiv.symm (delete Ψ' m2' k x2 hm2k)))
+      apply hR_op _ _ _ _ hfg_k
+      apply IH
+      intro k'
+      by_cases hkk' : k = k'
+      · subst hkk'; rw [get?_delete_eq rfl, hm1'k]; trivial
+      · have := hfg' k'; rw [get?_insert_ne hkk'] at this; rwa [get?_delete_ne hkk']
+
+theorem gen_proper {M : Type u} [OFE M] {op : M → M → M} {unit : M} [MonoidOps op unit]
+    (R : M → M → Prop)
+    (Φ Ψ : K → V → M) (m : M' V)
+    (hR_refl : ∀ x, R x x)
+    (hR_op : ∀ a a' b b', R a a' → R b b' → R (op a b) (op a' b'))
+    (hf : ∀ k x, get? m k = some x → R (Φ k x) (Ψ k x)) :
+    R ([^ op map] k ↦ x ∈ m, Φ k x) ([^ op map] k ↦ x ∈ m, Ψ k x) := by
+  simp only [bigOpM]
+  apply BigOpL.gen_proper_2 R _ _ _ _ (hR_refl unit) hR_op rfl
+  intro i x y hx hy; rw [hx] at hy; cases hy
+  exact hf x.1 x.2 (toList_get.mp (List.mem_iff_getElem?.mpr ⟨i, hx⟩))
+
+theorem ext {M : Type u} [OFE M] (op : M → M → M) {unit : M} [MonoidOps op unit]
+    (Φ Ψ : K → V → M) (m : M' V)
+    (hf : ∀ k x, get? m k = some x → Φ k x = Ψ k x) :
+    ([^ op map] k ↦ x ∈ m, Φ k x) = ([^ op map] k ↦ x ∈ m, Ψ k x) :=
+  gen_proper (R := (· = ·)) _ _ _ (fun _ => rfl) (fun _ _ _ _ ha hb => ha ▸ hb ▸ rfl) hf
+
+theorem dist (Φ Ψ : K → V → M) (m : M' V) (n : Nat)
+    (hf : ∀ k x, get? m k = some x → Φ k x ≡{n}≡ Ψ k x) :
+    ([^ op map] k ↦ x ∈ m, Φ k x) ≡{n}≡ ([^ op map] k ↦ x ∈ m, Ψ k x) :=
+  gen_proper (R := (· ≡{n}≡ ·)) _ _ _ (fun _ => Dist.rfl)
+    (fun _ _ _ _ => MonoidOps.op_ne_dist) hf
+
+theorem proper (Φ Ψ : K → V → M) (m : M' V)
+    (hf : ∀ k x, get? m k = some x → Φ k x ≡ Ψ k x) :
+    ([^ op map] k ↦ x ∈ m, Φ k x) ≡ ([^ op map] k ↦ x ∈ m, Ψ k x) :=
+  gen_proper (R := (· ≡ ·)) _ _ _ (fun _ => Equiv.rfl) (fun _ _ _ _ => MonoidOps.op_proper) hf
+
+theorem proper_2 [DecidableEq K] [OFE A] (Φ : K → A → M) (Ψ : K → A → M) (m1 m2 : M' A)
+    (hm : ∀ k, get? m1 k = get? m2 k)
+    (hf : ∀ k y1 y2,
+      get? m1 k = some y1 →
+      get? m2 k = some y2 →
+      y1 ≡ y2 →
+      Φ k y1 ≡ Ψ k y2) :
+    ([^ op map] k ↦ x ∈ m1, Φ k x) ≡ ([^ op map] k ↦ x ∈ m2, Ψ k x) := by
+  apply gen_proper_2 (R := (· ≡ ·)) _ _ _ _ (fun _ _ h => h) equiv_eqv
+    (fun _ _ _ _ => MonoidOps.op_proper)
+  intro k
+  have hlk := hm k
+  cases hm1k : get? m1 k with
+  | none => rw [hm1k] at hlk; rw [← hlk]; trivial
+  | some y1 =>
+    rw [hm1k] at hlk
+    cases hm2k : get? m2 k with
+    | none => rw [hm2k] at hlk; cases hlk
+    | some y2 => rw [hm2k] at hlk; cases hlk; exact hf k y1 y1 hm1k hm2k Equiv.rfl
+
+theorem dist_pointwise (Φ Ψ : K → V → M) (m : M' V) (n : Nat)
+    (hf : ∀ k x, Φ k x ≡{n}≡ Ψ k x) :
+    ([^ op map] k ↦ x ∈ m, Φ k x) ≡{n}≡ ([^ op map] k ↦ x ∈ m, Ψ k x) :=
+    dist _ _ _ _ fun k x _ => hf k x
+
+theorem proper_pointwise (Φ Ψ : K → V → M) (m : M' V)
+    (hf : ∀ k x, Φ k x ≡ Ψ k x) :
+    ([^ op map] k ↦ x ∈ m, Φ k x) ≡ ([^ op map] k ↦ x ∈ m, Ψ k x) :=
+    proper _ _ _ fun k x _ => hf k x
+
+theorem to_list (Φ : K → V → M) (m : M' V) :
+    ([^ op map] k ↦ x ∈ m, Φ k x) ≡
+      ([^ op list] kx ∈ toList (K := K) m, Φ kx.1 kx.2) := by rfl
+
+theorem of_list [DecidableEq K] (Φ : K → V → M) (l : List (K × V))
+    (hnodup : NoDupKeys l) :
+    ([^ op map] k ↦ x ∈ (PartialMap.ofList l : M' V), Φ k x) ≡
+      ([^ op list] kx ∈ l, Φ kx.1 kx.2) := by
+  simp only [bigOpM]
+  exact BigOpL.perm _ (LawfulFiniteMap.toList_ofList hnodup)
+
+theorem singleton (Φ : K → V → M) (i : K) (x : V) :
+    ([^ op map] k ↦ v ∈ ({[i := x]} : M' V), Φ k v) ≡ Φ i x := by
+  rw [show ({[i := x]} : M' V) = PartialMap.insert (∅ : M' V) i x from rfl]
+  apply (insert Φ (∅ : M' V) i x (get?_empty i)).trans
+  rw [empty]; exact MonoidOps.op_right_id _
+
+theorem const_unit [DecidableEq K] (m : M' V) :
+    bigOpM op (fun (_ : K) _ => unit) m ≡ unit := by
+  let P : M' V → Prop := fun m' => bigOpM op (fun (_ : K) (_ : V) => unit) m' ≡ unit
+  show P m; apply LawfulFiniteMap.induction_on (K := K) (P := P)
+  · intro m₁ m₂ heq h
+    refine (BigOpM.equiv _ _ _ heq).symm.trans ?_
+    exact h
+  · show P (∅ : M' V); show _ ≡ _; rw [empty]
+  · intro i x m' hm' IH
+    refine (insert _ _ _ _ hm').trans ?_
+    refine (MonoidOps.op_proper Equiv.rfl IH).trans ?_
+    exact MonoidOps.op_left_id _
+
+theorem map (h : V → B) (Φ : K → B → M) (m : M' V) :
+    ([^ op map] k ↦ x ∈ PartialMap.map h m, Φ k x) ≡
+      ([^ op map] k ↦ v ∈ m, Φ k (h v)) := by
+  simp only [bigOpM]
+  refine (BigOpL.perm _ LawfulFiniteMap.toList_map).trans ?_
+  exact BigOpL.map (op := op) _ _ (toList (K := K) m)
+
+theorem filter_map (h : V → Option V) (Φ : K → V → M) (m : M' V)
+    (hinj : Function.Injective h) :
+    ([^ op map] k ↦ x ∈ PartialMap.filterMap h m, Φ k x) ≡
+      ([^ op map] k ↦ v ∈ m, (h v).elim unit (Φ k)) := by
+  simp only [bigOpM]
+  refine (BigOpL.perm _ (LawfulFiniteMap.toList_filterMap hinj)).trans ?_
+  refine (BigOpL.filter_map (op := op) _ _ _).trans ?_
+  exact BigOpL.congr_forall fun _ kv => by cases hkv : h kv.2 <;> simp [Option.elim, Option.map]
+
+theorem insert_delete (Φ : K → V → M) (m : M' V) (i : K) (x : V) :
+    ([^ op map] k ↦ v ∈ PartialMap.insert m i x, Φ k v) ≡
+      op (Φ i x) ([^ op map] k ↦ v ∈ PartialMap.delete m i, Φ k v) := by
+  refine (BigOpM.equiv _ _ _ fun k => (LawfulPartialMap.insert_delete k).symm).trans ?_
+  exact insert _ _ _ _ (get?_delete_eq rfl)
+
+theorem insert_override (Φ : K → A → M) (m : M' A) (i : K) (x x' : A) :
+    get? m i = some x → Φ i x ≡ Φ i x' →
+    ([^ op map] k ↦ v ∈ PartialMap.insert m i x', Φ k v) ≡
+      ([^ op map] k ↦ v ∈ m, Φ k v) := by
+  intro hi hΦ
+  refine (insert_delete Φ m i x').trans ?_
+  refine (MonoidOps.op_proper hΦ.symm Equiv.rfl).trans ?_
+  exact (delete Φ m i x hi).symm
+
+theorem fn_insert [DecidableEq K] {B : Type w} (g : K → V → B → M) (f : K → B) (m : M' V)
+    (i : K) (x : V) (b : B) (hi : get? m i = none) :
+    ([^ op map] k ↦ y ∈ PartialMap.insert m i x, g k y (if k = i then b else f k)) ≡
+    op (g i x b) ([^ op map] k ↦ y ∈ m, g k y (f k)) := by
+  refine (insert _ m i x hi).trans (MonoidOps.op_proper (by simp) (proper _ _ _ fun k y hk => ?_))
+  simp [show k ≠ i from fun heq => by subst heq; rw [hi] at hk; cases hk]
+
+theorem fn_insert' [DecidableEq K] (f : K → M) (m : M' V) (i : K) (x : V) (P : M)
+    (hi : get? m i = none) :
+    ([^ op map] k ↦ _v ∈ PartialMap.insert m i x, if k = i then P else f k) ≡
+    op P ([^ op map] k ↦ _v ∈ m, f k) := by
+  refine (insert _ m i x hi).trans (MonoidOps.op_proper (by simp) (proper _ _ _ fun k _ hk => ?_))
+  simp [show k ≠ i from fun heq => by subst heq; rw [hi] at hk; cases hk]
+
+theorem filter (φ : K → V → Bool) (Φ : K → V → M) (m : M' V) :
+    ([^ op map] k ↦ x ∈ PartialMap.filter φ m, Φ k x) ≡ ([^ op map] k ↦ x ∈ m, if φ k x then Φ k x else unit) := by
+  unfold bigOpM
+  refine (BigOpL.perm _ LawfulFiniteMap.toList_filter).trans ?_
+  suffices ∀ l : List (K × V),
+      bigOpL op (fun _ kv => Φ kv.1 kv.2) (l.filter (fun kv => φ kv.1 kv.2)) ≡
+      bigOpL op (fun _ kv => if φ kv.1 kv.2 then Φ kv.1 kv.2 else unit) l from this _
+  intro l
+  induction l with
+  | nil => exact Equiv.rfl
+  | cons kv kvs ih =>
+    simp only [List.filter]
+    cases hp : φ kv.1 kv.2 with
+    | false =>
+      simp only [BigOpL.cons, hp]
+      exact Equiv.trans ih (Equiv.symm (MonoidOps.op_left_id _))
+    | true =>
+      simp only [BigOpL.cons, hp, ite_true]
+      exact MonoidOps.op_congr_r ih
+
+theorem union [DecidableEq K] (Φ : K → V → M) (m1 m2 : M' V) (hdisj : m1 ##ₘ m2) :
+    ([^ op map] k ↦ x ∈ m1 ∪ m2, Φ k x) ≡ op ([^ op map] k ↦ x ∈ m1, Φ k x) ([^ op map] k ↦ x ∈ m2, Φ k x) := by
+  let P : M' V → Prop := fun m1 =>
+    PartialMap.disjoint m1 m2 →
+    ([^ op map] k ↦ x ∈ PartialMap.union m1 m2, Φ k x) ≡
+    op ([^ op map] k ↦ x ∈ m1, Φ k x) ([^ op map] k ↦ x ∈ m2, Φ k x)
+  suffices h : P m1 from h hdisj
+  apply LawfulFiniteMap.induction_on (K := K) (P := P)
+  · intro m₁ m₂' heq hP hdisj'
+    have hdisj'' : PartialMap.disjoint m₁ m2 :=
+      fun k hk => hdisj' k ⟨(heq k).symm ▸ hk.1, hk.2⟩
+    have hunion_eq := BigOpM.equiv (op := op) (unit := unit)
+      Φ (PartialMap.union m₁ m2) (PartialMap.union m₂' m2)
+      (fun k => by rw [LawfulPartialMap.get?_union, LawfulPartialMap.get?_union, heq k])
+    refine hunion_eq.symm.trans ?_
+    refine (hP hdisj'').trans ?_
+    exact MonoidOps.op_proper (BigOpM.equiv Φ m₁ m₂' heq) Equiv.rfl
+  · show P (∅ : M' V)
+    intro _; rw [empty]
+    refine Equiv.trans ?_ (MonoidOps.op_left_id _).symm
+    apply BigOpM.equiv Φ _ _
+    intro k; show get? (PartialMap.union (∅ : M' V) m2) k = get? m2 k
+    rw [LawfulPartialMap.get?_union, show get? (∅ : M' V) k = none from get?_empty k]; simp
+  · intro i x m hi_none IH hdisj'
+    have hi_union : get? (PartialMap.union m m2) i = none := by
+      rw [LawfulPartialMap.get?_union_none]
+      refine ⟨hi_none, ?_⟩
+      cases (PartialMap.disjoint_iff _ m2).mp hdisj' i with
+      | inl h => rw [get?_insert_eq rfl] at h; cases h
+      | inr h => exact h
+    have hdisj_inner : PartialMap.disjoint m m2 := fun k ⟨hk1, hk2⟩ => hdisj' k ⟨by
+      by_cases h : i = k
+      · subst h; rw [hi_none] at hk1; cases hk1
+      · rwa [get?_insert_ne h], hk2⟩
+    refine (BigOpM.equiv Φ _ _ fun k => (LawfulPartialMap.union_insert_left k).symm).trans ?_
+    refine (insert Φ (m ∪ m2) i x hi_union).trans ?_
+    refine (MonoidOps.op_congr_r (IH hdisj_inner)).trans ?_
+    refine (MonoidOps.op_assoc _ _ _).symm.trans ?_
+    exact MonoidOps.op_congr_l (insert Φ m i x hi_none).symm
+
+theorem op_distrib (Φ Ψ : K → V → M) (m : M' V) :
+    ([^ op map] k ↦ x ∈ m, op (Φ k x) (Ψ k x)) ≡
+    op ([^ op map] k ↦ x ∈ m, Φ k x) ([^ op map] k ↦ x ∈ m, Ψ k x) := by
+  simp only [bigOpM]; exact BigOpL.op_distrib _ _ _
+
+theorem closed [DecidableEq K] (P : M → Prop) (Φ : K → V → M) (m : M' V)
+    (hproper : ∀ x y, x ≡ y → (P x ↔ P y))
+    (hunit : P unit)
+    (hop : ∀ x y, P x → P y → P (op x y))
+    (hf : ∀ k x, get? m k = some x → P (Φ k x)) :
+    P ([^ op map] k ↦ x ∈ m, Φ k x) := by
+  let Q : M' V → Prop := fun m'' => (∀ k x, get? m'' k = some x → P (Φ k x)) →
+                     P ([^ op map] k ↦ x ∈ m'', Φ k x)
+  suffices h : Q m from h hf
+  apply LawfulFiniteMap.induction_on (K := K) (P := Q)
+  · intro m₁ m₂ heq hQ hf'
+    apply (hproper _ _ (BigOpM.equiv Φ m₁ m₂ heq)).mp
+    exact hQ fun k x hget => hf' k x ((heq k) ▸ hget)
+  · show Q (∅ : M' V)
+    intro _; show P ([^ op map] k ↦ x ∈ (∅ : M' V), Φ k x); rw [empty]; exact hunit
+  · intro k x m'' hm'' IH hf''
+    apply (hproper _ _ (insert Φ m'' k x hm'')).mpr
+    apply hop _ _ (hf'' _ _ (get?_insert_eq rfl))
+    apply IH; intro k' x' hget'
+    by_cases heq : k = k'
+    · subst heq; rw [hget'] at hm''; cases hm''
+    · apply hf'' k' x'
+      rw [get?_insert_ne heq]; exact hget'
+
+-- TODO: kmap and map_seq are skipped for now
+
+theorem sep_zipWith {A : Type _} {B : Type _} {C : Type _}
+    (f : A → B → C) (g1 : C → A) (g2 : C → B)
+    (h1 : K → A → M) (h2 : K → B → M) (m1 : M' A) (m2 : M' B)
+    (hg1 : ∀ x y, g1 (f x y) = x)
+    (hg2 : ∀ x y, g2 (f x y) = y)
+    (hdom : ∀ k, (get? m1 k).isSome ↔ (get? m2 k).isSome) :
+    ([^ op map] k ↦ xy ∈ PartialMap.zipWith f m1 m2, op (h1 k (g1 xy)) (h2 k (g2 xy))) ≡
+    op ([^ op map] k ↦ x ∈ m1, h1 k x) ([^ op map] k ↦ x ∈ m2, h2 k x) := by
+  refine (op_distrib (fun k xy => h1 k (g1 xy)) (fun k xy => h2 k (g2 xy))
+    (PartialMap.zipWith f m1 m2)).trans ?_
+  apply MonoidOps.op_proper
+  · refine (map g1 h1 (PartialMap.zipWith f m1 m2)).symm.trans ?_
+    apply BigOpM.equiv h1 _ _
+    intro k
+    simp only [LawfulPartialMap.get?_map, LawfulPartialMap.get?_zipWith]
+    cases h1k : get? m1 k with
+    | none => simp [Option.bind]
+    | some a =>
+      have := (hdom k).mp (by rw [h1k]; simp)
+      cases h2k : get? m2 k with
+      | none => rw [h2k] at this; simp at this
+      | some b => simp [Option.bind, Option.map, hg1]
+  · refine (map g2 h2 (PartialMap.zipWith f m1 m2)).symm.trans ?_
+    apply BigOpM.equiv h2 _ _
+    intro k
+    simp only [LawfulPartialMap.get?_map, LawfulPartialMap.get?_zipWith]
+    cases h1k : get? m1 k with
+    | none =>
+      simp [Option.bind]
+      cases h2k : get? m2 k with
+      | none => rfl
+      | some b =>
+        have := (hdom k).mpr (by rw [h2k]; simp)
+        rw [h1k] at this; simp at this
+    | some a =>
+      cases h2k : get? m2 k with
+      | none =>
+        have := (hdom k).mp (by rw [h1k]; simp)
+        rw [h2k] at this; simp at this
+      | some b => simp [Option.bind, Option.map, hg2]
+
+theorem sep_zip {A : Type _} {B : Type _}
+    (h1 : K → A → M) (h2 : K → B → M) (m1 : M' A) (m2 : M' B)
+    (hdom : ∀ k, (get? m1 k).isSome ↔ (get? m2 k).isSome) :
+    ([^ op map] k ↦ xy ∈ PartialMap.zip m1 m2, op (h1 k xy.1) (h2 k xy.2)) ≡
+    op ([^ op map] k ↦ x ∈ m1, h1 k x) ([^ op map] k ↦ x ∈ m2, h2 k x) := by
+  simp only [PartialMap.zip]
+  exact sep_zipWith _ _ _ _ _ _ _ (fun _ _ => rfl) (fun _ _ => rfl) hdom
+
+end BigOpM
+
+end Iris.Algebra
diff --git a/src/Iris/Algebra/Monoid.lean b/src/Iris/Algebra/Monoid.lean
new file mode 100644
index 00000000..459b3250
--- /dev/null
+++ b/src/Iris/Algebra/Monoid.lean
@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2026 Zongyuan Liu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zongyuan Liu
+-/
+import Iris.Algebra.OFE
+
+namespace Iris.Algebra
+
+/-! # Monoids for Big Operators
+
+- `Monoid` contains the laws and requires an OFE structure
+- Use explicit `op` and `unit` parameters to support multiple monoids on the same type
+-/
+
+open OFE
+
+/-- A commutative monoid on an OFE, used for big operators.
+The operation must be non-expansive, associative, commutative, and have a left identity. -/
+class MonoidOps {M : Type u} [OFE M] (op : M → M → M) (unit : outParam M) where
+  /-- The operation is non-expansive in both arguments -/
+  op_ne : NonExpansive₂ op
+  /-- Associativity up to equivalence -/
+  op_assoc : ∀ a b c : M, op (op a b) c ≡ op a (op b c)
+  /-- Commutativity up to equivalence -/
+  op_comm : ∀ a b : M, op a b ≡ op b a
+  /-- Left identity up to equivalence -/
+  op_left_id : ∀ a : M, op unit a ≡ a
+
+namespace MonoidOps
+
+attribute [simp] op_left_id
+
+variable {M : Type u} [OFE M] {op : M → M → M}
+
+/-- The operation is proper with respect to equivalence. -/
+theorem op_proper {unit : M} [MonoidOps op unit] {a a' b b' : M}
+    (ha : a ≡ a') (hb : b ≡ b') : op a b ≡ op a' b' := by
+  haveI : NonExpansive₂ op := op_ne
+  exact NonExpansive₂.eqv ha hb
+
+/-- Right identity follows from commutativity and left identity. -/
+@[simp] theorem op_right_id {unit : M} [MonoidOps op unit] (a : M) : op a unit ≡ a :=
+  Equiv.trans (op_comm (unit := unit) a unit) (op_left_id a)
+
+/-- Congruence on the left argument. -/
+theorem op_congr_l {unit : M} [MonoidOps op unit] {a a' b : M} (h : a ≡ a') : op a b ≡ op a' b :=
+  op_proper (unit := unit) h Equiv.rfl
+
+/-- Congruence on the right argument. -/
+theorem op_congr_r {unit : M} [MonoidOps op unit] {a b b' : M} (h : b ≡ b') : op a b ≡ op a b' :=
+  op_proper (unit := unit) Equiv.rfl h
+
+/-- Rearrange `(a * b) * (c * d)` to `(a * c) * (b * d)`. -/
+theorem op_op_swap {unit : M} [MonoidOps op unit] {a b c d : M} :
+    op (op a b) (op c d) ≡ op (op a c) (op b d) :=
+  calc op (op a b) (op c d)
+      _ ≡ op a (op b (op c d)) := op_assoc a b (op c d)
+      _ ≡ op a (op (op b c) d) := op_congr_r (Equiv.symm (op_assoc b c d))
+      _ ≡ op a (op (op c b) d) := op_congr_r (op_congr_l (op_comm b c))
+      _ ≡ op a (op c (op b d)) := op_congr_r (op_assoc c b d)
+      _ ≡ op (op a c) (op b d) := Equiv.symm (op_assoc a c (op b d))
+
+/-- Swap inner elements: `a * (b * c)` to `b * (a * c)`. -/
+theorem op_swap_inner {unit : M} [MonoidOps op unit] {a b c : M} :
+    op a (op b c) ≡ op b (op a c) :=
+  calc op a (op b c)
+      _ ≡ op (op a b) c := Equiv.symm (op_assoc a b c)
+      _ ≡ op (op b a) c := op_congr_l (op_comm a b)
+      _ ≡ op b (op a c) := op_assoc b a c
+
+/-- Non-expansiveness for dist. -/
+theorem op_ne_dist {unit : M} [MonoidOps op unit] {n : Nat} {a a' b b' : M}
+    (ha : a ≡{n}≡ a') (hb : b ≡{n}≡ b') : op a b ≡{n}≡ op a' b' := by
+  haveI : NonExpansive₂ op := op_ne
+  exact NonExpansive₂.ne ha hb
+
+end MonoidOps
+
+/-! ## Monoid Homomorphisms -/
+
+/-- A weak monoid homomorphism preserves the operation but not necessarily the unit. -/
+class WeakMonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂]
+    (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂)
+    [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂]
+    (R : M₂ → M₂ → Prop) (f : M₁ → M₂) where
+  /-- The relation is reflexive -/
+  rel_refl : ∀ a : M₂, R a a
+  /-- The relation is transitive -/
+  rel_trans : ∀ {a b c : M₂}, R a b → R b c → R a c
+  /-- The relation is proper with respect to equivalence -/
+  rel_proper : ∀ {a a' b b' : M₂}, a ≡ a' → b ≡ b' → (R a b ↔ R a' b')
+  /-- The operation is proper with respect to R -/
+  op_proper : ∀ {a a' b b' : M₂}, R a a' → R b b' → R (op₂ a b) (op₂ a' b')
+  /-- The function is non-expansive -/
+  f_ne : NonExpansive f
+  /-- The homomorphism property -/
+  homomorphism : ∀ x y, R (f (op₁ x y)) (op₂ (f x) (f y))
+
+/-- A monoid homomorphism preserves both the operation and the unit. -/
+class MonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂]
+    (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂)
+    [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂]
+    (R : M₂ → M₂ → Prop) (f : M₁ → M₂)
+    extends WeakMonoidHomomorphism op₁ op₂ unit₁ unit₂ R f where
+  /-- The unit is preserved -/
+  map_unit : R (f unit₁) unit₂
+
+end Iris.Algebra
diff --git a/src/Iris/Std/List.lean b/src/Iris/Std/List.lean
new file mode 100644
index 00000000..4f1aa8d8
--- /dev/null
+++ b/src/Iris/Std/List.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Zongyuan Liu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zongyuan Liu
+-/
+
+/-!
+# List Lemmas
+
+This file contains list theory lemmas that are standard properties
+not available in Lean core.
+-/
+
+namespace Iris.Std.List
+
+/-- List equivalence relation parameterized by an element equivalence relation. -/
+inductive Equiv {α : Type _} (R : α → α → Prop) : List α → List α → Prop where
+  | nil : Equiv R [] []
+  | cons {x y : α} {l k : List α} : R x y → Equiv R l k → Equiv R (x :: l) (y :: k)
+
+def zipIdxInt {α : Type _} (l : List α) (n : Int) : List (α × Int) :=
+  l.mapIdx (fun i v => (v, (i : Int) + n))
+
+end Iris.Std.List
diff --git a/src/Iris/Std/PartialMap.lean b/src/Iris/Std/PartialMap.lean
index bb52582b..211cf421 100644
--- a/src/Iris/Std/PartialMap.lean
+++ b/src/Iris/Std/PartialMap.lean
@@ -84,7 +84,7 @@ export UnboundedHeap (notFull_empty notFull_insert_fresh)
 
 namespace PartialMap
 
-variable {K V M} [PartialMap M K]
+variable {K} {V : Type u} {M} [PartialMap M K]
 
 /-- The empty partial map can be written as `∅`. -/
 instance : EmptyCollection (M V) := ⟨PartialMap.empty⟩
@@ -143,7 +143,7 @@ def difference (m₁ m₂ : M V) : M V :=
 def zipWith (f : V → V' → V'') (m₁ : M V) (m₂ : M V') : M V'' :=
   bindAlter (fun k v => (get? m₂ k).bind fun v' => some <| f v v') m₁
 
-def zip (m₁ : M V) (m₂ : M V') : M (V × V') :=
+def zip {V' : Type u} (m₁ : M V) (m₂ : M V') : M (V × V') :=
   zipWith (fun x y => (x, y)) m₁ m₂
 
 /-- Partial maps support the set difference operation `\` via difference. -/
@@ -155,9 +155,7 @@ instance : SDiff (M V) := ⟨difference⟩
 /-- Pointwise equivalence is transitive. -/
 instance instEquivTrans : Trans equiv (@equiv K V M _) equiv := ⟨by simp_all⟩
 
-scoped syntax term " ≡ₘ " term : term
-scoped macro_rules
-  | `($m₁ ≡ₘ $m₂) => `(PartialMap.equiv $m₁ $m₂)
+scoped infix:50 " ≡ₘ " => PartialMap.equiv
 
 /-- Iris notation for singleton map: `{[k := v]}` -/
 scoped syntax "{[" term " := " term "]}" : term
@@ -231,17 +229,9 @@ namespace FiniteMap
 
 variable {K V : Type _} {M : Type _ → Type _} [FiniteMap M K]
 
--- /-- Convert the map to a list of key-value pairs. The order is unspecified. -/
--- def toList (m : M V) : List (K × V) :=
---   mapFold (fun k v acc => (k, v) :: acc) [] m
-
 def mapFold {A : Type _} (f : K → V → A → A) (a : A) (m : M V) : A :=
   List.foldl (fun a' ⟨k, v⟩ => f k v a') a (toList (K := K) m)
 
-/-- Convert a list to a map with sequential natural number keys starting from `start`. -/
-def map_seq [FiniteMap M Nat] (start : Nat) (l : List V) : M V :=
-  PartialMap.ofList (l.mapIdx (fun i v => (start + i, v)))
-
 end FiniteMap
 
 namespace LawfulPartialMap
@@ -268,10 +258,12 @@ theorem get?_insert_delete_same {m : M V} {k k' : K} {v : V} :
   · simp [h, get?_insert_eq]
   · simp [get?_insert_ne h, get?_delete_ne h]
 
-theorem get?_singleton_eq {k k' : K} {v : V} (h : k = k') : get? ({[k := v]} : M V) k' = some v := by
+theorem get?_singleton_eq {k k' : K} {v : V} (h : k = k') :
+  get? ({[k := v]} : M V) k' = some v := by
   simp [PartialMap.singleton, get?_insert_eq h]
 
-theorem get?_singleton_ne {k k' : K} {v : V} (h : k ≠ k') : get? ({[k := v]} : M V) k' = none := by
+theorem get?_singleton_ne {k k' : K} {v : V} (h : k ≠ k') :
+  get? ({[k := v]} : M V) k' = none := by
   simp [PartialMap.singleton, get?_insert_ne h, get?_empty]
 
 theorem get?_singleton [DecidableEq K] {k k' : K} {v : V} :
@@ -298,7 +290,8 @@ theorem disjoint_empty_right (m : M V) : m ##ₘ (∅ : M V) := by
   simp [show get? (∅ : M V) k = none from get?_empty k] at h₂
 
 theorem get?_insert_some_iff [DecidableEq K] {m : M V} {i j : K} {x y : V} :
-    get? (insert m i x) j = some y ↔ (i = j ∧ x = y) ∨ (i ≠ j ∧ get? m j = some y) := by
+    get? (insert m i x) j = some y
+    ↔ (i = j ∧ x = y) ∨ (i ≠ j ∧ get? m j = some y) := by
   rw [get?_insert]; split <;> simp_all
 
 theorem get?_insert_none_iff [DecidableEq K] {m : M V} {i j : K} {x : V} :
@@ -421,7 +414,8 @@ theorem subset_insert {m : M V} {i : K} {x : V} (h : get? m i = none) :
   · rw [get?_insert_ne hik]
     exact hk
 
-theorem delete_subset_delete {m₁ m₂ : M V} {i : K} (h : m₁ ⊆ m₂) : delete m₁ i ⊆ delete m₂ i := by
+theorem delete_subset_delete {m₁ m₂ : M V} {i : K} (h : m₁ ⊆ m₂) :
+  delete m₁ i ⊆ delete m₂ i := by
   intro k v hk
   by_cases hik : i = k
   · rw [get?_delete_eq hik] at hk
@@ -438,9 +432,11 @@ theorem insert_subset_insert {m₁ m₂ : M V} {i : K} {x : V} (h : m₁ ⊆ m
   · rw [get?_insert_ne hik] at hk ⊢
     exact h k v hk
 
-theorem singleton_ne_empty {i : K} {x : V} : ¬({[i := x]} ≡ₘ (∅ : M V)) := insert_ne_empty
+theorem singleton_ne_empty {i : K} {x : V} : ¬({[i := x]} ≡ₘ (∅ : M V))
+  := insert_ne_empty
 
-theorem delete_singleton_eq {i : K} {x : V} : delete ({[i := x]} : M V) i ≡ₘ empty := by
+theorem delete_singleton_eq {i : K} {x : V} :
+  delete ({[i := x]} : M V) i ≡ₘ empty := by
   intro j
   by_cases h : i = j
   · rw [get?_delete_eq h, get?_empty]
@@ -484,7 +480,8 @@ theorem all_insert (P : K → V → Prop) {m : M V} {i : K} {x : V}
     simp [get?_insert_ne hik] at hget
     assumption
 
-theorem all_insert_iff (P : K → V → Prop) {m : M V} {i : K} {x : V} (hi : get? m i = none) :
+theorem all_insert_iff (P : K → V → Prop) {m : M V} {i : K} {x : V}
+    (hi : get? m i = none) :
     (PartialMap.all P (insert m i x) ↔ P i x ∧ PartialMap.all P m) :=
   ⟨fun h => ⟨all_insert_of_all P h, all_of_all_insert P hi h⟩,
    fun ⟨hpix, h⟩ => all_insert P hpix h⟩
@@ -607,7 +604,8 @@ theorem union_insert_left {m₁ m₂ : M V} {i : K} {x : V} :
   intro k
   by_cases hik : i = k
   · subst hik
-    cases h : get? m₂ i <;> simp [get?_insert_eq rfl, PartialMap.union, get?_merge, Option.merge, h]
+    cases h : get? m₂ i <;> simp [get?_insert_eq rfl, PartialMap.union
+                                , get?_merge, Option.merge, h]
   · simp [get?_insert_ne hik, PartialMap.union, get?_merge]
 
 theorem get?_map {f : V → V'} {m : M V} {k : K} :
@@ -626,11 +624,13 @@ theorem get?_filterMap {f : V → Option V} {m : M V} {k : K} :
   simp [filterMap, get?_bindAlter]
 
 theorem get?_filter {φ : K → V → Bool} {m : M V} {k : K} :
-    get? (filter φ m) k = (get? m k).bind (fun v => if φ k v then some v else none) := by
+    get? (filter φ m) k
+    = (get? m k).bind (fun v => if φ k v then some v else none) := by
   simp [Option.bind, filter, get?_bindAlter]
 
 theorem get?_zipWith {f : V → V' → V''} {m₁ : M V} {m₂ : M V'} {k : K} :
-    get? (zipWith f m₁ m₂) k = (get? m₁ k).bind fun v₁ => (get? m₂ k).map fun v₂ => f v₁ v₂ := by
+    get? (zipWith f m₁ m₂) k
+    = (get? m₁ k).bind fun v₁ => (get? m₂ k).map fun v₂ => f v₁ v₂ := by
   simp [zipWith, get?_bindAlter]
   cases h1 : get? m₁ k <;> cases h2 : get? m₂ k <;> simp [Option.bind]
 
@@ -639,21 +639,24 @@ theorem get?_zip {m₁ : M V} {m₂ : M V'} {k : K} :
   simp [zip, zipWith, get?_bindAlter]
   cases h1 : get? m₁ k <;> cases h2 : get? m₂ k <;> simp [Option.bind]
 
-theorem map_zipWith_right {f : V → V' → V''} {g : V''' → V'} {m₁ : M V} {m₂ : M V'''} :
+theorem map_zipWith_right {f : V → V' → V''} {g : V''' → V'}
+    {m₁ : M V} {m₂ : M V'''} :
     PartialMap.map (fun (v, w) => f v (g w)) (zip m₁ m₂) ≡ₘ
       zipWith f m₁ (PartialMap.map g m₂) := by
   intro k
   simp [get?_map, get?_zip, get?_zipWith]
   cases get? m₁ k <;> cases get? m₂ k <;> simp [Option.bind, Option.map]
 
-theorem map_zipWith_left {f : V → V' → V''} {g : V''' → V} {m₁ : M V'''} {m₂ : M V'} :
+theorem map_zipWith_left {f : V → V' → V''} {g : V''' → V}
+    {m₁ : M V'''} {m₂ : M V'} :
     PartialMap.map (fun (w, v) => f (g w) v) (zip m₁ m₂) ≡ₘ
       zipWith f (PartialMap.map g m₁) m₂ := by
   intro k
   simp [get?_map, get?_zip, get?_zipWith]
   cases get? m₁ k <;> cases get? m₂ k <;> simp [Option.bind, Option.map]
 
-theorem zipWith_insert {f : V → V' → V''} {m₁ : M V} {m₂ : M V'} {k : K} {v : V} {v' : V'} :
+theorem zipWith_insert {f : V → V' → V''} {m₁ : M V} {m₂ : M V'} {k : K}
+    {v : V} {v' : V'} :
     zipWith f (insert m₁ k v) (insert m₂ k v') ≡ₘ
       insert (zipWith f m₁ m₂) k (f v v') := by
   intro k'
@@ -675,10 +678,11 @@ theorem zipWith_comm {f : V → V' → V''} {m₁ : M V} {m₂ : M V'} :
     zipWith f m₁ m₂ ≡ₘ zipWith f m₁ m₂ := by
   intro _; intro _; rfl
 
--- -- FIXME: universe issue
--- theorem zip_comm {m₁ : M V} {m₂ : M V'} :
---     PartialMap.map Prod.swap (zip m₁ m₂) ≡ₘ zip m₂ m₁ := by
---   sorry
+theorem zip_comm {m₁ : M V} {m₂ : M V'} :
+    PartialMap.map Prod.swap (zip m₁ m₂) ≡ₘ zip m₂ m₁ := by
+  intro k
+  simp [get?_map, get?_zip]
+  cases get? m₁ k <;> cases get? m₂ k <;> simp [Option.bind, Option.map]
 
 theorem zip_map {f : V → V'} {g : V → V''} {m : M V} :
     zip (PartialMap.map f m) (PartialMap.map g m) ≡ₘ
@@ -710,22 +714,29 @@ theorem zip_empty_right {m : M V} :
   simp only [zip, zipWith, get?_bindAlter, get?_empty, Option.bind]
   cases h : get? m k <;> simp
 
--- -- FIXME: universe issue
--- theorem zip_insert {m₁ : M V} {m₂ : M V'} {k : K} {v : V} {v' : V'} :
---     zip (insert m₁ k v) (insert m₂ k v') ≡ₘ insert (zip m₁ m₂) k (v, v') := by
---   sorry
+theorem zip_insert {m₁ : M V} {m₂ : M V'} {k : K} {v : V} {v' : V'} :
+    zip (insert m₁ k v) (insert m₂ k v') ≡ₘ insert (zip m₁ m₂) k (v, v') := by
+  intro k'
+  by_cases h : k = k'
+  · subst h
+    simp [get?_zip, get?_insert_eq rfl]
+  · simp [get?_zip, get?_insert_ne h]
 
--- FIXME: universe issue
--- theorem zip_delete {m₁ : M V} {m₂ : M V'} {k : K} :
---     zip (delete m₁ k) (delete m₂ k) ≡ₘ delete (zip m₁ m₂) k := by
---   sorry
+theorem zip_delete {m₁ : M V} {m₂ : M V'} {k : K} :
+    zip (delete m₁ k) (delete m₂ k) ≡ₘ delete (zip m₁ m₂) k := by
+  intro k'
+  by_cases h : k = k'
+  · subst h
+    simp [get?_zip, get?_delete_eq rfl]
+  · simp [get?_zip, get?_delete_ne h]
 
 theorem isSome_zip {m₁ : M V} {m₂ : M V'} {k : K} :
     (get? (zip m₁ m₂) k).isSome ↔ (get? m₁ k).isSome ∧ (get? m₂ k).isSome := by
   rw [get?_zip]
   cases h1 : get? m₁ k <;> cases h2 : get? m₂ k <;> simp
 
-theorem ofList_cons {L : List (K × V)} : ofList (M := M) ((k, v) :: L) = insert (ofList L) k v :=
+theorem ofList_cons {L : List (K × V)} :
+  ofList (M := M) ((k, v) :: L) = insert (ofList L) k v :=
   rfl
 
 theorem noDupKeys_cons {L : List (K × V)} : NoDupKeys (h :: L) → NoDupKeys L := by
@@ -786,8 +797,13 @@ variable {K V : Type _} {M : Type _ → Type _} [LawfulFiniteMap M K]
 
 open FiniteMap LawfulFiniteMap PartialMap LawfulPartialMap
 
+theorem mapFold_empty {f : K → V → A → A} :
+  mapFold f a (∅ : M V) = a := by
+  simp only [mapFold, Std.toList, toList_empty (M := M) (K := K) (V := V)]
+  rfl
+
 -- TODO: These should be theorems
--- mapFold_empty {f : K → V → A → A} : mapFold f a ∅ = a
+-- NOTE: This one is not provable without P respecting equivalence
 -- mapFold_ind {P : M A → Prop}:
 --   P ∅ →
 --   (∀ i x m,
@@ -799,7 +815,8 @@ open FiniteMap LawfulFiniteMap PartialMap LawfulPartialMap
 --     P (insert m i x)) →
 --   ∀ m, P m
 
-theorem toList_get?_none {m : M V} : (∀ v, (k, v) ∉ toList (K := K) m) ↔ get? m k = none := by
+theorem toList_get?_none {m : M V} :
+  (∀ v, (k, v) ∉ toList (K := K) m) ↔ get? m k = none := by
   constructor
   · intro Hn
     refine Option.eq_none_iff_forall_ne_some.mpr ?_
@@ -823,6 +840,26 @@ theorem ofList_toList [DecidableEq K] {m : M V} :
     cases h ▸ toList_get.mp Hk
   · exact get?_ofList_some (toList_get.mpr h) toList_noDupKeys
 
+@[elab_as_elim]
+theorem induction_on [DecidableEq K] {P : M V → Prop}
+    (hequiv : ∀ m₁ m₂, PartialMap.equiv m₁ m₂ → P m₁ → P m₂)
+    (hemp : P PartialMap.empty)
+    (hins : ∀ i x m, get? m i = none → P m → P (PartialMap.insert m i x))
+    (m : M V) : P m := by
+  apply hequiv _ _ ofList_toList
+  suffices ∀ l, NoDupKeys l → P (ofList l) from this _ toList_noDupKeys
+  intro l hnd
+  induction l with
+  | nil => simpa [ofList] using hemp
+  | cons kv rest ih =>
+    rw [ofList_cons]
+    apply hins kv.1 kv.2
+    · refine get?_ofList_none (M := M) ?_ (noDupKeys_cons hnd)
+      intro ⟨v, hv⟩
+      exact (List.nodup_cons.mp hnd).1
+        (List.mem_map_of_mem (f := Prod.fst) (a := (kv.1, v)) hv)
+    · exact ih (noDupKeys_cons hnd)
+
 theorem mem_of_mem_ofList [DecidableEq K] {l : List (K × V)} {i : K} {x : V}
     (H : get? (ofList l : M V) i = some x) : (i, x) ∈ l := by
   induction l
@@ -1043,5 +1080,445 @@ theorem toList_zip {m₁ : M V} {m₂ : M V'} :
 
 end LawfulFiniteMap
 
+/-- Remap keys in a map from one key type to another. -/
+def kmap {K1 K2 : Type _} {V : Type _} {M1 : Type _ → Type _} {M2 : Type _ → Type _}
+    [LawfulFiniteMap M1 K1] [LawfulFiniteMap M2 K2]
+    (f : K1 → K2) (m : M1 V) : M2 V :=
+  PartialMap.ofList ((toList (K := K1) m).map (Prod.map f id))
+
+theorem no_dup_keys_prod_map {K1 K2 : Type _} {V : Type _}
+  {M1 : Type _ → Type _} {M2 : Type _ → Type _}
+  [DecidableEq K1] [DecidableEq K2]
+  [LawfulFiniteMap M1 K1] [LawfulFiniteMap M2 K2]
+  {m : M1 V} {f : K1 → K2} (hinj : Function.Injective f) {g : V → V} :
+  NoDupKeys (toList (K := K1) m)
+    → NoDupKeys (List.map (Prod.map f g) (toList m)) := by
+  simp only [NoDupKeys]
+  rw [List.map_map]
+  intro H
+  apply FromMathlib.Nodup.map_on
+  · rintro ⟨k, x⟩ Hin ⟨k', x'⟩ Hin'; dsimp; intro heq
+    rw [hinj heq]; rw [hinj heq] at Hin
+    rw [LawfulPartialMap.noDupKeys_inj LawfulFiniteMap.toList_noDupKeys Hin Hin']
+  · apply FromMathlib.List.Nodup.of_map _ H
+
+namespace Kmap
+
+open PartialMap LawfulPartialMap LawfulFiniteMap
+
+variable {K1 K2 : Type _} {V : Type _} {M1 : Type _ → Type _} {M2 : Type _ → Type _}
+variable [DecidableEq K1] [DecidableEq K2]
+variable [LawfulFiniteMap M1 K1] [LawfulFiniteMap M2 K2]
+variable (f : K1 → K2)
+
+theorem get?_kmap_some (hinj : Function.Injective f) (m : M1 V) (j : K2) (x : V) :
+    get? (kmap (M2 := M2) f m) j = some x ↔ ∃ i, j = f i ∧ get? m i = some x := by
+  constructor
+  · intro h
+    have ⟨a, heq1, heq2⟩ : ∃ a, (a, x) ∈ toList m ∧ f a = j := by
+      have this := mem_of_mem_ofList h
+      rw [List.mem_map] at this
+      obtain ⟨⟨a, b⟩, hin, heq⟩ := this; dsimp at heq; rw [Prod.mk.injEq] at heq
+      exists a; rw [<-heq.right]; apply And.intro; assumption
+      exact heq.left
+    exists a; rw [heq2, <-h]; apply And.intro; simp
+    simp only [kmap]
+    rw [get?_ofList_some (v := x)]
+    · rw [<-toList_get]; exact heq1
+    · rw [List.mem_map]
+      exists ⟨a, x⟩; apply And.intro; assumption
+      dsimp; rw [<-heq2]
+    · apply no_dup_keys_prod_map (M2 := M2) hinj
+      apply toList_noDupKeys
+  · intro ⟨i, heq, hget⟩
+    subst heq; rw [<-hget]
+    simp only [kmap]
+    rw [get?_ofList_some (v := x)]; symm; assumption
+    · rw [List.mem_map]
+      exists ⟨i, x⟩; apply And.intro;
+        apply toList_get.mpr; assumption
+      dsimp
+    · apply no_dup_keys_prod_map (M2 := M2) hinj
+      apply toList_noDupKeys
+
+theorem get?_kmap_isSome (hinj : Function.Injective f) (m : M1 V) (j : K2) :
+    (get? (kmap (M2 := M2) f m) j).isSome ↔ ∃ i, j = f i ∧ (get? m i).isSome := by
+  constructor
+  · intro h
+    have ⟨a, h⟩ := Option.isSome_iff_exists.mp h
+    rw [get?_kmap_some f hinj m j] at h
+    obtain ⟨i, heq1, heq2⟩ := h
+    exists i; apply And.intro; assumption
+    rw [Option.isSome_iff_exists]
+    exists a
+  · intro ⟨i, heq, h⟩
+    have ⟨a, h⟩ := Option.isSome_iff_exists.mp h
+    rw [Option.isSome_iff_exists]
+    exists a
+    rw [get?_kmap_some f hinj m j]
+    exists i
+
+theorem get?_kmap_none (hinj : Function.Injective f) (m : M1 V) (j : K2) :
+    get? (kmap (M2 := M2) f m) j = none ↔ ∀ i, j = f i → get? m i = none := by
+  constructor
+  · intro g i heq
+    rw [<-toList_get?_none]
+    intro v h
+    rw [<-toList_get?_none] at g
+    apply g v
+    rw [heq]
+    apply toList_get.mpr
+    rw [get?_kmap_some _ hinj]
+    exists i; apply And.intro; rfl
+    apply toList_get.mp; assumption
+  · intro g
+    rw [<-toList_get?_none]
+    intro v h
+    rw [toList_get, get?_kmap_some _ hinj] at h
+    obtain ⟨i, heq, hget⟩ := h
+    rw [g i heq] at hget
+    simp at hget
+
+theorem get?_kmap (hinj : Function.Injective f) (m : M1 V) (i : K1) :
+    get? (kmap (M2 := M2) f m) (f i) = get? m i := by
+  cases h : get? m i
+  · rw [get?_kmap_none f hinj]
+    intro i' heq
+    rw [<-hinj heq]
+    assumption
+  · rw [get?_kmap_some f hinj, <-h]
+    exists i
+
+theorem kmap_empty (hinj : Function.Injective f) :
+  kmap (M1 := M1) (M2 := M2) f (∅ : M1 V) ≡ₘ ∅ := by
+  rw [eq_empty_iff]
+  intro k
+  rw [get?_kmap_none _ hinj]
+  intro i heq
+  exact get?_empty i
+
+theorem kmap_injective (hinj : Function.Injective f) (m1 m2 : M1 V) :
+    kmap (M2 := M2) f m1 ≡ₘ kmap (M2 := M2) f m2
+    → m1 ≡ₘ m2 := by
+  intro heq
+  apply induction_on (K := K1) (P := fun m1 => ∀ m2,
+    kmap (M2 := M2) f m1 ≡ₘ kmap (M2 := M2) f m2
+    → m1 ≡ₘ m2)
+  · intro m₁ m₂ heqm hP m2' heq'
+    intro k
+    specialize (heq' (f k))
+    rw [get?_kmap _ hinj, get?_kmap _ hinj] at heq'
+    rw [<-heq']
+  · intro m2' heq'
+    intro k'
+    specialize (heq' (f k'))
+    rw [get?_kmap _ hinj, get?_kmap _ hinj] at heq'
+    exact heq'
+  · intro k x m' hm' IH m2' heq'
+    intro k'
+    specialize (heq' (f k'))
+    rw [get?_kmap _ hinj, get?_kmap _ hinj] at heq'
+    exact heq'
+  · exact heq
+
+theorem kmap_insert (hinj : Function.Injective f) (m : M1 V) (k : K1) (x : V) :
+    get? m k = none →
+    kmap f (insert m k x) ≡ₘ insert (kmap (M2 := M2) f m) (f k) x := by
+  intro hk j
+  by_cases h : f k = j
+  · subst h
+    rw [get?_insert_eq rfl, get?_kmap _ hinj, get?_insert_eq rfl]
+  · rw [get?_insert_ne h]
+    cases g : get? (kmap (M2 := M2) f (insert m k x)) j
+    · rw [get?_kmap_none _ hinj] at g
+      symm
+      rw [get?_kmap_none _ hinj]
+      intro i heq
+      specialize g i heq
+      rw [heq] at h
+      rw [get?_insert_ne] at g; assumption
+      intro j
+      apply h
+      rw [j]
+    · rw [get?_kmap_some _ hinj] at g
+      obtain ⟨i, heq, hget⟩ := g
+      rw [heq] at h
+      symm
+      rw [get?_kmap_some _ hinj]
+      exists i; apply And.intro; assumption
+      rw [get?_insert_ne] at hget; assumption
+      intro j
+      apply h
+      rw [j]
+
+  theorem kmap_compose [DecidableEq K3] [LawfulFiniteMap M3 K3]
+    (hinj_f : Function.Injective f) (g : K2 → K3)
+    (hinj_g : Function.Injective g) (m : M1 V) :
+    kmap g (kmap (M2 := M2) f m) ≡ₘ kmap (M2 := M3) (g ∘ f) m := by
+  intro k
+  have hinj_fg : Function.Injective (g ∘ f) := Function.Injective.comp hinj_g hinj_f
+  cases h : get? (kmap g (M2 := M3) (kmap (M2 := M2) f m)) k
+  · symm
+    rw [get?_kmap_none _ hinj_fg]
+    intro i heq
+    rw [get?_kmap_none _ hinj_g] at h
+    specialize (h (f i) heq)
+    rw [get?_kmap_none _ hinj_f] at h
+    apply h _ rfl
+  · symm
+    rw [get?_kmap_some _ hinj_fg]
+    rw [get?_kmap_some _ hinj_g] at h
+    obtain ⟨j, heq_j, h⟩ := h
+    rw [get?_kmap_some _ hinj_f] at h
+    obtain ⟨i, heq_i, h⟩ := h
+    exists i; apply And.intro; simp only [heq_i, heq_j, Function.comp_apply]
+    assumption
+
+  theorem kmap_id {m : M1 V} : kmap (K2 := K1) (M2 := M1) id m ≡ₘ m := by
+    intro k
+    simp only [kmap]
+    rw [Prod.map_id, List.map_id]
+    apply ofList_toList (M := M1) (m := m) k
+
+  theorem kmap_union (hinj : Function.Injective f)
+    (m₁ m₂ : M1 V) :
+    kmap f (m₁ ∪ m₂) ≡ₘ (kmap (M2 := M2) f m₁) ∪ (kmap f m₂) := by
+    intro k
+    simp only [Union.union]
+    rw [get?_union (m₁ := kmap f m₁) (m₂ := kmap f m₂) (k := k)]
+    cases h : get? (kmap (M2 := M2) f (union m₁ m₂)) k
+    · symm
+      rw [Option.orElse_eq_or, Option.or_eq_none_iff]
+      rw [get?_kmap_none _ hinj, get?_kmap_none _ hinj]
+      rw [get?_kmap_none _ hinj] at h
+      apply And.intro
+      · intro i heq
+        specialize h i heq
+        rw [get?_union (m₁ := m₁) (m₂ := m₂) (k := i)] at h
+        rw [Option.orElse_eq_or, Option.or_eq_none_iff] at h
+        apply h.left
+      · intro i heq
+        specialize h i heq
+        rw [get?_union (m₁ := m₁) (m₂ := m₂) (k := i)] at h
+        rw [Option.orElse_eq_or, Option.or_eq_none_iff] at h
+        apply h.right
+    · symm
+      rw [Option.orElse_eq_or, Option.or_eq_some_iff]
+      rw [get?_kmap_some _ hinj] at h
+      obtain ⟨i, heq, h⟩ := h
+      rw [get?_union (m₁ := m₁) (m₂ := m₂) (k := i)] at h
+      rw [Option.orElse_eq_or, Option.or_eq_some_iff] at h
+      cases h with
+      | inl h =>
+        left
+        rw [heq, get?_kmap_some _ hinj]
+        exists i
+      | inr h =>
+        right
+        rw [heq, get?_kmap_some _ hinj, get?_kmap_none _ hinj]
+        apply And.intro
+        · intro j heq'
+          rw [<-hinj heq', h.left]
+        · exists i; apply And.intro; simp
+          exact h.right
+
+  theorem kmap_delete (hinj : Function.Injective f)
+    (i : K1) (m : M1 V) :
+    kmap f (delete m i) ≡ₘ delete (kmap (M2 := M2) f m) (f i) := by
+    intro j
+    by_cases h : f i = j
+    · subst h
+      rw [get?_delete_eq rfl, get?_kmap_none _ hinj]
+      intro k heq
+      rw [hinj heq, get?_delete_eq rfl]
+    · rw [get?_delete_ne h]
+      cases g : get? (kmap (M2 := M2) f m) j
+      · rw [get?_kmap_none _ hinj] at g
+        rw [get?_kmap_none _ hinj]
+        intro k heq
+        rw [get?_delete_ne]
+        · apply g _ heq
+        · intro c; rw [heq, c] at h; apply h rfl
+      · rw [get?_kmap_some _ hinj] at g
+        obtain ⟨k, heq, g⟩ := g
+        rw [get?_kmap_some _ hinj]
+        exists k; apply And.intro; assumption
+        rw [get?_delete_ne, g]
+        intro c; rw [heq, c] at h; apply h rfl
+
+  theorem kmap_singleton (hinj : Function.Injective f) (k : K1) (x : V) :
+    kmap (M2 := M2) f (singleton (M := M1) k x) ≡ₘ singleton (f k) x := by
+    intro j
+    by_cases h : f k = j
+    · subst h
+      rw [get?_kmap _ hinj, get?_singleton_eq rfl, get?_singleton_eq rfl]
+    · rw [get?_singleton_ne h, get?_kmap_none _ hinj]
+      intro i heq
+      rw [get?_singleton_ne]
+      intro c; rw [heq, c] at h; apply h rfl
+
+  theorem kmap_mem (hinj : Function.Injective f) (m : M1 V) (k : K1) :
+    k ∈ m ↔ f k ∈ kmap (M2 := M2) f m := by
+    simp only [Membership.mem]
+    rw [get?_kmap_isSome _ hinj]
+    apply Iff.intro
+    · intro h
+      exists k
+    · intro h
+      obtain ⟨i, heq, hget⟩ := h
+      rw [hinj heq]
+      assumption
+
+  theorem kmap_dom (hinj : Function.Injective f) (m : M1 V) :
+    dom (kmap (M2 := M2) f m) = (fun k => ∃ j, k = f j ∧ dom m j) := by
+    ext j
+    simp only [dom]
+    rw [get?_kmap_isSome _ hinj]
+
+  theorem kmap_bindAlter (hinj : Function.Injective f) (g : K2 → V → Option V') (m : M1 V) :
+    kmap f (bindAlter (g ∘ f) m) ≡ₘ bindAlter g (kmap (M2 := M2) f m) := by
+    intro k
+    rw [get?_bindAlter]
+    cases h : get? (kmap (M2 := M2) f m) k
+    · rw [Option.bind_none, get?_kmap_none _ hinj]
+      intro i heq
+      rw [get?_kmap_none _ hinj] at h
+      rw [get?_bindAlter]
+      rw [Option.bind_eq_none_iff]
+      intro a g
+      specialize h i heq
+      cases h ▸ g
+    · rw [Option.bind_some]
+      rw [get?_kmap_some _ hinj] at h
+      obtain ⟨i, heq, h⟩ := h
+      rw [heq, get?_kmap _ hinj]
+      rw [get?_bindAlter, h, Option.bind_some]
+      rfl
+
+  theorem kmap_map (hinj : Function.Injective f)
+    (g : V → V') (m : M1 V) :
+    kmap f (map g m) ≡ₘ map g (kmap (M2 := M2) f m) := by
+    intro k
+    simp only [map]
+    rw [<-kmap_bindAlter (M2 := M2) _ hinj (fun k v => some (g v)) m k]
+    rfl
+
+  theorem kmap_filterMap (hinj : Function.Injective f)
+    (g : V → Option V) (m : M1 V) :
+    kmap f (filterMap g m) ≡ₘ filterMap g (kmap (M2 := M2) f m) := by
+    intro k
+    simp only [filterMap]
+    rw [<-kmap_bindAlter (M2 := M2) _ hinj (fun k v => g v) m k]
+    rfl
+
+  theorem kmap_filter (hinj : Function.Injective f) (φ : K2 → V → Bool)  (m : M1 V) :
+    kmap f (filter (fun k v => φ (f k) v) m) ≡ₘ filter φ (kmap (M2 := M2) f m) := by
+    intro k
+    simp only [filter]
+    rw [<-kmap_bindAlter (M2 := M2) _ hinj (fun k v => if φ k v = true then some v else none) m k]
+    rfl
+
+  theorem kmap_disjoint (hinj : Function.Injective f) (m₁ m₂ : M1 V) :
+    (kmap (M2 := M2) f m₁) ##ₘ (kmap f m₂) ↔ m₁ ##ₘ m₂ := by
+    simp only [PartialMap.disjoint]
+    apply Iff.intro
+    · intro h i heq
+      apply h (f i)
+      rw [get?_kmap_isSome _ hinj, get?_kmap_isSome _ hinj]
+      apply And.intro
+      · exists i; apply And.intro; rfl
+        rw [heq.left]
+      · exists i; apply And.intro; rfl
+        rw [heq.right]
+    · intro h k heq
+      rw [get?_kmap_isSome _ hinj, get?_kmap_isSome _ hinj] at heq
+      obtain ⟨i, heq1, h1⟩ := heq.left
+      obtain ⟨j, heq2, h2⟩ := heq.right
+      cases (hinj (heq1 ▸ heq2))
+      apply h i
+      rw [h1, h2]; simp
+
+  theorem kmap_submap (hinj : Function.Injective f) (m₁ m₂ : M1 V) :
+    (kmap (M2 := M2) f m₁) ⊆ (kmap f m₂) ↔ m₁ ⊆ m₂ := by
+    simp only [HasSubset.Subset]
+    apply Iff.intro
+    · intro h i v hget
+      specialize h (f i) v
+      rw [get?_kmap_some _ hinj, get?_kmap_some _ hinj] at h
+      have hyp : ∃ i_1, f i = f i_1 ∧ get? m₁ i_1 = some v := by
+        exists i
+      obtain ⟨j, heq, hget⟩ := h hyp
+      rw [hinj heq]
+      exact hget
+    · intro h i v hget
+      rw [get?_kmap_some _ hinj]
+      rw [get?_kmap_some _ hinj] at hget
+      obtain ⟨j, heq, hget⟩ := hget
+      exists j; apply And.intro; assumption
+      apply h _ _ hget
+
+  theorem kmap_all (hinj : Function.Injective f) (P : K2 → V → Prop) (m : M1 V) :
+    all (P ∘ f) m ↔ all P (kmap (M2 := M2) f m) := by
+    apply Iff.intro
+    · intro h i v
+      rw [get?_kmap_some _ hinj]
+      intro h
+      obtain ⟨j, heq, hget⟩ := h
+      rw [heq]; apply h _ _ hget
+    · intro h i v
+      specialize h (f i) v
+      rw [get?_kmap _ hinj] at h
+      apply h
+
+  theorem kmap_zipWith (hinj : Function.Injective f)
+    (h : V → V' → V'')
+    (m₁ : M1 V) (m₂ : M1 V') :
+    kmap (M2 := M2) f (zipWith h m₁ m₂)
+    ≡ₘ zipWith h (kmap (M2 := M2) f m₁) (kmap (M2 := M2) f m₂) := by
+    intro k
+    simp only [zipWith]
+    rw [<-kmap_bindAlter (M2 := M2) _ hinj _ m₁ k]
+    congr
+    ext j v x
+    rw [Function.comp_apply]
+    rw [get?_kmap _ hinj]
+
+  theorem kmap_difference (hinj : Function.Injective f) (m₁ m₂ : M1 V) :
+    kmap f (m₁ \ m₂) ≡ₘ (kmap (M2 := M2) f m₁) \ (kmap f m₂) := by
+    intro k
+    rw [get?_difference (m₁ := kmap f m₁) (m₂ := kmap f m₂) (k := k)]
+    cases h : get? (kmap (M2 := M2) f (m₁ \ m₂)) k
+    · rw [get?_kmap_none _ hinj] at h
+      symm
+      simp only [ite_eq_left_iff, Bool.not_eq_true, Option.isSome_eq_false_iff,
+        Option.isNone_iff_eq_none]
+      intro g
+      rw [get?_kmap_none _ hinj]
+      intro i heq
+      specialize h i heq
+      rw [get?_kmap_none _ hinj] at g
+      specialize g i heq
+      rw [get?_difference (m₁ := m₁) (m₂ := m₂) (k := i)] at h
+      rw [g, Option.isSome_none] at h
+      simp only [Bool.false_eq_true] at h
+      apply h
+    · rw [get?_kmap_some _ hinj] at h
+      symm
+      simp only [Option.ite_none_left_eq_some, Bool.not_eq_true
+        , Option.isSome_eq_false_iff, Option.isNone_iff_eq_none]
+      obtain ⟨i, heq, h⟩ := h
+      rw [get?_difference (m₁ := m₁) (m₂ := m₂) (k := i)] at h
+      rw [Option.ite_none_left_eq_some] at h
+      rw [get?_kmap_none _ hinj, get?_kmap_some _ hinj, heq]
+      simp only [Bool.not_eq_true, Option.isSome_eq_false_iff
+        , Option.isNone_iff_eq_none] at h
+      apply And.intro
+      · intro j heq
+        rw [<-hinj heq]
+        rw [h.left]
+      · exists i; apply And.intro; rfl
+        rw [h.right]
+
+end Kmap
 
 end Iris.Std