diff --git a/PORTING.md b/PORTING.md
index da5be018..610ed0ce 100644
--- a/PORTING.md
+++ b/PORTING.md
@@ -16,8 +16,8 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] CMRA
   - [ ] Updates
   - [ ] Functors
-- [ ] `big_op.v`
-  - TBD (Zongyuan?)
+- [x] `big_op.v`
+  - [x] `bigOpL`, `bigOpM` definitions and lemmas
 - [ ] `cmra.v`
   - [x] Lemmas
   - [ ] Total CMRA construction
@@ -72,7 +72,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`
@@ -199,7 +199,8 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `algebra.v`
 - `ascii.v`
 - [x] `bi.v`
-- [ ] `big_op.v`
+- [x] `big_op.v`
+  - [x] `big_sepL`, `big_sepM` definitions and lemmas
 - [ ] `cmra.v`
 - [x] `derived_connectives.v`
 - [ ] `derived_laws.v`
diff --git a/src/Iris/Algebra.lean b/src/Iris/Algebra.lean
index 30043dc5..7a25fa15 100644
--- a/src/Iris/Algebra.lean
+++ b/src/Iris/Algebra.lean
@@ -13,3 +13,5 @@ import Iris.Algebra.UPred
 import Iris.Algebra.Heap
 import Iris.Algebra.View
 import Iris.Algebra.HeapView
+import Iris.Algebra.Monoid
+import Iris.Algebra.BigOp
diff --git a/src/Iris/Algebra/BigOp.lean b/src/Iris/Algebra/BigOp.lean
new file mode 100644
index 00000000..a7d842a1
--- /dev/null
+++ b/src/Iris/Algebra/BigOp.lean
@@ -0,0 +1,931 @@
+/-
+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.FiniteMap
+
+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
+
+/-- Corresponds to Rocq's `big_opL`. -/
+def bigOpL {M : Type u} {A : Type v} (op : M → M → M) (unit : M)
+    (Φ : Nat → A → M) (l : List A) : M :=
+  match l with
+  | [] => unit
+  | x :: xs => op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs)
+
+namespace BigOpL
+
+variable {M : Type _} {A : Type _} [OFE M] {op : M → M → M} {unit : M} [Monoid M op unit]
+
+omit [OFE M] [Monoid M op unit] in
+/-- Corresponds to Rocq's `big_opL_nil`. -/
+@[simp] theorem nil (Φ : Nat → A → M) :
+    bigOpL op unit Φ ([] : List A) = unit := rfl
+
+omit [OFE M] [Monoid M op unit] in
+/-- Corresponds to Rocq's `big_opL_cons`. -/
+@[simp] theorem cons (Φ : Nat → A → M) (x : A) (xs : List A) :
+    bigOpL op unit Φ (x :: xs) = op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs) := rfl
+
+/-- Corresponds to Rocq's `big_opL_singleton`. -/
+@[simp] theorem singleton (Φ : Nat → A → M) (x : A) :
+    bigOpL op unit Φ [x] ≡ Φ 0 x := by
+  simp only [cons, nil]
+  exact Monoid.op_right_id _
+
+/-- Corresponds to Rocq's `big_opL_proper`. -/
+theorem congr {Φ Ψ : Nat → A → M} {l : List A}
+    (h : ∀ i x, l[i]? = some x → Φ i x ≡ Ψ i x) :
+    bigOpL op unit Φ l ≡ bigOpL op unit Ψ l := by
+  induction l generalizing Φ Ψ with
+  | nil => exact Equiv.rfl
+  | cons y ys ih =>
+    simp only [cons]
+    have h0 : Φ 0 y ≡ Ψ 0 y := h 0 y rfl
+    have htail : ∀ i x, ys[i]? = some x → Φ (i + 1) x ≡ Ψ (i + 1) x := by
+      intro i x hget
+      exact h (i + 1) x hget
+    exact Monoid.op_proper h0 (ih htail)
+
+/-- Corresponds to Rocq's `big_opL_ne`. -/
+theorem congr_ne {Φ Ψ : Nat → A → M} {l : List A} {n : Nat}
+    (h : ∀ i x, l[i]? = some x → Φ i x ≡{n}≡ Ψ i x) :
+    bigOpL op unit Φ l ≡{n}≡ bigOpL op unit Ψ l := by
+  induction l generalizing Φ Ψ with
+  | nil => exact Dist.rfl
+  | cons y ys ih =>
+    simp only [cons]
+    have h0 : Φ 0 y ≡{n}≡ Ψ 0 y := h 0 y rfl
+    have htail : ∀ i x, ys[i]? = some x → Φ (i + 1) x ≡{n}≡ Ψ (i + 1) x := by
+      intro i x hget
+      exact h (i + 1) x hget
+    exact Monoid.op_ne_dist h0 (ih htail)
+
+/-- Congruence when the functions are equivalent on all indices. -/
+theorem congr' {Φ Ψ : Nat → A → M} {l : List A}
+    (h : ∀ i x, Φ i x ≡ Ψ i x) :
+    bigOpL op unit Φ l ≡ bigOpL op unit Ψ l :=
+  congr (fun i x _ => h i x)
+
+/-- Corresponds to Rocq's `big_opL_app`. -/
+theorem append (Φ : Nat → A → M) (l₁ l₂ : List A) :
+    bigOpL op unit Φ (l₁ ++ l₂) ≡
+      op (bigOpL op unit Φ l₁) (bigOpL op unit (fun n => Φ (n + l₁.length)) l₂) := by
+  induction l₁ generalizing Φ with
+  | nil => simp only [nil]; exact Equiv.symm (Monoid.op_left_id _)
+  | cons x xs ih =>
+    simp only [List.cons_append, cons, List.length_cons]
+    have ih' := ih (fun n => Φ (n + 1))
+    have heq : ∀ n, n + xs.length + 1 = n + (xs.length + 1) := fun n => by omega
+    calc op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) (xs ++ l₂))
+        _ ≡ op (Φ 0 x) (op (bigOpL op unit (fun n => Φ (n + 1)) xs)
+              (bigOpL op unit (fun n => Φ (n + xs.length + 1)) l₂)) :=
+            Monoid.op_congr_r ih'
+        _ ≡ op (op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs))
+              (bigOpL op unit (fun n => Φ (n + xs.length + 1)) l₂) :=
+            Equiv.symm (Monoid.op_assoc _ _ _)
+        _ ≡ op (op (Φ 0 x) (bigOpL op unit (fun n => Φ (n + 1)) xs))
+              (bigOpL op unit (fun n => Φ (n + (xs.length + 1))) l₂) := by
+            simp only [heq]; exact Equiv.rfl
+
+/-- Corresponds to Rocq's `big_opL_snoc`. -/
+theorem snoc (Φ : Nat → A → M) (l : List A) (x : A) :
+    bigOpL op unit Φ (l ++ [x]) ≡ op (bigOpL op unit Φ l) (Φ l.length x) := by
+  have h := @append M A _ op unit _ Φ l [x]
+  simp only [cons, nil, Nat.zero_add] at h
+  have hr : op (Φ l.length x) unit ≡ Φ l.length x := Monoid.op_right_id (Φ l.length x)
+  exact Monoid.op_congr_r hr |> Equiv.trans h
+
+/-- Corresponds to Rocq's `big_opL_unit`. -/
+theorem unit_const (l : List A) :
+    bigOpL op unit (fun _ _ => unit) l ≡ unit := by
+  induction l with
+  | nil => exact Equiv.rfl
+  | cons _ _ ih => simp only [cons]; exact Equiv.trans (Monoid.op_left_id _) ih
+
+/-- Corresponds to Rocq's `big_opL_op`. -/
+theorem op_distr (Φ Ψ : Nat → A → M) (l : List A) :
+    bigOpL op unit (fun i x => op (Φ i x) (Ψ i x)) l ≡
+      op (bigOpL op unit Φ l) (bigOpL op unit Ψ l) := by
+  induction l generalizing Φ Ψ with
+  | nil => simp only [nil]; exact Equiv.symm (Monoid.op_left_id _)
+  | cons x xs ih =>
+    simp only [cons]
+    exact Equiv.trans (Monoid.op_congr_r (ih _ _)) Monoid.op_op_swap
+
+/-- Corresponds to Rocq's `big_opL_fmap`. -/
+theorem map {B : Type v} (h : A → B) (Φ : Nat → B → M) (l : List A) :
+    bigOpL op unit Φ (l.map h) ≡ bigOpL op unit (fun i x => Φ i (h x)) l := by
+  induction l generalizing Φ with
+  | nil => exact Equiv.rfl
+  | cons x xs ih =>
+    simp only [List.map_cons, cons]
+    exact Monoid.op_proper Equiv.rfl (ih (fun n => Φ (n + 1)))
+
+omit [OFE M] [Monoid M op unit] in
+/-- Corresponds to Rocq's `big_opL_closed`. -/
+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 (bigOpL op unit Φ l) := by
+  induction l generalizing Φ with
+  | nil => exact hunit
+  | cons y ys ih =>
+    simp only [cons]
+    have h0 : P (Φ 0 y) := hf 0 y rfl
+    have htail : ∀ i x, ys[i]? = some x → P (Φ (i + 1) x) := fun i x hget => hf (i + 1) x hget
+    exact hop _ _ h0 (ih _ htail)
+
+/-- Corresponds to Rocq's `big_opL_permutation`. -/
+theorem perm (Φ : A → M) {l₁ l₂ : List A} (hp : l₁.Perm l₂) :
+    bigOpL op unit (fun _ => Φ) l₁ ≡ bigOpL op unit (fun _ => Φ) l₂ := by
+  induction hp with
+  | nil => exact Equiv.rfl
+  | cons _ _ ih => simp only [cons]; exact Monoid.op_congr_r ih
+  | swap _ _ _ => simp only [cons]; exact Monoid.op_swap_inner (unit := unit)
+  | trans _ _ ih1 ih2 => exact Equiv.trans ih1 ih2
+
+/-- Corresponds to Rocq's `big_opL_take_drop`. -/
+theorem take_drop (Φ : Nat → A → M) (l : List A) (n : Nat) :
+    bigOpL op unit Φ l ≡
+      op (bigOpL op unit Φ (l.take n)) (bigOpL op unit (fun k => Φ (n + k)) (l.drop n)) := by
+  by_cases hn : n ≤ l.length
+  · have h := @append M A _ op unit _ Φ (l.take n) (l.drop n)
+    simp only [List.take_append_drop, List.length_take_of_le hn, Nat.add_comm] at h
+    exact h
+  · 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 (Monoid.op_right_id _)
+
+/-- Corresponds to Rocq's `big_opL_omap`. -/
+theorem filter_map {B : Type v} (h : A → Option B) (Φ : B → M) (l : List A) :
+    bigOpL op unit (fun _ => Φ) (l.filterMap h) ≡
+      bigOpL op unit (fun _ x => (h x).elim unit Φ) l := 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 (Monoid.op_left_id _))
+    · exact Monoid.op_congr_r ih
+
+/-- Corresponds to Rocq's `big_opL_bind`. -/
+theorem bind {B : Type v} (h : A → List B) (Φ : B → M) (l : List A) :
+    bigOpL op unit (fun _ => Φ) (l.flatMap h) ≡
+      bigOpL op unit (fun _ x => bigOpL op unit (fun _ => Φ) (h x)) l := by
+  induction l with
+  | nil => exact Equiv.rfl
+  | cons x xs ih =>
+    simp only [List.flatMap_cons, cons]
+    exact Equiv.trans (append _ _ _) (Monoid.op_congr_r ih)
+
+omit [OFE M] [Monoid M op unit] in
+/-- Corresponds to Rocq's `big_opL_gen_proper_2`. -/
+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 (bigOpL op unit Φ l₁) (bigOpL op unit Ψ l₂) := 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]
+      have h0 : R (Φ 0 x) (Ψ 0 y) := hf 0 x y rfl rfl
+      have htail : ∀ i, ∀ a b, xs[i]? = some a → ys[i]? = some b →
+          R (Φ (i + 1) a) (Ψ (i + 1) b) := fun i a b ha hb => hf (i + 1) a b ha hb
+      exact hop _ _ _ _ h0 (ih (fun n => Φ (n + 1)) (fun n => Ψ (n + 1)) ys hlen htail)
+
+omit [OFE M] [Monoid M op unit] in
+/-- Corresponds to Rocq's `big_opL_gen_proper`. -/
+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 (bigOpL op unit Φ l) (bigOpL op unit Ψ l) := by
+  apply gen_proper_2 (op := op) (unit := unit) R Φ Ψ l l
+  · exact hR_refl unit
+  · exact hR_op
+  · rfl
+  · intro k x y hx hy
+    cases hget : l[k]? with
+    | none =>
+      rw [hget] at hx
+      cases hx
+    | some z =>
+      have hxz : x = z := by rw [hget] at hx; cases hx; rfl
+      have hyz : y = z := by rw [hget] at hy; cases hy; rfl
+      rw [hxz, hyz]
+      exact hf k z hget
+
+omit [OFE M] [Monoid M op unit] in
+/-- Corresponds to Rocq's `big_opL_ext`. -/
+theorem ext {Φ Ψ : Nat → A → M} {l : List A}
+    (h : ∀ i x, l[i]? = some x → Φ i x = Ψ i x) :
+    bigOpL op unit Φ l = bigOpL op unit Ψ l := by
+    apply gen_proper
+    · intro _
+      rfl
+    · intros _ _ _ _ ha hb
+      rw [ha, hb]
+    · apply h
+
+omit [OFE M] [Monoid M op unit] in
+/-- Corresponds to Rocq's `big_opL_consZ_l`. -/
+theorem cons_int_l (Φ : Int → A → M) (x : A) (l : List A) :
+    bigOpL op unit (fun k => Φ k) (x :: l) =
+    op (Φ 0 x) (bigOpL op unit (fun k y => Φ (1 + (k : Int)) y) l) := by
+  simp only [cons]
+  apply congrArg
+  apply ext
+  intro i y hy
+  congr 1
+  omega
+
+omit [OFE M] [Monoid M op unit] in
+/-- Corresponds to Rocq's `big_opL_consZ_r`. -/
+theorem cons_int_r (Φ : Int → A → M) (x : A) (l : List A) :
+    bigOpL op unit (fun k => Φ k) (x :: l) =
+    op (Φ 0 x) (bigOpL op unit (fun k y => Φ ((k : Int) + 1) y) l) := by
+  simp only [cons]
+  rfl
+
+/-- Corresponds to Rocq's `big_opL_proper_2`. -/
+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₂) :
+    bigOpL op unit Φ l₁ ≡ bigOpL op unit Ψ l₂ := by
+  apply gen_proper_2 (op := op) (unit := unit) (· ≡ ·) Φ Ψ l₁ l₂
+  · exact Equiv.rfl
+  · intros a a' b b' ha hb; exact Monoid.op_proper ha hb
+  · exact hlen
+  · intro k x y hx hy
+    cases hget1 : l₁[k]? with
+    | none =>
+      rw [hget1] at hx
+      cases hx
+    | some z₁ =>
+      cases hget2 : l₂[k]? with
+      | none =>
+        have h1 : k < l₁.length := by
+          cases h : l₁[k]? <;> simp_all
+        rw [hlen] at h1
+        have h2 : k < l₂.length := h1
+        have : l₂[k]? ≠ none := by
+          intro h
+          have : l₂[k]? = some l₂[k] := List.getElem?_eq_getElem h2
+          simp [h] at this
+        contradiction
+      | some z₂ =>
+        have hxz1 : x = z₁ := by rw [hget1] at hx; cases hx; rfl
+        have hyz2 : y = z₂ := by rw [hget2] at hy; cases hy; rfl
+        rw [hxz1, hyz2]
+        exact hf k z₁ z₂ hget1 hget2
+
+/-- Corresponds to Rocq's `big_opL_zip_seq`. -/
+theorem zip_idx (Φ : A × Nat → M) (n : Nat) (l : List A) :
+    bigOpL op unit (fun _ => Φ) (l.zipIdx n) ≡
+      bigOpL op unit (fun i x => Φ (x, n + i)) l := by
+  induction l generalizing n with
+  | nil => simp only [nil]; exact Equiv.rfl
+  | cons x xs ih =>
+    simp only [cons, Nat.add_zero]
+    refine Monoid.op_proper Equiv.rfl (Equiv.trans (ih (n + 1)) (congr' fun i _ => ?_))
+    simp only [Nat.add_assoc, Nat.add_comm 1 i]; exact Equiv.rfl
+
+/-- Corresponds to Rocq's `big_opL_zip_seqZ`. -/
+theorem zip_idx_int (Φ : A × Int → M) (n : Int) (l : List A) :
+    bigOpL op unit (fun _ => Φ) (Std.List.zipIdxInt l n) ≡
+      bigOpL op unit (fun i x => Φ (x, n + (i : Int))) l := by
+  unfold Std.List.zipIdxInt
+  suffices ∀ m, bigOpL op unit (fun _ => Φ) (l.mapIdx (fun i v => (v, (i : Int) + m))) ≡
+                bigOpL op unit (fun i x => Φ (x, m + (i : Int))) l by exact 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 Monoid.op_proper
+    · show Φ (x, (0 : Int) + m) ≡ Φ (x, m + (0 : Int))
+      rw [Int.zero_add, Int.add_zero]
+    · have h_shift : ∀ i, ((i + 1 : Nat) : Int) + m = (i : Int) + (m + 1) := by
+        intro i; omega
+      have list_eq : (List.mapIdx (fun i v => (v, ↑(i + 1) + m)) xs) =
+                     (List.mapIdx (fun i v => (v, ↑i + (m + 1))) xs) := by
+        apply List.ext_getElem
+        · simp only [List.length_mapIdx]
+        · intro n hn1 hn2
+          simp only [List.getElem_mapIdx]
+          congr 1
+          exact h_shift n
+      rw [list_eq]
+      have h_ih := ih (m + 1)
+      refine Equiv.trans h_ih (congr' fun i _ => ?_)
+      have : m + 1 + (i : Int) = m + ((i + 1 : Nat) : Int) := by omega
+      rw [this]
+
+/-- Corresponds to Rocq's `big_opL_sep_zip_with`. -/
+theorem sep_zip_with {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) :
+    bigOpL op unit (fun i c => op (Φ i (g1 c)) (Ψ i (g2 c))) (List.zipWith f l₁ l₂) ≡
+      op (bigOpL op unit Φ l₁) (bigOpL op unit Ψ l₂) := by
+  induction l₁ generalizing l₂ Φ Ψ with
+  | nil =>
+    cases l₂ with
+    | nil => simp only [List.zipWith_nil_left, nil]; exact Equiv.symm (Monoid.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]
+      exact Equiv.trans (Monoid.op_congr_r (ih (fun n => Φ (n + 1)) (fun n => Ψ (n + 1)) ys hlen)) Monoid.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) :
+    bigOpL op unit (fun i xy => op (Φ i xy.1) (Ψ i xy.2)) (l₁.zip l₂) ≡
+      op (bigOpL op unit Φ l₁) (bigOpL op unit Ψ l₂) := by
+  simp [List.zip]
+  apply sep_zip_with (op := op)
+  · intro _ _
+    trivial
+  · intro _ _
+    trivial
+  · apply 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 [Monoid M₁ op₁ unit₁] [Monoid M₂ op₂ unit₂]
+variable {B : Type w}
+
+/-- Monoid homomorphisms distribute over big ops. -/
+theorem commute {R : M₂ → M₂ → Prop} {f : M₁ → M₂}
+    (hom : MonoidHomomorphism op₁ op₂ unit₁ unit₂ R f)
+    (Φ : Nat → B → M₁) (l : List B) :
+    R (f (bigOpL op₁ unit₁ Φ l)) (bigOpL op₂ unit₂ (fun i x => f (Φ i x)) l) := by
+  induction l generalizing Φ with
+  | nil => simp only [nil]; exact hom.map_unit
+  | cons x xs ih =>
+    simp only [cons]
+    have hhom := hom.homomorphism (Φ 0 x) (bigOpL op₁ unit₁ (fun n => Φ (n + 1)) xs)
+    have hih := ih (fun n => Φ (n + 1))
+    exact hom.rel_trans hhom (hom.op_proper (hom.rel_refl _) hih)
+
+/-- Weak monoid homomorphisms distribute over non-empty big ops. -/
+theorem commute_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 (bigOpL op₁ unit₁ Φ l)) (bigOpL op₂ unit₂ (fun i x => f (Φ i x)) l) := 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
+      have hlhs : f (op₁ (Φ 0 x) unit₁) ≡ f (Φ 0 x) :=
+        NonExpansive.eqv (Monoid.op_right_id (Φ 0 x))
+      have hrhs : op₂ (f (Φ 0 x)) unit₂ ≡ f (Φ 0 x) :=
+        Monoid.op_right_id (f (Φ 0 x))
+      exact hom.rel_proper hlhs hrhs |>.mpr (hom.rel_refl _)
+    | cons y ys =>
+      have hhom := hom.homomorphism (Φ 0 x) (bigOpL op₁ unit₁ (fun n => Φ (n + 1)) (y :: ys))
+      have hih := ih (fun n => Φ (n + 1)) (List.cons_ne_nil y ys)
+      exact hom.rel_trans hhom (hom.op_proper (hom.rel_refl _) hih)
+
+end BigOpL
+
+namespace BigOpM
+
+open Iris.Std
+
+variable {M : Type u} [OFE M] {op : M → M → M} {unit : M} [Monoid M op unit]
+variable {M' : Type _ → Type _} {K : Type _} {V : Type _}
+variable [DecidableEq K] [DecidableEq V] [FiniteMap K M'] [FiniteMapLaws K M']
+
+/-- Corresponds to Rocq's `big_opM`. -/
+def bigOpM (Φ : K → V → M) (m : M' V) : M :=
+  bigOpL op unit (fun _ kv => Φ kv.1 kv.2) (FiniteMap.toList m)
+
+omit [OFE M] [Monoid M op unit] [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_empty`. -/
+@[simp] theorem empty (Φ : K → V → M) :
+    bigOpM (op := op) (unit := unit) Φ (∅ : M' V) = unit := by
+  simp only [bigOpM, FiniteMapLaws.toList_empty, BigOpL.nil]
+
+/-- Corresponds to Rocq's `big_opM_insert`. -/
+theorem insert (Φ : K → V → M) (m : M' V) (i : K) (x : V) :
+    FiniteMap.get? m i = none →
+    bigOpM (op := op) (unit := unit) Φ (FiniteMap.insert m i x) ≡
+      op (Φ i x) (bigOpM (op := op) (unit := unit) Φ m) := by
+  intro hi
+  simp only [bigOpM]
+  have hperm := FiniteMapLaws.toList_insert m i x hi
+  have heq : bigOpL op unit (fun _ kv => Φ kv.1 kv.2) (FiniteMap.toList (FiniteMap.insert m i x)) ≡
+             bigOpL op unit (fun _ kv => Φ kv.1 kv.2) ((i, x) :: FiniteMap.toList m) :=
+    BigOpL.perm _ hperm
+  simp only [BigOpL.cons] at heq
+  exact heq
+
+/-- Corresponds to Rocq's `big_opM_delete`. -/
+theorem delete (Φ : K → V → M) (m : M' V) (i : K) (x : V) :
+    FiniteMap.get? m i = some x →
+    bigOpM (op := op) (unit := unit) Φ m ≡
+      op (Φ i x) (bigOpM (op := op) (unit := unit) Φ (FiniteMap.delete m i)) := by
+  intro hi
+  have heq := FiniteMapLaws.insert_delete_cancel m i x hi
+  have : bigOpM (op := op) (unit := unit) Φ m = bigOpM (op := op) (unit := unit) Φ (FiniteMap.insert (FiniteMap.delete m i) i x) := by
+    rw [heq]
+  rw [this]
+  have hdelete := FiniteMapLaws.get?_delete_same m i
+  exact insert Φ (FiniteMap.delete m i) i x hdelete
+
+variable {A : Type w} [DecidableEq A]
+
+/-- Corresponds to Rocq's `big_opM_gen_proper_2`. -/
+theorem gen_proper_2 {B : Type w} [DecidableEq B] (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 FiniteMap.get? m1 k, FiniteMap.get? m2 k with
+      | some y1, some y2 => R (Φ k y1) (Ψ k y2)
+      | none, none => True
+      | _, _ => False) :
+    R (bigOpM (op := op) (unit := unit) Φ m1) (bigOpM (op := op) (unit := unit) Ψ m2) := by
+  refine FiniteMapLaws.induction_on (P := fun m1' => ∀ m2' Φ' Ψ',
+      (∀ k, match FiniteMap.get? m1' k, FiniteMap.get? m2' k with
+        | some y1, some y2 => R (Φ' k y1) (Ψ' k y2)
+        | none, none => True
+        | _, _ => False) →
+      R (bigOpM (op := op) (unit := unit) Φ' m1') (bigOpM (op := op) (unit := unit) Ψ' m2'))
+    ?hemp ?hins m1 m2 Φ Ψ hfg
+  case hemp =>
+    intro m2' Φ' Ψ' hfg'
+    refine FiniteMapLaws.induction_on (P := fun m2'' => ∀ Φ'' Ψ'',
+        (∀ k, match FiniteMap.get? (∅ : M' A) k, FiniteMap.get? m2'' k with
+          | some y1, some y2 => R (Φ'' k y1) (Ψ'' k y2)
+          | none, none => True
+          | _, _ => False) →
+        R (bigOpM (op := op) (unit := unit) Φ'' (∅ : M' A)) (bigOpM (op := op) (unit := unit) Ψ'' m2''))
+      ?hemp2 ?hins2 m2' Φ' Ψ' hfg'
+    case hemp2 => intro _ _ _; rw [empty, empty]; exact hR_sub unit unit Equiv.rfl
+    case hins2 =>
+      intro k x2 _ _ _ _ _ hfg''
+      have := hfg'' k
+      rw [FiniteMapLaws.get?_empty, FiniteMapLaws.get?_insert_same] at this
+      cases this
+  case hins =>
+    intro k x1 m1' hm1'k IH m2' Φ' Ψ' hfg'
+    have hfg_k := hfg' k
+    rw [FiniteMapLaws.get?_insert_same] at hfg_k
+    cases hm2k : FiniteMap.get? m2' k with
+    | none => rw [hm2k] at hfg_k; cases hfg_k
+    | some x2 =>
+      rw [hm2k] at hfg_k
+      have h_IH : R (bigOpM (op := op) (unit := unit) Φ' m1')
+                    (bigOpM (op := op) (unit := unit) Ψ' (FiniteMap.delete m2' k)) := by
+        refine IH _ _ _ fun k' => ?_
+        by_cases hkk' : k = k'
+        · subst hkk'; rw [FiniteMapLaws.get?_delete_same, hm1'k]; trivial
+        · have h1 := FiniteMapLaws.get?_insert_ne m1' k k' x1 hkk'
+          have h2 := FiniteMapLaws.get?_delete_ne m2' k k' hkk'
+          rw [← h1, h2]; exact hfg' k'
+      exact hR_equiv.trans (hR_sub _ _ (insert Φ' m1' k x1 hm1'k))
+        (hR_equiv.trans (hR_op _ _ _ _ hfg_k h_IH) (hR_sub _ _ (Equiv.symm (delete Ψ' m2' k x2 hm2k))))
+
+omit [Monoid M op unit] [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_gen_proper`. -/
+theorem gen_proper {M : Type u} {op : M → M → M} {unit : M} (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, FiniteMap.get? m k = some x → R (Φ k x) (Ψ k x)) :
+    R (bigOpM (op := op) (unit := unit) Φ m) (bigOpM (op := op) (unit := unit) Ψ m) := by
+  simp only [bigOpM]
+  apply BigOpL.gen_proper_2 (op := op) (unit := unit) R
+  · exact hR_refl unit
+  · exact hR_op
+  · rfl
+  · intro i x y hx hy
+    rw [hx] at hy
+    cases hy
+    have : (x.1, x.2) ∈ FiniteMap.toList m := by
+      rw [List.mem_iff_getElem?]
+      exact ⟨i, hx⟩
+    have := FiniteMapLaws.mem_toList m x.1 x.2 |>.mp this
+    exact hf x.1 x.2 this
+
+omit [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_ext`. -/
+theorem ext {M : Type u} (op : M → M → M) (unit : M) (Φ Ψ : K → V → M) (m : M' V)
+    (hf : ∀ k x, FiniteMap.get? m k = some x → Φ k x = Ψ k x) :
+    bigOpM (op := op) (unit := unit) Φ m = bigOpM (op := op) (unit := unit) Ψ m := by
+  apply gen_proper (R := (· = ·))
+  · intro _; rfl
+  · intros _ _ _ _ ha hb; rw [ha, hb]
+  · exact hf
+
+omit [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_ne`. -/
+theorem ne (Φ Ψ : K → V → M) (m : M' V) (n : Nat)
+    (hf : ∀ k x, FiniteMap.get? m k = some x → Φ k x ≡{n}≡ Ψ k x) :
+    bigOpM (op := op) (unit := unit) Φ m ≡{n}≡ bigOpM (op := op) (unit := unit) Ψ m := by
+  apply gen_proper (R := (· ≡{n}≡ ·))
+  · intro _; exact Dist.rfl
+  · intros a a' b b' ha hb; exact Monoid.op_ne_dist ha hb
+  · exact hf
+
+omit [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_proper`. -/
+theorem proper (Φ Ψ : K → V → M) (m : M' V)
+    (hf : ∀ k x, FiniteMap.get? m k = some x → Φ k x ≡ Ψ k x) :
+    bigOpM (op := op) (unit := unit) Φ m ≡ bigOpM (op := op) (unit := unit) Ψ m := by
+  apply gen_proper (R := (· ≡ ·))
+  · intro _; exact Equiv.rfl
+  · intros a a' b b' ha hb; exact Monoid.op_proper ha hb
+  · exact hf
+
+omit [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_proper_2`. -/
+theorem proper_2 [OFE A] (Φ : K → A → M) (Ψ : K → A → M) (m1 m2 : M' A)
+    (hm : ∀ k, FiniteMap.get? m1 k = FiniteMap.get? m2 k)
+    (hf : ∀ k y1 y2,
+      FiniteMap.get? m1 k = some y1 →
+      FiniteMap.get? m2 k = some y2 →
+      y1 ≡ y2 →
+      Φ k y1 ≡ Ψ k y2) :
+    bigOpM (op := op) (unit := unit) Φ m1 ≡ bigOpM (op := op) (unit := unit) Ψ m2 := by
+  apply gen_proper_2 (R := (· ≡ ·))
+  · intros _ _ h; exact h
+  · exact equiv_eqv
+  · intros a a' b b' ha hb; exact Monoid.op_proper ha hb
+  · intro k
+    have hlk := hm k
+    cases hm1k : FiniteMap.get? m1 k with
+    | none =>
+      rw [hm1k] at hlk
+      rw [← hlk]
+      trivial
+    | some y1 =>
+      rw [hm1k] at hlk
+      cases hm2k : FiniteMap.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
+
+omit [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_ne'` instance. -/
+theorem ne_pointwise (Φ Ψ : K → V → M) (m : M' V) (n : Nat)
+    (hf : ∀ k x, Φ k x ≡{n}≡ Ψ k x) :
+    bigOpM (op := op) (unit := unit) Φ m ≡{n}≡ bigOpM (op := op) (unit := unit) Ψ m := by
+  apply ne
+  intros k x _
+  exact hf k x
+
+omit [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_proper'` instance. -/
+theorem proper_pointwise (Φ Ψ : K → V → M) (m : M' V)
+    (hf : ∀ k x, Φ k x ≡ Ψ k x) :
+    bigOpM (op := op) (unit := unit) Φ m ≡ bigOpM (op := op) (unit := unit) Ψ m := by
+  apply proper
+  intros k x _
+  exact hf k x
+
+omit [Monoid M op unit] [DecidableEq K] [DecidableEq V] [FiniteMapLaws K M'] in
+/-- Corresponds to Rocq's `big_opM_map_to_list`. -/
+theorem to_list (Φ : K → V → M) (m : M' V) :
+    bigOpM (op := op) (unit := unit) Φ m ≡
+    bigOpL op unit (fun _ kx => Φ kx.1 kx.2) (FiniteMap.toList m) := by
+  simp only [bigOpM]
+  rfl
+
+/-- Corresponds to Rocq's `big_opM_list_to_map`. -/
+theorem of_list (Φ : K → V → M) (l : List (K × V))
+    (hnodup : (l.map Prod.fst).Nodup) :
+    bigOpM (op := op) (unit := unit) Φ (FiniteMap.ofList l : M' V) ≡
+    bigOpL op unit (fun _ kx => Φ kx.1 kx.2) l := by
+  have h1 := to_list (op := op) (unit := unit) Φ (FiniteMap.ofList l : M' V)
+  apply Equiv.trans h1
+  apply BigOpL.perm
+  exact FiniteMapLaws.toList_ofList l hnodup
+
+/-- Corresponds to Rocq's `big_opM_singleton`. -/
+theorem singleton (Φ : K → V → M) (i : K) (x : V) :
+    bigOpM (op := op) (unit := unit) Φ (FiniteMap.singleton (M := M') i x) ≡ Φ i x := by
+  have : FiniteMap.get? (∅ : M' V) i = none := FiniteMapLaws.get?_empty i
+  have := insert (op := op) (unit := unit) Φ (∅ : M' V) i x this
+  rw [empty] at this
+  exact Equiv.trans this (Monoid.op_right_id (Φ i x))
+
+/-- Corresponds to Rocq's `big_opM_unit`. -/
+theorem unit_const (m : M' V) :
+    bigOpM (op := op) (unit := unit) (fun _ _ => unit) m ≡ unit := by
+  refine FiniteMapLaws.induction_on
+    (P := fun (m' : M' V) => bigOpM (op := op) (unit := unit) (fun _ _ => unit) m' ≡ unit)
+    ?hemp ?hins m
+  case hemp =>
+    show bigOpM (op := op) (unit := unit) (fun _ _ => unit) ∅ ≡ unit
+    rw [empty]
+  case hins =>
+    intro i x m' hm' IH
+    show bigOpM (op := op) (unit := unit) (fun _ _ => unit) (FiniteMap.insert m' i x) ≡ unit
+    have h_ins := insert (op := op) (unit := unit) (fun _ _ => unit) m' i x hm'
+    exact Equiv.trans h_ins (Equiv.trans (Monoid.op_proper Equiv.rfl IH) (Monoid.op_left_id unit))
+
+omit [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_fmap`. -/
+theorem map {B : Type w} [DecidableEq B] (h : V → B) (Φ : K → B → M) (m : M' V) :
+    bigOpM (op := op) (unit := unit) Φ (FiniteMap.map h m) ≡
+    bigOpM (op := op) (unit := unit) (fun k v => Φ k (h v)) m := by
+  simp only [bigOpM]
+  have h1 : bigOpL op unit (fun _ kv => Φ kv.1 kv.2) (FiniteMap.toList (FiniteMap.map h m)) ≡
+            bigOpL op unit (fun _ kv => Φ kv.1 kv.2) ((FiniteMap.toList m).map (fun kv => (kv.1, h kv.2))) := by
+    apply BigOpL.perm
+    exact FiniteMapLaws.toList_map m h
+  apply Equiv.trans h1
+  exact BigOpL.map (op := op) (unit := unit) (fun kv => (kv.1, h kv.2)) (fun _ kv => Φ kv.1 kv.2) (FiniteMap.toList m)
+
+omit [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_omap`. -/
+theorem filter_map [FiniteMapLawsSelf K M'] (h : V → Option V) (Φ : K → V → M) (m : M' V) :
+    bigOpM (op := op) (unit := unit) Φ (FiniteMap.filterMap h m) ≡
+    bigOpM (op := op) (unit := unit) (fun k v => (h v).elim unit (Φ k)) m := by
+  simp only [bigOpM, FiniteMap.filterMap]
+  -- Use toList_filterMap to relate toList of filterMap to filterMap of toList
+  have h1 : bigOpL op unit (fun _ kv => Φ kv.1 kv.2)
+              (FiniteMap.toList (FiniteMap.ofList ((FiniteMap.toList m).filterMap (fun (k, v) => (h v).map (k, ·))) : M' V)) ≡
+            bigOpL op unit (fun _ kv => Φ kv.1 kv.2)
+              ((FiniteMap.toList m).filterMap (fun (k, v) => (h v).map (k, ·))) := by
+    apply BigOpL.perm
+    have hperm := toList_filterMap m h
+    exact hperm
+  refine Equiv.trans h1 ?_
+  -- Now use BigOpL.filter_map
+  have h2 : bigOpL op unit (fun _ kv => Φ kv.1 kv.2)
+              ((FiniteMap.toList m).filterMap (fun (k, v) => (h v).map (k, ·))) ≡
+            bigOpL op unit (fun _ kv => ((h kv.2).map (kv.1, ·)).elim unit (fun kv' => Φ kv'.1 kv'.2))
+              (FiniteMap.toList m) := by
+    exact BigOpL.filter_map (op := op) (unit := unit) (fun kv => (h kv.2).map (kv.1, ·)) (fun kv => Φ kv.1 kv.2) (FiniteMap.toList m)
+  refine Equiv.trans h2 ?_
+  -- Simplify the function
+  apply BigOpL.congr'
+  intro i kv
+  cases hkv : h kv.2 <;> simp [Option.elim, Option.map]
+
+/-- Corresponds to Rocq's `big_opM_insert_delete`. -/
+theorem insert_delete (Φ : K → V → M) (m : M' V) (i : K) (x : V) :
+    bigOpM (op := op) (unit := unit) Φ (FiniteMap.insert m i x) ≡
+      op (Φ i x) (bigOpM (op := op) (unit := unit) Φ (FiniteMap.delete m i)) := by
+  rw [← FiniteMapLaws.insert_delete m i x]
+  exact insert Φ (FiniteMap.delete m i) i x (FiniteMapLaws.get?_delete_same m i)
+
+/-- Corresponds to Rocq's `big_opM_insert_override`. -/
+theorem insert_override (Φ : K → A → M) (m : M' A) (i : K) (x x' : A) :
+    FiniteMap.get? m i = some x → Φ i x ≡ Φ i x' →
+    bigOpM (op := op) (unit := unit) Φ (FiniteMap.insert m i x') ≡
+      bigOpM (op := op) (unit := unit) Φ m := by
+  intro hi hΦ
+  rw [← FiniteMapLaws.insert_delete m i x']
+  refine Equiv.trans (insert Φ (FiniteMap.delete m i) i x' (FiniteMapLaws.get?_delete_same m i)) ?_
+  refine Equiv.trans (Monoid.op_proper (Equiv.symm hΦ) Equiv.rfl) ?_
+  exact Equiv.symm (delete Φ m i x hi)
+
+/-- Corresponds to Rocq's `big_opM_fn_insert`. -/
+theorem fn_insert {B : Type w} [DecidableEq B] (g : K → V → B → M) (f : K → B) (m : M' V)
+    (i : K) (x : V) (b : B) (hi : FiniteMap.get? m i = none) :
+    bigOpM (op := op) (unit := unit) (fun k y => g k y (if k = i then b else f k))
+      (FiniteMap.insert m i x) ≡
+    op (g i x b) (bigOpM (op := op) (unit := unit) (fun k y => g k y (f k)) m) := by
+  have h1 := insert (op := op) (unit := unit) (fun k y => g k y (if k = i then b else f k)) m i x hi
+  refine Equiv.trans h1 ?_
+  apply Monoid.op_proper
+  · simp
+  · apply proper (op := op) (unit := unit)
+    intros k y hk
+    have hne : k ≠ i := fun heq => by rw [heq] at hk; rw [hi] at hk; cases hk
+    simp [hne]
+
+/-- Corresponds to Rocq's `big_opM_fn_insert'`. -/
+theorem fn_insert' (f : K → M) (m : M' V) (i : K) (x : V) (P : M)
+    (hi : FiniteMap.get? m i = none) :
+    bigOpM (op := op) (unit := unit) (fun k _ => if k = i then P else f k)
+      (FiniteMap.insert m i x) ≡
+    op P (bigOpM (op := op) (unit := unit) (fun k _ => f k) m) := by
+  have h1 := insert (op := op) (unit := unit) (fun k _ => if k = i then P else f k) m i x hi
+  refine Equiv.trans h1 ?_
+  apply Monoid.op_proper
+  · simp
+  · apply proper (op := op) (unit := unit)
+    intros k y hk
+    have hne : k ≠ i := fun heq => by rw [heq] at hk; rw [hi] at hk; cases hk
+    simp [hne]
+
+
+omit [DecidableEq K] [DecidableEq V] in
+private theorem filter_list_aux (Φ : K × V → M) (φ : K → V → Bool) (l : List (K × V)) :
+    bigOpL op unit (fun _ kv => Φ kv) (l.filter (fun kv => φ kv.1 kv.2)) ≡
+    bigOpL op unit (fun _ kv => if φ kv.1 kv.2 then Φ kv else unit) l := by
+  induction l with
+  | nil => simp only [List.filter, BigOpL.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 (Monoid.op_left_id _))
+    | true =>
+      simp only [BigOpL.cons, hp]
+      exact Monoid.op_congr_r ih
+
+omit [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_filter'`. -/
+theorem filter' [FiniteMapLawsSelf K M'] (φ : K → V → Bool) (Φ : K → V → M) (m : M' V) :
+    bigOpM (op := op) (unit := unit) Φ (FiniteMap.filter φ m) ≡
+    bigOpM (op := op) (unit := unit) (fun k x => if φ k x then Φ k x else unit) m := by
+  unfold bigOpM
+  have hperm := toList_filter m φ
+  have heq : bigOpL op unit (fun _ kv => Φ kv.1 kv.2)
+               (FiniteMap.toList (FiniteMap.filter φ m)) ≡
+             bigOpL op unit (fun _ kv => Φ kv.1 kv.2)
+               ((FiniteMap.toList m).filter (fun kv => φ kv.1 kv.2)) :=
+    BigOpL.perm _ hperm
+  refine Equiv.trans heq ?_
+  exact filter_list_aux (fun kv => Φ kv.1 kv.2) φ (FiniteMap.toList m)
+
+/-- Corresponds to Rocq's `big_opM_union`. -/
+theorem union (Φ : K → V → M) (m1 m2 : M' V) (hdisj : m1 ##ₘ m2) :
+    bigOpM (op := op) (unit := unit) Φ (m1 ∪ m2) ≡
+    op (bigOpM (op := op) (unit := unit) Φ m1) (bigOpM (op := op) (unit := unit) Φ m2) := by
+  apply FiniteMapLaws.induction_on (P := fun m1 =>
+    m1 ##ₘ m2 →
+    bigOpM (op := op) (unit := unit) Φ (m1 ∪ m2) ≡
+    op (bigOpM (op := op) (unit := unit) Φ m1) (bigOpM (op := op) (unit := unit) Φ m2))
+  · intro _
+    rw [FiniteMapLaws.ext (∅ ∪ m2) m2 fun k => by simp [FiniteMapLaws.get?_union, FiniteMapLaws.get?_empty], empty]
+    exact (Monoid.op_left_id _).symm
+  · intro i x m hi_none IH hdisj'
+    have hi_m2 : get? m2 i = none := by simpa [FiniteMapLaws.get?_insert_same] using FiniteMapLaws.disjoint_iff (Std.insert m i x) m2 |>.mp hdisj' i
+    have hm_disj : m ##ₘ m2 := fun k ⟨hk1, hk2⟩ => hdisj' k ⟨by
+      by_cases h : i = k <;> simp [FiniteMapLaws.get?_insert_same, FiniteMapLaws.get?_insert_ne, *], hk2⟩
+    rw [← FiniteMapLaws.ext (Std.insert (m ∪ m2) i x) (Std.insert m i x ∪ m2) fun k => congrFun (FiniteMapLaws.union_insert_left m m2 i x) k]
+    refine (insert Φ (m ∪ m2) i x (by simp [FiniteMapLaws.get?_union_none, hi_none, hi_m2])).trans ?_
+    refine (Monoid.op_congr_r (IH hm_disj)).trans ?_
+    refine (Monoid.op_assoc _ _ _).symm.trans ?_
+    exact Monoid.op_congr_l (insert Φ m i x hi_none).symm
+  · exact hdisj
+
+omit [DecidableEq V] [DecidableEq K] [FiniteMapLaws K M'] in
+/-- Corresponds to Rocq's `big_opM_op`. -/
+theorem op_distr (Φ Ψ : K → V → M) (m : M' V) :
+    bigOpM (op := op) (unit := unit) (fun k x => op (Φ k x) (Ψ k x)) m ≡
+    op (bigOpM (op := op) (unit := unit) Φ m) (bigOpM (op := op) (unit := unit) Ψ m) := by
+  simp only [bigOpM]
+  have h := BigOpL.op_distr (op := op) (unit := unit)
+    (fun _ kv => Φ kv.1 kv.2) (fun _ kv => Ψ kv.1 kv.2) (FiniteMap.toList m)
+  exact h
+
+private theorem closed_aux (P : M → Prop) (Φ : K → V → M)
+    (hproper : ∀ x y, x ≡ y → (P x ↔ P y))
+    (hunit : P unit)
+    (hop : ∀ x y, P x → P y → P (op x y)) :
+    ∀ (m' : M' V), (∀ k' x', FiniteMap.get? m' k' = some x' → P (Φ k' x')) →
+        P (bigOpM (op := op) (unit := unit) Φ m') := by
+  intro m' hf'
+  refine FiniteMapLaws.induction_on
+    (P := fun m'' => (∀ k x, FiniteMap.get? m'' k = some x → P (Φ k x)) →
+                     P (bigOpM (op := op) (unit := unit) Φ m''))
+    ?hemp ?hins m' hf'
+  case hemp =>
+    intro _
+    simp only [empty]
+    exact hunit
+  case hins =>
+    intro k x m'' hm'' IH hf''
+    have h_ins := insert (op := op) (unit := unit) Φ m'' k x hm''
+    apply (hproper _ _ h_ins) |>.mpr
+    apply hop
+    · apply hf''
+      exact FiniteMapLaws.get?_insert_same m'' k x
+    · apply IH
+      intro k' x' hget'
+      apply hf''
+      rw [FiniteMapLaws.get?_insert_ne m'' k k' x]
+      · exact hget'
+      · intro heq
+        subst heq
+        rw [hget'] at hm''
+        exact Option.noConfusion hm''
+
+/-- Corresponds to Rocq's `big_opM_closed`. -/
+theorem closed (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, FiniteMap.get? m k = some x → P (Φ k x)) :
+    P (bigOpM (op := op) (unit := unit) Φ m) :=
+  closed_aux P Φ hproper hunit hop m hf
+
+omit [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_kmap`. -/
+theorem kmap {M'' : Type _ → Type _} {K' : Type _} [DecidableEq K'] [FiniteMap K' M'']
+    [FiniteMapLaws K' M''] [FiniteMapKmapLaws K K' M' M'']
+    (h : K → K') (hinj : ∀ {x y}, h x = h y → x = y) (Φ : K' → V → M) (m : M' V) :
+    bigOpM (op := op) (unit := unit) Φ (FiniteMap.kmap (M' := M'') h m : M'' V) ≡
+    bigOpM (op := op) (unit := unit) (fun k v => Φ (h k) v) m := by
+  simp only [bigOpM]
+  have h1 : bigOpL op unit (fun _ kv => Φ kv.1 kv.2) (FiniteMap.toList (FiniteMap.kmap (M' := M'') h m : M'' V)) ≡
+            bigOpL op unit (fun _ kv => Φ kv.1 kv.2) ((FiniteMap.toList m).map (fun kv => (h kv.1, kv.2))) := by
+    apply BigOpL.perm
+    exact FiniteMapKmapLaws.toList_kmap h m hinj
+  apply Equiv.trans h1
+  exact BigOpL.map (op := op) (unit := unit) (fun kv => (h kv.1, kv.2)) (fun _ kv => Φ kv.1 kv.2) (FiniteMap.toList m)
+
+omit [DecidableEq V] in
+/-- Corresponds to Rocq's `big_opM_map_seq`. -/
+theorem map_seq {M'' : Type w → Type _} [FiniteMap Nat M''] [FiniteMapLaws Nat M'']
+    [FiniteMapSeqLaws M'']
+    (Φ : Nat → V → M) (start : Nat) (l : List V) :
+    bigOpM (op := op) (unit := unit) Φ (FiniteMap.map_seq (M := M'') start l : M'' V) ≡
+    bigOpL op unit (fun i x => Φ (start + i) x) l := by
+  simp only [bigOpM]
+  refine Equiv.trans (BigOpL.perm _ (FiniteMapSeqLaws.toList_map_seq start l)) ?_
+  induction l generalizing start with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [List.mapIdx_cons, BigOpL.cons, Nat.zero_add, Nat.add_zero]
+    have : xs.mapIdx (fun i v => (i + 1 + start, v)) = xs.mapIdx (fun i v => (i + (start + 1), v)) := by
+      congr 1; funext i v; rw [Nat.add_assoc, Nat.add_comm 1 start]
+    rw [this]
+    exact Monoid.op_proper Equiv.rfl (Equiv.trans (ih (start + 1)) (BigOpL.congr' fun i _ => by simp [Nat.add_assoc, Nat.add_comm 1]))
+
+/-- Corresponds to Rocq's `big_opM_sep_zip_with`. -/
+theorem sep_zip_with {A : Type _} {B : Type _} {C : Type _}
+    [DecidableEq A] [DecidableEq B] [DecidableEq C]
+    (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, (FiniteMap.get? m1 k).isSome ↔ (FiniteMap.get? m2 k).isSome) :
+    bigOpM (op := op) (unit := unit) (fun k xy => op (h1 k (g1 xy)) (h2 k (g2 xy)))
+      (FiniteMap.zipWith f m1 m2) ≡
+    op (bigOpM (op := op) (unit := unit) h1 m1) (bigOpM (op := op) (unit := unit) h2 m2) := by
+  have h_op := op_distr (op := op) (unit := unit)
+    (fun k xy => h1 k (g1 xy)) (fun k xy => h2 k (g2 xy)) (FiniteMap.zipWith f m1 m2)
+  apply Equiv.trans h_op
+  apply Monoid.op_proper
+  · have h1_fmap := map (op := op) (unit := unit) g1 h1 (FiniteMap.zipWith f m1 m2)
+    apply Equiv.trans (Equiv.symm h1_fmap)
+    have heq := FiniteMapLaws.map_zipWith_right f g1 m1 m2 hg1 hdom
+    rw [heq]
+  · have h2_fmap := map (op := op) (unit := unit) g2 h2 (FiniteMap.zipWith f m1 m2)
+    apply Equiv.trans (Equiv.symm h2_fmap)
+    have heq := FiniteMapLaws.map_zipWith_left f g2 m1 m2 hg2 hdom
+    rw [heq]
+
+/-- Corresponds to Rocq's `big_opM_sep_zip`. -/
+theorem sep_zip {A : Type _} {B : Type _}
+    [DecidableEq A] [DecidableEq B]
+    (h1 : K → A → M) (h2 : K → B → M) (m1 : M' A) (m2 : M' B)
+    (hdom : ∀ k, (FiniteMap.get? m1 k).isSome ↔ (FiniteMap.get? m2 k).isSome) :
+    bigOpM (op := op) (unit := unit) (fun k xy => op (h1 k xy.1) (h2 k xy.2))
+      (FiniteMap.zip m1 m2) ≡
+    op (bigOpM (op := op) (unit := unit) h1 m1) (bigOpM (op := op) (unit := unit) h2 m2) := by
+  simp only [FiniteMap.zip]
+  exact sep_zip_with (op := op) (unit := unit) Prod.mk Prod.fst Prod.snd h1 h2 m1 m2
+    (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..03fe3007
--- /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 Monoid (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 Monoid
+
+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} [Monoid M 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} [Monoid M 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} [Monoid M 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} [Monoid M 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} [Monoid M 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} [Monoid M 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} [Monoid M 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 Monoid
+
+/-! ## 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₂)
+    [Monoid M₁ op₁ unit₁] [Monoid M₂ 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₂)
+    [Monoid M₁ op₁ unit₁] [Monoid M₂ 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/BI.lean b/src/Iris/BI.lean
index 3bea992c..7af46a4d 100644
--- a/src/Iris/BI.lean
+++ b/src/Iris/BI.lean
@@ -6,3 +6,4 @@ import Iris.BI.Instances
 import Iris.BI.BI
 import Iris.BI.Notation
 import Iris.BI.Updates
+import Iris.BI.BigOp
diff --git a/src/Iris/BI/BigOp.lean b/src/Iris/BI/BigOp.lean
new file mode 100644
index 00000000..106eb63b
--- /dev/null
+++ b/src/Iris/BI/BigOp.lean
@@ -0,0 +1,307 @@
+/-
+Copyright (c) 2026 Sam Hart. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sam Hart
+-/
+import Iris.BI.BI
+import Iris.BI.DerivedLaws
+import Iris.BI.DerivedLawsLater
+import Iris.Algebra.BigOp
+import Iris.Std.FiniteMap
+
+/-! # BI-Level Big Operators
+
+Reference: `iris/bi/big_op.v`
+
+Iterated separating conjunction over lists and finite maps, specialized from the
+algebra-level `bigOpL` and `bigOpM` to the BI separation connective `∗` with
+unit `emp`.
+
+The list version `big_sepL Φ l` computes:
+
+    Φ 0 x₀ ∗ Φ 1 x₁ ∗ ⋯ ∗ Φ (n-1) xₙ₋₁
+
+The map version `big_sepM Φ m` computes the same over the key-value pairs of `m`,
+in the order given by `toList`. Since `∗` is commutative and associative, the
+result is independent of enumeration order (up to `⊣⊢`).
+
+These are the main iteration primitives used throughout the Iris base logic:
+- `wsat` uses `[∗ map]` to assert that every registered invariant is either
+  open or closed
+- Proof mode tactics decompose `[∗ list]` and `[∗ map]` goals via
+  `big_sepM_insert`, `big_sepM_delete`, etc.
+
+## Main Definitions
+
+- `big_sepL` — iterated `∗` over a list with index: `[∗ list] i ↦ x ∈ l, Φ i x`
+- `big_sepM` — iterated `∗` over a finite map: `[∗ map] k ↦ v ∈ m, Φ k v`
+
+## Main Results
+
+- `big_sepL_nil`, `big_sepL_cons` — computation rules
+- `big_sepL_mono` — pointwise entailment lifts to the big sep
+- `big_sepM_empty`, `big_sepM_insert`, `big_sepM_delete` — map operations
+- `big_sepM_lookup_acc` — extract one entry with a restoration wand
+- `big_sepM_sep` — distribute `∗` over `[∗ map]`
+-/
+
+namespace Iris.BI
+
+open Iris.Algebra Iris.Std
+
+variable {PROP : Type _} [BI PROP]
+
+/-! ## Separating Conjunction Monoid -/
+
+/-- `sep` / `emp` form a monoid on any BI, enabling use of `bigOpL` and `bigOpM`. -/
+instance sepMonoid : Monoid PROP BIBase.sep (BIBase.emp : PROP) where
+  op_ne := by
+    -- non-expansiveness is inherited from the BI structure
+    simpa using (BI.sep_ne (PROP := PROP))
+  op_assoc := by
+    -- associativity follows from the derived bi-entailment
+    intro a b c
+    exact equiv_iff.mpr (sep_assoc (P := a) (Q := b) (R := c))
+  op_comm := by
+    -- commutativity follows from the derived bi-entailment
+    intro a b
+    exact equiv_iff.mpr (sep_comm (P := a) (Q := b))
+  op_left_id := by
+    -- left identity is `emp_sep` as a bi-entailment
+    intro a
+    exact equiv_iff.mpr (emp_sep (P := a))
+
+/-! ## List Big Sep -/
+
+/-- Iterated separating conjunction over a list with index.
+    `big_sepL Φ l = Φ 0 x₀ ∗ Φ 1 x₁ ∗ ⋯ ∗ Φ (n-1) xₙ₋₁` -/
+def big_sepL {A : Type _} (Φ : Nat → A → PROP) (l : List A) : PROP :=
+  bigOpL BIBase.sep BIBase.emp Φ l
+
+/-! ### List Computation Rules -/
+
+/-- Empty list gives `emp`. -/
+@[simp] theorem big_sepL_nil {A : Type _} (Φ : Nat → A → PROP) :
+    big_sepL Φ ([] : List A) = (BIBase.emp : PROP) := rfl
+
+/-- Cons unfolds to head `∗` tail. -/
+@[simp] theorem big_sepL_cons {A : Type _} (Φ : Nat → A → PROP) (x : A) (l : List A) :
+    big_sepL Φ (x :: l) = BIBase.sep (Φ 0 x) (big_sepL (fun n => Φ (n + 1)) l) := rfl
+
+/-- Singleton list gives just the element. -/
+theorem big_sepL_singleton {A : Type _} (Φ : Nat → A → PROP) (x : A) :
+    big_sepL Φ [x] ⊣⊢ Φ 0 x := by
+  -- reduce to the algebraic singleton lemma and translate equivalence
+  have h : big_sepL Φ [x] ≡ Φ 0 x := by
+    -- unfold and use the singleton simplification
+    simp [big_sepL]
+  exact (equiv_iff (P := big_sepL Φ [x]) (Q := Φ 0 x)).1 h
+
+/-! ### List Structural Lemmas -/
+
+/-- Pointwise entailment lifts to the iterated separating conjunction. -/
+theorem big_sepL_mono {A : Type _} {Φ Ψ : Nat → A → PROP} {l : List A}
+    (h : ∀ i x, l[i]? = some x → Φ i x ⊢ Ψ i x) :
+    big_sepL Φ l ⊢ big_sepL Ψ l := by
+  -- prove by list induction using `sep_mono`
+  induction l generalizing Φ Ψ with
+  | nil =>
+    -- both sides are `emp`
+    simp [big_sepL_nil]
+  | cons x xs ih =>
+    -- use monotonicity for head and tail
+    have hhead : Φ 0 x ⊢ Ψ 0 x := h 0 x rfl
+    have htail : ∀ i y, xs[i]? = some y → Φ (i + 1) y ⊢ Ψ (i + 1) y := by
+      -- shift indices for the tail
+      intro i y hget
+      exact h (i + 1) y hget
+    have ht : big_sepL (fun n => Φ (n + 1)) xs ⊢ big_sepL (fun n => Ψ (n + 1)) xs := ih htail
+    -- unfold the head and apply `sep_mono`
+    simpa [big_sepL_cons] using sep_mono hhead ht
+
+/-- Append distributes: `[∗ list](l₁ ++ l₂) ⊣⊢ [∗ list]l₁ ∗ [∗ list]l₂`. -/
+theorem big_sepL_app {A : Type _} (Φ : Nat → A → PROP) (l₁ l₂ : List A) :
+    big_sepL Φ (l₁ ++ l₂) ⊣⊢
+      BIBase.sep (big_sepL Φ l₁) (big_sepL (fun n => Φ (n + l₁.length)) l₂) := by
+  -- use the algebraic append lemma and translate equivalence
+  have h : big_sepL Φ (l₁ ++ l₂) ≡
+      BIBase.sep (big_sepL Φ l₁) (big_sepL (fun n => Φ (n + l₁.length)) l₂) := by
+    simpa [big_sepL] using
+      (BigOpL.append (op := BIBase.sep) (unit := (BIBase.emp : PROP)) Φ l₁ l₂)
+  exact equiv_iff.mp h
+
+/-- Distribute `∗` inside: `[∗ list](Φ ∗ Ψ) ⊣⊢ [∗ list]Φ ∗ [∗ list]Ψ`. -/
+theorem big_sepL_sep {A : Type _} (Φ Ψ : Nat → A → PROP) (l : List A) :
+    big_sepL (fun i x => BIBase.sep (Φ i x) (Ψ i x)) l ⊣⊢
+      BIBase.sep (big_sepL Φ l) (big_sepL Ψ l) := by
+  -- use the algebraic distributivity lemma and translate equivalence
+  have h : big_sepL (fun i x => BIBase.sep (Φ i x) (Ψ i x)) l ≡
+      BIBase.sep (big_sepL Φ l) (big_sepL Ψ l) := by
+    simpa [big_sepL] using
+      (BigOpL.op_distr (op := BIBase.sep) (unit := (BIBase.emp : PROP)) Φ Ψ l)
+  exact equiv_iff.mp h
+
+/-! ## Map Big Sep -/
+
+variable {K : Type _} {V : Type _}
+variable {M' : Type _ → Type _} [FiniteMap K M']
+
+/-- Iterated separating conjunction over a finite map.
+    `big_sepM Φ m = ∗_{(k,v) ∈ m} Φ k v` -/
+def big_sepM (Φ : K → V → PROP) (m : M' V) : PROP :=
+  BigOpM.bigOpM (op := BIBase.sep) (unit := (BIBase.emp : PROP)) Φ m
+
+/-! ## Notation -/
+
+syntax "[∗" "list]" ident " ↦ " ident " ∈ " term ", " term : term
+syntax "[∗" "map]" ident " ↦ " ident " ∈ " term ", " term : term
+
+macro_rules
+  | `(iprop([∗ list] $i ↦ $x ∈ $l, $P)) =>
+      ``(big_sepL (fun $i $x => iprop($P)) $l)
+  | `(iprop([∗ map] $k ↦ $v ∈ $m, $P)) =>
+      ``(big_sepM (fun $k $v => iprop($P)) $m)
+
+/-! ### Map Structural Lemmas -/
+
+/-- Distribute `∗` inside: `[∗ map](Φ ∗ Ψ) ⊣⊢ [∗ map]Φ ∗ [∗ map]Ψ`. -/
+theorem big_sepM_sep (Φ Ψ : K → V → PROP) (m : M' V) :
+    big_sepM (fun k v => BIBase.sep (Φ k v) (Ψ k v)) m ⊣⊢
+      BIBase.sep (big_sepM Φ m) (big_sepM Ψ m) := by
+  -- use the algebraic distributivity lemma and translate equivalence
+  have h : big_sepM (fun k v => BIBase.sep (Φ k v) (Ψ k v)) m ≡
+      BIBase.sep (big_sepM Φ m) (big_sepM Ψ m) := by
+    simpa [big_sepM] using
+      (BigOpM.op_distr (op := BIBase.sep) (unit := (BIBase.emp : PROP)) Φ Ψ m)
+  exact equiv_iff.mp h
+
+section
+variable [DecidableEq K] [FiniteMapLaws K M']
+
+/-! ### Map Computation Rules -/
+
+/-- Empty map gives `emp`. -/
+@[simp] theorem big_sepM_empty (Φ : K → V → PROP) :
+    big_sepM Φ (∅ : M' V) = (BIBase.emp : PROP) := by
+  -- unfold to the algebraic empty lemma
+  simp [big_sepM]
+
+section
+variable [DecidableEq V]
+
+/-- Insert into a map with a fresh key unfolds to entry `∗` rest. -/
+theorem big_sepM_insert (Φ : K → V → PROP) (m : M' V) (i : K) (x : V)
+    (h : get? m i = none) :
+    big_sepM Φ (insert m i x) ⊣⊢
+      BIBase.sep (Φ i x) (big_sepM Φ m) := by
+  -- use the algebraic insert lemma and translate equivalence
+  have h' : big_sepM Φ (insert m i x) ≡
+      BIBase.sep (Φ i x) (big_sepM Φ m) := by
+    simpa [big_sepM] using
+      (BigOpM.insert (op := BIBase.sep) (unit := (BIBase.emp : PROP)) Φ m i x h)
+  exact equiv_iff.mp h'
+
+/-- Delete from a map: `big_sepM m ⊣⊢ Φ k v ∗ big_sepM (delete k m)`. -/
+theorem big_sepM_delete (Φ : K → V → PROP) (m : M' V) (i : K) (x : V)
+    (h : get? m i = some x) :
+    big_sepM Φ m ⊣⊢ BIBase.sep (Φ i x) (big_sepM Φ (delete m i)) := by
+  -- use the algebraic delete lemma and translate equivalence
+  have h' : big_sepM Φ m ≡
+      BIBase.sep (Φ i x) (big_sepM Φ (delete m i)) := by
+    simpa [big_sepM] using
+      (BigOpM.delete (op := BIBase.sep) (unit := (BIBase.emp : PROP)) Φ m i x h)
+  exact equiv_iff.mp h'
+
+/-- Pointwise entailment lifts to the iterated map conjunction. -/
+theorem big_sepM_mono {Φ Ψ : K → V → PROP} {m : M' V}
+    (h : ∀ k v, get? m k = some v → Φ k v ⊢ Ψ k v) :
+    big_sepM Φ m ⊢ big_sepM Ψ m := by
+  -- strengthen induction to carry pointwise entailments
+  refine FiniteMapLaws.induction_on
+    (P := fun m' => (∀ k v, get? m' k = some v → Φ k v ⊢ Ψ k v) →
+      big_sepM Φ m' ⊢ big_sepM Ψ m') ?hemp ?hins m h
+  case hemp =>
+    -- empty map: both sides are `emp`
+    intro _
+    simp [big_sepM_empty]
+  case hins =>
+    intro i x m' hnone IH hmap
+    -- split the inserted map into head and tail
+    have hhead : Φ i x ⊢ Ψ i x := by
+      -- apply the pointwise hypothesis at the new key
+      exact hmap i x (by simp [FiniteMapLaws.get?_insert_same])
+    have htail : ∀ k v, get? m' k = some v → Φ k v ⊢ Ψ k v := by
+      -- restrict the pointwise hypothesis to the tail map
+      intro k v hk
+      by_cases hki : k = i
+      · subst hki; rw [hnone] at hk; cases hk
+      · have hne : i ≠ k := Ne.symm hki
+        have hk' : get? (insert m' i x) k = some v := by
+          simpa [FiniteMapLaws.get?_insert_ne m' i k x hne] using hk
+        exact hmap k v hk'
+    have ht : big_sepM Φ m' ⊢ big_sepM Ψ m' := IH htail
+    -- reassemble with `sep_mono`
+    refine (big_sepM_insert Φ m' i x hnone).1.trans ?_
+    refine (sep_mono hhead ht).trans ?_
+    exact (big_sepM_insert Ψ m' i x hnone).2
+
+/-- Extract one entry from the big sep and get a wand to put it back.
+    This is the key lemma for opening/closing invariants in `wsat`. -/
+theorem big_sepM_lookup_acc {Φ : K → V → PROP} {m : M' V} {i : K} {x : V}
+    (h : get? m i = some x) :
+    big_sepM Φ m ⊢ BIBase.sep (Φ i x) (BIBase.wand (Φ i x) (big_sepM Φ m)) := by
+  -- peel out the entry and repackage with a wand
+  have hdelete := big_sepM_delete Φ m i x h
+  refine hdelete.1.trans ?_
+  have hwand : big_sepM Φ (delete m i) ⊢ BIBase.wand (Φ i x) (big_sepM Φ m) := by
+    -- derive the wand from the reversed delete lemma
+    refine wand_intro ?_
+    exact sep_symm.trans hdelete.2
+  -- combine head and wand
+  exact sep_mono .rfl hwand
+
+/-- Distribute `▷` over the map big sep. -/
+theorem big_sepM_later {Φ : K → V → PROP} {m : M' V} [BIAffine PROP] :
+    BIBase.later (big_sepM Φ m) ⊢ big_sepM (fun k v => BIBase.later (Φ k v)) m := by
+  -- prove by map induction using `later_sep`
+  refine FiniteMapLaws.induction_on
+    (P := fun m' => BIBase.later (big_sepM Φ m') ⊢
+      big_sepM (fun k v => BIBase.later (Φ k v)) m') ?hemp ?hins m
+  case hemp =>
+    -- empty map: `▷ emp ⊢ emp`
+    simpa [big_sepM_empty] using (later_emp (PROP := PROP)).1
+  case hins =>
+    intro i x m' hnone IH
+    -- rewrite both sides using insertion and push `later` through `∗`
+    have hinsΦ := big_sepM_insert Φ m' i x hnone
+    have hinsΨ := big_sepM_insert (fun k v => BIBase.later (Φ k v)) m' i x hnone
+    refine (later_congr hinsΦ).1.trans ?_
+    refine (later_sep).1.trans ?_
+    refine (sep_mono .rfl IH).trans ?_
+    exact hinsΨ.2
+
+/-- Singleton map. -/
+theorem big_sepM_singleton (Φ : K → V → PROP) (i : K) (x : V) :
+    big_sepM Φ (FiniteMap.singleton i x : M' V) ⊣⊢ Φ i x := by
+  -- use the algebraic singleton lemma and translate equivalence
+  have h : big_sepM Φ (FiniteMap.singleton i x : M' V) ≡ Φ i x := by
+    simpa [big_sepM] using
+      (BigOpM.singleton (op := BIBase.sep) (unit := (BIBase.emp : PROP)) Φ i x)
+  exact equiv_iff.mp h
+
+/-- Union of disjoint maps. -/
+theorem big_sepM_union (Φ : K → V → PROP) (m₁ m₂ : M' V)
+    (h : m₁ ##ₘ m₂) :
+    big_sepM Φ (m₁ ∪ m₂) ⊣⊢
+      BIBase.sep (big_sepM Φ m₁) (big_sepM Φ m₂) := by
+  -- use the algebraic union lemma and translate equivalence
+  have h' : big_sepM Φ (m₁ ∪ m₂) ≡
+      BIBase.sep (big_sepM Φ m₁) (big_sepM Φ m₂) := by
+    simpa [big_sepM] using
+      (BigOpM.union (op := BIBase.sep) (unit := (BIBase.emp : PROP)) Φ m₁ m₂ h)
+  exact equiv_iff.mp h'
+
+end
+end
+
+end Iris.BI
diff --git a/src/Iris/Std.lean b/src/Iris/Std.lean
index 1b2f1422..faa95f44 100644
--- a/src/Iris/Std.lean
+++ b/src/Iris/Std.lean
@@ -10,3 +10,5 @@ import Iris.Std.Rewrite
 import Iris.Std.Tactic
 import Iris.Std.TC
 import Iris.Std.Try
+import Iris.Std.FiniteMap
+import Iris.Std.List
diff --git a/src/Iris/Std/FiniteMap.lean b/src/Iris/Std/FiniteMap.lean
new file mode 100644
index 00000000..4385cdae
--- /dev/null
+++ b/src/Iris/Std/FiniteMap.lean
@@ -0,0 +1,1388 @@
+/-
+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.Std.List
+
+/-! ## Abstract Finite Map Interface
+
+This file defines an abstract interface for finite maps, inspired by stdpp's `fin_maps`. -/
+
+namespace Iris.Std
+
+/-- The type `M` represents a finite map from keys of type `K` to values of type `V`. -/
+class FiniteMap (K : outParam (Type u)) (M : Type u' → Type _) where
+  /-- Lookup a key in the map, returning `none` if not present.
+      Corresponds to Rocq's `lookup`. -/
+  get? : M V → K → Option V
+  /-- Insert or update a key-value pair.
+      Corresponds to Rocq's `insert`. -/
+  insert : M V → K → V → M V
+  /-- Remove a key from the map.
+      Corresponds to Rocq's `delete`. -/
+  delete : M V → K → M V
+  /-- The empty map. -/
+  empty : M V
+  /-- Convert the map to a list of key-value pairs.
+      Corresponds to Rocq's `map_to_list`. -/
+  toList : M V → List (K × V)
+  /-- Construct a map from a list of key-value pairs.
+      Corresponds to Rocq's `list_to_map`. -/
+  ofList : List (K × V) → M V
+  /-- Fold over all key-value pairs in the map.
+      The order of folding depends on the internal representation.
+      Corresponds to Rocq's `map_fold`. -/
+  fold {A : Type u'} : (K → V → A → A) → A → M V → A
+
+export FiniteMap (get? insert delete toList ofList fold)
+
+namespace FiniteMap
+
+variable {K : Type u} {V : Type u'} {M : Type u' → Type _} [FiniteMap K M]
+
+/-- Empty map instance for `∅` notation. -/
+instance : EmptyCollection (M V) := ⟨empty⟩
+
+/-- Singleton map containing exactly one key-value pair.
+    Corresponds to Rocq's `{[ i := x ]}` notation. -/
+def singleton (k : K) (v : V) : M V := insert ∅ k v
+
+/-- Union of two maps (left-biased: values from `m₁` take precedence).
+    Corresponds to Rocq's `m₁ ∪ m₂`. -/
+def union (m₁ m₂ : M V) : M V:=
+  (toList m₁).foldl (fun acc (k, v) => insert acc k v) m₂
+
+instance : Union (M V):= ⟨union⟩
+
+/-- Two maps have disjoint domains.
+    Corresponds to Rocq's `map_disjoint`. -/
+def disjoint (m₁ m₂ : M V) : Prop := ∀ k, ¬((get? m₁ k).isSome ∧ (get? m₂ k).isSome)
+
+/-- Submap relation: `m₁` is a submap of `m₂` if every key-value pair in `m₁` is also in `m₂`.
+    Corresponds to Rocq's `map_subseteq`. -/
+def submap (m₁ m₂ : M V) : Prop := ∀ k v, get? m₁ k = some v → get? m₂ k = some v
+
+instance : HasSubset (M V) := ⟨submap⟩
+
+/-- Map a function over all values in the map.
+    Corresponds to Rocq's `fmap` (notation `f <$> m`). -/
+def map (f : V → V') : M V → (M V') :=
+  fun m => ofList ((toList m).map (fun (k, v) => (k, f v)))
+
+/-- Filter and map: apply a function that can optionally drop entries.
+    Corresponds to Rocq's `omap`. -/
+def filterMap (f : V → Option V') : M V → M V' :=
+  fun m => ofList ((toList m).filterMap (fun (k, v) => (f v).map (k, ·)))
+
+/-- Filter entries by a predicate on key-value pairs.
+    Corresponds to Rocq's `filter`. -/
+def filter (φ : K → V → Bool) : M V → M V :=
+  fun m => ofList ((toList m).filter (fun (k, v) => φ k v))
+
+/-- Zip two maps with a combining function.
+    Corresponds to Rocq's `map_zip_with`. -/
+def zipWith {V' : Type _} {V'' : Type _} (f : V → V' → V'') (m₁ : M V) (m₂ : M V') : M V'' :=
+  ofList ((toList m₁).filterMap (fun (k, v) =>
+    match get? m₂ k with
+    | some v' => some (k, f v v')
+    | none => none))
+
+/-- Zip two maps: combine values at matching keys into pairs.
+    This is `zipWith Prod.mk`.
+    Corresponds to Rocq's `map_zip`. -/
+def zip (m₁ : M V) (m₂ : M V') : M (V × V') :=
+  zipWith Prod.mk m₁ m₂
+
+/-- Membership: a key is in the map if it has a value. -/
+def mem (m : M V) (k : K) : Prop := (get? m k).isSome
+
+/-- Difference: remove all keys in `m₂` from `m₁`.
+    Corresponds to Rocq's `map_difference`. -/
+def difference (m₁ m₂ : M V) : M V :=
+  ofList ((toList m₁).filter (fun (k, _) => (get? m₂ k).isNone))
+
+instance : SDiff (M V) := ⟨difference⟩
+
+/-- Transform keys of a map using an injective function.
+    Corresponds to Rocq's `kmap`. -/
+def kmap {K' : Type u} {M' : Type u' → _} [FiniteMap K' M'] (f : K → K') (m : M V) : (M' V) :=
+  ofList ((toList m).map (fun (k, v) => (f k, v)))
+
+/-- Convert a list to a map with sequential natural number keys starting from `start`.
+    Corresponds to Rocq's `map_seq`. -/
+def map_seq [FiniteMap Nat M] (start : Nat) (l : List V) : M V :=
+  ofList (l.mapIdx (fun i v => (start + i, v)))
+
+/-- Check if a key is the first key in the map's `toList` representation.
+    Corresponds to Rocq's `map_first_key`: `∃ x, map_to_list m !! 0 = Some (i,x)`. -/
+def firstKey (m : M V) (i : K) : Prop :=
+  ∃ x, (toList m).head? = some (i, x)
+
+/-- Corresponds to Rocq's `map_Forall`. -/
+def Forall (P : K → V → Prop) (m : M V) : Prop :=
+  ∀ k v, get? m k = some v → P k v
+
+end FiniteMap
+
+/-- Notation for singleton map: `{[k := v]}` -/
+scoped syntax "{[" term " := " term "]}" : term
+
+scoped macro_rules
+  | `({[$k := $v]}) => `(FiniteMap.singleton $k $v)
+
+/-- Notation for map disjointness: `m₁ ##ₘ m₂` -/
+scoped infix:50 " ##ₘ " => FiniteMap.disjoint
+
+/-- Membership instance for finite maps: `k ∈ m` means the key `k` is in the map `m`. -/
+instance  {K : Type u} {M : Type u' → Type _}  [inst : FiniteMap K M] : Membership K (M V) :=
+  ⟨fun (m : M V) (k : K) => (inst.get? m k).isSome⟩
+
+/-- Laws that a finite map implementation must satisfy. -/
+class FiniteMapLaws (K : (outParam (Type u))) (M : Type u' → Type _)
+    [DecidableEq K] [FiniteMap K M] where
+  /-- Corresponds to Rocq's `map_eq`. -/
+  ext : ∀ (m₁ m₂ : M V), (∀ i, get? m₁ i = get? m₂ i) → m₁ = m₂
+  /-- Corresponds to Rocq's `lookup_empty`. -/
+  get?_empty : ∀ k, get? (∅ : M V) k = none
+  /-- Corresponds to Rocq's `lookup_insert_eq`. -/
+  get?_insert_same : ∀ (m : M V) k v, get? (insert m k v) k = some v
+  /-- Corresponds to Rocq's `lookup_insert_ne`. -/
+  get?_insert_ne : ∀ (m : M V) k k' v, k ≠ k' → get? (insert m k v) k' = get? m k'
+  /-- Corresponds to Rocq's `lookup_delete_eq`. -/
+  get?_delete_same : ∀ (m : M V) k, get? (delete m k) k = none
+  /-- Corresponds to Rocq's `lookup_delete_ne`. -/
+  get?_delete_ne : ∀ (m : M V) k k', k ≠ k' → get? (delete m k) k' = get? m k'
+  /-- Corresponds to Rocq's `lookup_union`. -/
+  get?_union : ∀ (m₁ m₂ : M V) k,
+    get? (m₁ ∪ m₂) k = (get? m₁ k).orElse (fun _ => get? m₂ k)
+  /-- Corresponds to Rocq's `lookup_difference`. -/
+  get?_difference : ∀ (m₁ m₂ : M V) k,
+    get? (m₁ \ m₂) k = if (get? m₂ k).isSome then none else get? m₁ k
+  /-- Corresponds to Rocq's implicit behavior of `list_to_map`. -/
+  ofList_nil : (ofList [] : M V) = ∅
+  /-- Corresponds to Rocq's implicit behavior of `list_to_map`. -/
+  ofList_cons : ∀ (k : K) (v : V) (l : List (K × V)),
+    (ofList ((k, v) :: l) : M V) = insert (ofList l) k v
+  /-- Corresponds to Rocq's `map_to_list_spec`. -/
+  toList_spec (m : M V) :
+    (toList m).Nodup ∧ (∀ i x, (i, x) ∈ toList m ↔ get? m i = some x)
+  /-- Corresponds to Rocq's `map_ind`. -/
+  induction_on {P : M V → Prop}
+    (hemp : P ∅)
+    (hins : ∀ i x m, get? m i = none → P m → P (insert m i x))
+    (m : M V) : P m
+
+/-- Self-referential extended laws. -/
+class FiniteMapLawsSelf (K : outParam (Type u)) (M : Type u' → Type _)
+    [DecidableEq K] [FiniteMap K M] [FiniteMapLaws K M] where
+  /-- toList of filterMap is related to filterMap over toList. -/
+  toList_filterMap : ∀ (m : M V) (f : V → Option V),
+    (toList (FiniteMap.filterMap (M := M) f m)).Perm
+      ((toList m).filterMap (fun kv => (f kv.2).map (kv.1, ·)))
+  /-- toList of filter is related to filter over toList. -/
+  toList_filter : ∀ (m : M V) (φ : K → V → Bool),
+    (toList (FiniteMap.filter (M := M) φ m)).Perm
+      ((toList m).filter (fun kv => φ kv.1 kv.2))
+
+/-- Laws for kmap operation. -/
+class FiniteMapKmapLaws (K : outParam (Type u)) (K' : outParam (Type u)) (M : Type u' → Type _) (M' : Type u' → Type _)
+    [DecidableEq K] [DecidableEq K'] [FiniteMap K M] [FiniteMap K' M']
+    [FiniteMapLaws K M] [FiniteMapLaws K' M'] where
+  /-- toList of kmap is related to mapping over toList.
+      Corresponds to Rocq's `map_to_list_kmap`. -/
+  toList_kmap : ∀ (f : K → K') (m : M V),
+    (∀ {x y}, f x = f y → x = y) →  -- f is injective
+    (toList (FiniteMap.kmap (M' := M') f m)).Perm
+      ((toList m).map (fun (k, v) => (f k, v)))
+
+/-- Laws for map_seq operation. -/
+class FiniteMapSeqLaws (M : Type u → Type _) [FiniteMap Nat M] [FiniteMapLaws Nat M] where
+  /-- toList of map_seq is related to zip with sequence.
+      Corresponds to Rocq's `map_to_list_seq`. -/
+  toList_map_seq : ∀ (start : Nat) (l : List V),
+    (toList (FiniteMap.map_seq start l : M V)).Perm
+      (l.mapIdx (fun i v => ((i + start), v)))
+
+export FiniteMapLaws (ext
+get?_empty
+get?_insert_same get?_insert_ne
+get?_delete_same get?_delete_ne
+ofList_nil ofList_cons
+toList_spec
+induction_on)
+
+export FiniteMapLawsSelf (toList_filterMap toList_filter)
+export FiniteMapKmapLaws (toList_kmap)
+export FiniteMapSeqLaws (toList_map_seq)
+
+namespace FiniteMapLaws
+
+variable {K : Type u} {V : Type u'} {M : Type u' → Type _}
+variable [DecidableEq K] [FiniteMap K M] [FiniteMapLaws K M]
+
+private theorem mem_of_get?_ofList (l : List (K × V)) (k : K) (v : V) :
+    get? (ofList l : M V) k = some v → (k, v) ∈ l := by
+  intro h
+  induction l with
+  | nil =>
+    simp [ofList_nil, get?_empty] at h
+  | cons kv kvs ih =>
+    rw [ofList_cons] at h
+    by_cases heq : kv.1 = k
+    · have eq_val : kv.2 = v := by
+        rw [heq, get?_insert_same] at h
+        exact Option.some.inj h
+      have eq_kv : kv = (k, v) := by
+        ext
+        · exact heq
+        · exact eq_val
+      rw [← eq_kv]
+      exact List.Mem.head _
+    · rw [get?_insert_ne _ _ _ _ heq] at h
+      have := ih h
+      exact List.Mem.tail _ this
+
+
+/-- Corresponds to Rocq's `lookup_insert`. -/
+theorem get?_insert (m : M V) (k k' : K) (v : V) :
+    get? (insert m k v) k' = if k = k' then some v else get? m k' := by
+  split
+  · next h => rw [h, get?_insert_same]
+  · next h => exact get?_insert_ne m k k' v h
+
+/-- Corresponds to Rocq's `lookup_delete`. -/
+theorem get?_delete (m : M V) (k k' : K) :
+    get? (delete m k) k' = if k = k' then none else get? m k' := by
+  split
+  · next h => rw [h, get?_delete_same]
+  · next h => exact get?_delete_ne m k k' h
+
+/-- Corresponds to Rocq's `insert_delete_eq`. -/
+theorem get?_insert_delete (m : M V) (k k' : K) (v : V) :
+    get? (insert (delete m k) k v) k' = get? (insert m k v) k' := by
+  by_cases h : k = k'
+  · simp [h, get?_insert_same]
+  · simp [get?_insert_ne _ _ _ _ h, get?_delete_ne _ _ _ h]
+
+/-- Corresponds to Rocq's `NoDup_map_to_list`. -/
+theorem nodup_toList (m : M V): (toList m).Nodup := by
+   apply (toList_spec m).1
+
+/-- If a list has no duplicates and the projection is injective on list elements,
+    then the mapped list has no duplicates. -/
+theorem List.Nodup.map_of_injective {α β : Type _} {l : List α} {f : α → β}
+    (hnodup : l.Nodup) (hinj : ∀ a b, a ∈ l → b ∈ l → f a = f b → a = b) :
+    (l.map f).Nodup := by
+  induction l with
+  | nil => exact List.nodup_nil
+  | cons x xs ih =>
+    rw [List.map_cons, List.nodup_cons]
+    rw [List.nodup_cons] at hnodup
+    constructor
+    · intro hx_in
+      rw [List.mem_map] at hx_in
+      obtain ⟨y, hy_mem, hy_eq⟩ := hx_in
+      have hx_mem : x ∈ x :: xs := List.mem_cons_self
+      have hy_mem' : y ∈ x :: xs := List.mem_cons_of_mem x hy_mem
+      have : x = y := hinj x y hx_mem hy_mem' hy_eq.symm
+      subst this
+      exact hnodup.1 hy_mem
+    · apply ih hnodup.2
+      intro a b ha hb
+      exact hinj a b (List.mem_cons_of_mem x ha) (List.mem_cons_of_mem x hb)
+
+/-- Keys of toList have no duplicates. -/
+theorem nodup_toList_keys (m : M V) : (toList m).map Prod.fst |>.Nodup := by
+  apply List.Nodup.map_of_injective (nodup_toList m)
+  intro ⟨k₁, v₁⟩ ⟨k₂, v₂⟩ h1 h2 heq
+  simp at heq
+  obtain ⟨_, hmem⟩ := toList_spec (M := M) (K := K) (V := V) m
+  have hv1 : get? m k₁ = some v₁ := (hmem k₁ v₁).mp h1
+  have hv2 : get? m k₂ = some v₂ := (hmem k₂ v₂).mp h2
+  rw [heq] at hv1
+  rw [hv1] at hv2
+  cases hv2
+  ext <;> simp [heq]
+
+/-- Corresponds to Rocq's `elem_of_map_to_list`. -/
+theorem mem_toList (m : M V) : ∀ k v, (k, v) ∈ toList m ↔ get? m k = some v := by
+  apply (toList_spec m).2
+
+/-- Corresponds to Rocq's `elem_of_list_to_map_2`. -/
+theorem mem_of_mem_ofList (l : List (K × V)) (i : K) (x : V) :
+    get? (ofList l : M V) i = some x → (i, x) ∈ l := by
+  induction l with
+  | nil =>
+    intro h
+    rw [ofList_nil, get?_empty] at h
+    cases h
+  | cons kv l ih =>
+    intro h
+    obtain ⟨k, v⟩ := kv
+    rw [ofList_cons] at h
+    rw [get?_insert] at h
+    split at h
+    · next heq =>
+        cases h
+        rw [← heq]
+        simp [List.mem_cons]
+    · next hne =>
+        have : (i, x) ∈ l := ih h
+        exact List.mem_cons_of_mem _ this
+
+/-- Corresponds to Rocq's `elem_of_list_to_map_1`. -/
+theorem mem_ofList_of_mem (l : List (K × V)) (i : K) (x : V) :
+    (l.map Prod.fst).Nodup → (i, x) ∈ l → get? (ofList l : M V) i = some x := by
+  intro hnodup hmem
+  induction l with
+  | nil =>
+    simp at hmem
+  | cons kv l ih =>
+    obtain ⟨k, v⟩ := kv
+    rw [List.map_cons, List.nodup_cons] at hnodup
+    simp [List.mem_cons] at hmem
+    cases hmem with
+    | inl heq =>
+      obtain ⟨rfl, rfl⟩ := heq
+      rw [ofList_cons, get?_insert_same]
+    | inr hmem' =>
+      obtain ⟨hk_notin, hnodup_tail⟩ := hnodup
+      have hi_in : i ∈ l.map Prod.fst := by
+        rw [List.mem_map]
+        exact ⟨(i, x), hmem', rfl⟩
+      have hne : k ≠ i := by
+        intro heq
+        subst heq
+        exact hk_notin hi_in
+      have : get? (ofList l : M V) i = some x := ih hnodup_tail hmem'
+      rw [ofList_cons, get?_insert_ne _ _ _ _ hne, this]
+
+/-- Corresponds to Rocq's `elem_of_list_to_map` -/
+theorem mem_ofList (l : List (K × V)) i x (hnodup : (l.map Prod.fst).Nodup):
+   (i,x) ∈ l ↔ get? (ofList l : M V) i = some x := by
+    constructor
+    apply mem_ofList_of_mem; exact hnodup
+    apply mem_of_mem_ofList
+
+/-- Corresponds to Rocq's `list_to_map_inj`. -/
+theorem ofList_injective [DecidableEq V] (l1 l2 : List (K × V)) :
+    (l1.map Prod.fst).Nodup → (l2.map Prod.fst).Nodup →
+    (ofList l1 : M V) = ofList l2 → l1.Perm l2 := by
+  intro hnodup1 hnodup2 heq
+  have hnodup1' : l1.Nodup := List.nodup_of_nodup_map_fst l1 hnodup1
+  have hnodup2' : l2.Nodup := List.nodup_of_nodup_map_fst l2 hnodup2
+  haveI : DecidableEq (K × V) := inferInstance
+  apply List.perm_of_nodup_of_mem_iff hnodup1' hnodup2'
+  intro ⟨i, x⟩
+  rw [mem_ofList (M := M) (K := K) l1 i x hnodup1,
+      mem_ofList (M := M) (K := K) l2 i x hnodup2]
+  rw [heq]
+
+/-- Coresponds to Rocq's `list_to_map_to_list` -/
+theorem ofList_toList (m : M V) :
+    ofList (toList m) = m := by
+  apply ext (K := K)
+  intro i
+  cases heq : get? m i
+  · cases heq' : get? (ofList (toList m) : M V) i
+    · rfl
+    · rename_i val
+      have hmem : (i, val) ∈ toList m :=
+        (mem_ofList (M := M) (K := K) (toList m) i val (nodup_toList_keys m)).mpr heq'
+      have : get? m i = some val := (mem_toList m i val).mp hmem
+      rw [heq] at this
+      exact Option.noConfusion this
+  · rename_i val
+    have hmem : (i, val) ∈ toList m := (mem_toList m i val).mpr heq
+    have : get? (ofList (toList m) : M V) i = some val :=
+      (mem_ofList (M := M) (K := K) (toList m) i val (nodup_toList_keys m)).mp hmem
+    rw [this]
+
+  /-- Corresponds to Rocq's `map_to_list_to_map`. -/
+ theorem toList_ofList [DecidableEq V] : ∀ (l : List (K × V)), (l.map Prod.fst).Nodup →
+    (toList (ofList l : M V)).Perm l := by
+  intro l hnodup
+  apply ofList_injective (M := M) (K:=K)
+  · exact nodup_toList_keys (M := M) (K := K) (V := V) (ofList l)
+  · exact hnodup
+  rw [ofList_toList]
+
+/-- Two maps with the same get? behavior have permutation-equivalent toLists. -/
+theorem toList_perm_of_get?_eq [DecidableEq V] {m₁ m₂ : M V}
+    (h : ∀ k, get? m₁ k = get? m₂ k) : (toList m₁).Perm (toList m₂) := by
+  have hnodup₁ := nodup_toList (M := M) (K := K) (V := V) m₁
+  have hnodup₂ := nodup_toList (M := M) (K := K) (V := V) m₂
+  have hmem : ∀ kv, kv ∈ toList m₁ ↔ kv ∈ toList m₂ := by
+    intro ⟨k, v⟩
+    rw [mem_toList m₁ k v, mem_toList m₂ k v, h]
+  exact List.perm_of_nodup_of_mem_iff hnodup₁ hnodup₂ hmem
+
+/-- toList of insert and insert-after-delete are permutations of each other. -/
+theorem toList_insert_delete [DecidableEq V] (m : M V) (k : K) (v : V) :
+    (toList (insert m k v)).Perm (toList (insert (delete m k) k v)) :=
+  toList_perm_of_get?_eq (fun k' => (get?_insert_delete m k k' v).symm)
+
+/-- Singleton lookup for equal keys.
+    Corresponds to Rocq's `get?_singleton_same`. -/
+theorem get?_singleton_same (k : K) (v : V) :
+    get? ({[k := v]} : M V) k = some v := by
+  simp [FiniteMap.singleton, get?_insert_same]
+
+/-- Singleton lookup for different keys.
+    Corresponds to Rocq's `get?_singleton_ne`. -/
+theorem get?_singleton_ne (k k' : K) (v : V) (h : k ≠ k') :
+    get? ({[k := v]} : M V) k' = none := by
+  simp [FiniteMap.singleton, get?_insert_ne _ _ _ _ h, get?_empty]
+
+/-- Singleton lookup general case.
+    Corresponds to Rocq's `get?_singleton`. -/
+theorem get?_singleton (k k' : K) (v : V) :
+    get? ({[k := v]} : M V) k' = if k = k' then some v else none := by
+  split
+  · next h => rw [h, get?_singleton_same]
+  · next h => exact get?_singleton_ne k k' v h
+
+/-- Insert is idempotent for the same key-value.
+    Corresponds to Rocq's `insert_insert_eq`. -/
+theorem insert_insert (m : M V) (k : K) (v v' : V) :
+    get? (insert (insert m k v) k v') = get? (insert m k v' : M V) := by
+  funext k'
+  by_cases h : k = k'
+  · simp [h, get?_insert_same]
+  · simp [get?_insert_ne _ _ _ _ h]
+
+/-- Deleting from empty is empty.
+    Corresponds to Rocq's `delete_empty_eq`. -/
+theorem delete_empty_eq (k : K) :
+    get? (delete (∅ : M V) k) = get? (∅ : M V) := by
+  funext k'
+  by_cases h : k = k'
+  · simp [h, get?_delete_same, get?_empty]
+  · simp [get?_delete_ne _ _ _ h, get?_empty]
+
+/-- Corresponds to Rocq's `map_empty_subseteq`. -/
+theorem empty_subset (m : M V) : (∅ : M V) ⊆ m := by
+  intro k v h
+  simp [get?_empty] at h
+
+/-- Corresponds to Rocq's `map_disjoint_empty_l`. -/
+theorem disjoint_empty_left (m : M V) : (∅ : M V) ##ₘ m := by
+  intro k ⟨h₁, _⟩
+  simp [get?_empty] at h₁
+
+/-- Corresponds to Rocq's `lookup_insert_Some`. -/
+theorem get?_insert_some (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
+  rw [get?_insert]
+  split <;> simp_all
+
+/-- Corresponds to Rocq's `lookup_insert_is_Some`. -/
+theorem get?_insert_isSome (m : M V) (i j : K) (x : V) :
+    (get? (insert m i x) j).isSome ↔ i = j ∨ (i ≠ j ∧ (get? m j).isSome) := by
+  rw [get?_insert]
+  split <;> simp_all
+
+/-- Corresponds to Rocq's `lookup_insert_None`. -/
+theorem get?_insert_none (m : M V) (i j : K) (x : V) :
+    get? (insert m i x) j = none ↔ get? m j = none ∧ i ≠ j := by
+  rw [get?_insert]
+  split <;> simp_all
+
+/-- Corresponds to Rocq's `lookup_insert_rev`. -/
+theorem get?_insert_rev (m : M V) (i : K) (x y : V) :
+    get? (insert m i x) i = some y → x = y := by
+  simp [get?_insert_same]
+
+/-- Corresponds to Rocq's `insert_id`. -/
+theorem insert_get? (m : M V) (i : K) (x : V) :
+    get? m i = some x → (∀ k, get? (insert m i x) k = get? m k) := by
+  intro h k
+  by_cases hk : i = k
+  · subst hk; simp only [get?_insert_same, h]
+  · simp [get?_insert_ne _ _ _ _ hk]
+
+/-- Corresponds to Rocq's `lookup_delete_Some`. -/
+theorem get?_delete_some (m : M V) (i j : K) (y : V) :
+    get? (delete m i) j = some y ↔ i ≠ j ∧ get? m j = some y := by
+  rw [get?_delete]
+  split <;> simp_all
+
+/-- Corresponds to Rocq's `lookup_delete_is_Some`. -/
+theorem get?_delete_isSome (m : M V) (i j : K) :
+    (get? (delete m i) j).isSome ↔ i ≠ j ∧ (get? m j).isSome := by
+  rw [get?_delete]
+  split <;> simp_all
+
+/-- Corresponds to Rocq's `lookup_delete_None`. -/
+theorem get?_delete_none (m : M V) (i j : K) :
+    get? (delete m i) j = none ↔ i = j ∨ get? m j = none := by
+  rw [get?_delete]
+  split <;> simp_all
+
+/-- Corresponds to Rocq's `insert_delete_id`. -/
+theorem insert_delete_cancel (m : M V) (i : K) (x : V) :
+    get? m i = some x → insert (delete m i) i x = m := by
+  intro h
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro j
+  by_cases hij : i = j
+  · subst hij
+    simp [get?_insert_same, h]
+  · simp [get?_insert_ne _ _ _ _ hij, get?_delete_ne _ _ _ hij]
+
+  /-- Corresponds to Rocq's `map_to_list_empty`. -/
+theorem toList_empty : toList (∅ : M V) = [] := by
+  apply List.eq_nil_iff_forall_not_mem.mpr
+  intro ⟨i, x⟩ hmem
+  rw [mem_toList] at hmem
+  rw [get?_empty] at hmem
+  exact Option.noConfusion hmem
+
+  /-- Corresponds to Rocq's `map_to_list_insert`. -/
+theorem toList_insert [DecidableEq V] : ∀ (m : M V) k v, get? m k = none →
+    (toList (insert m k v)).Perm ((k, v) :: toList m) := by
+  intro m k v hk_none
+  apply ofList_injective (M := M) (K := K)
+  · exact nodup_toList_keys (insert m k v)
+  · rw [List.map_cons, List.nodup_cons]
+    constructor
+    · intro hk_in
+      rw [List.mem_map] at hk_in
+      obtain ⟨⟨k', v'⟩, hmem, hk_eq⟩ := hk_in
+      simp at hk_eq
+      subst hk_eq
+      have : get? m k' = some v' := (mem_toList m k' v').mp hmem
+      rw [hk_none] at this
+      exact Option.noConfusion this
+    · exact nodup_toList_keys m
+  · rw [ofList_toList]
+    rw [ofList_cons, ofList_toList]
+
+/-- Corresponds to Rocq's `map_to_list_delete`. -/
+theorem toList_delete [DecidableEq V] (m : M V) (k : K) (v : V) (h : get? m k = some v) :
+    (toList m).Perm ((k, v) :: toList (delete m k)) := by
+  have heq : toList m = toList (insert (delete m k) k v) := by
+    rw [insert_delete_cancel m k v h]
+  rw [heq]
+  apply toList_insert
+  exact get?_delete_same m k
+
+
+/-- Corresponds to Rocq's `delete_insert_id`. -/
+theorem delete_insert_cancel (m : M V) (i : K) (x : V) :
+    get? m i = none → delete (insert m i x) i = m := by
+  intro h
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro j
+  by_cases hij : i = j
+  · subst hij
+    simp [get?_delete_same, h]
+  · simp [get?_delete_ne _ _ _ hij, get?_insert_ne _ _ _ _ hij]
+
+/-- Empty map is characterized by all lookups returning none. -/
+theorem eq_empty_iff (m : M V) : m = ∅ ↔ ∀ k, get? m k = none := by
+  constructor
+  · intro h k
+    rw [h, get?_empty]
+  · intro h
+    apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+    intro k
+    rw [h, get?_empty]
+
+/-- Corresponds to Rocq's `delete_delete_eq`. -/
+theorem delete_delete_same (m : M V) (i : K) :
+    delete (delete m i) i = delete m i := by
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro j
+  by_cases hij : i = j
+  · subst hij
+    simp [get?_delete_same]
+  · simp [get?_delete_ne _ _ _ hij]
+
+/-- Corresponds to Rocq's `delete_delete`. -/
+theorem delete_delete_comm (m : M V) (i j : K) :
+    delete (delete m i) j = delete (delete m j) i := by
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro k
+  by_cases hik : i = k <;> by_cases hjk : j = k <;> simp [get?_delete, *]
+
+/-- Corresponds to Rocq's `delete_insert_ne`. -/
+theorem delete_insert_of_ne (m : M V) (i j : K) (x : V) :
+    i ≠ j → delete (insert m i x) j = insert (delete m j) i x := by
+  intro hij
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro k
+  by_cases hik : i = k <;> by_cases hjk : j = k
+  · subst hik hjk; exact absurd rfl hij
+  · subst hik; simp [get?_insert, get?_delete, hjk]
+  · subst hjk; simp [get?_insert, get?_delete, hik]
+  · simp [get?_insert, get?_delete, hik, hjk]
+
+/-- Corresponds to Rocq's `insert_delete_eq`. -/
+theorem insert_delete (m : M V) (i : K) (x : V) :
+    insert (delete m i) i x = insert m i x := by
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro j
+  by_cases hij : i = j
+  · subst hij
+    simp [get?_insert_same]
+  · simp [get?_insert_ne _ _ _ _ hij, get?_delete_ne _ _ _ hij]
+
+/-- Corresponds to Rocq's `insert_insert`. -/
+theorem insert_insert_comm (m : M V) (i j : K) (x y : V) :
+    i ≠ j → insert (insert m i x) j y = insert (insert m j y) i x := by
+  intro hij
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro k
+  by_cases hik : i = k <;> by_cases hjk : j = k
+  · subst hik hjk; exact absurd rfl hij
+  · subst hik; simp [get?_insert, hjk]
+  · subst hjk; simp [get?_insert, hik]
+  · simp [get?_insert, hik, hjk]
+
+/-- Corresponds to Rocq's `insert_insert_eq`. -/
+theorem insert_insert_same (m : M V) (i : K) (x y : V) :
+    insert (insert m i x) i y = insert m i y := by
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro j
+  by_cases hij : i = j
+  · subst hij
+    simp [get?_insert_same]
+  · simp [get?_insert_ne _ _ _ _ hij]
+
+/-- Corresponds to Rocq's `delete_empty`. -/
+theorem delete_empty_eq' (i : K) :
+    delete (∅ : M V) i = ∅ := by
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro j
+  simp [get?_delete, get?_empty]
+
+/-- Corresponds to Rocq's `delete_id`. -/
+theorem delete_of_get? (m : M V) (i : K) :
+    get? m i = none → delete m i = m := by
+  intro h
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro j
+  by_cases hij : i = j
+  · subst hij
+    simp [get?_delete_same, h]
+  · simp [get?_delete_ne _ _ _ hij]
+
+/-- Corresponds to Rocq's `insert_id`. -/
+theorem insert_get?' (m : M V) (i : K) (x : V) :
+    get? m i = some x → insert m i x = m := by
+  intro h
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro j
+  by_cases hij : i = j
+  · subst hij
+    simp [get?_insert_same, h]
+  · simp [get?_insert_ne _ _ _ _ hij]
+
+omit [DecidableEq K] [FiniteMapLaws K M] in
+/-- Corresponds to Rocq's `insert_empty`. -/
+theorem insert_empty (i : K) (x : V) :
+    insert (∅ : M V) i x = {[i := x]} := by
+  rfl
+
+/-- Corresponds to Rocq's `insert_non_empty`. -/
+theorem insert_ne_empty (m : M V) (i : K) (x : V) :
+    insert m i x ≠ ∅ := by
+  intro h
+  have := eq_empty_iff (insert m i x) |>.mp h i
+  simp [get?_insert_same] at this
+
+/-- Corresponds to Rocq's `delete_subseteq`. -/
+theorem delete_subset_self (m : M V) (i : K) : delete m i ⊆ m := by
+  intro k v h
+  by_cases hik : i = k
+  · subst hik
+    simp [get?_delete_same] at h
+  · simp [get?_delete_ne _ _ _ hik] at h
+    exact h
+
+/-- Corresponds to Rocq's `delete_subset`. -/
+theorem delete_subset_of_mem (m : M V) (i : K) (v : V) :
+    get? m i = some v → delete m i ⊆ m ∧ delete m i ≠ m := by
+  intro hi
+  constructor
+  · exact delete_subset_self m i
+  · intro heq
+    have : get? (delete m i) i = get? m i := by rw [heq]
+    simp [get?_delete_same, hi] at this
+
+/-- Corresponds to Rocq's `insert_subseteq`. -/
+theorem subset_insert (m : M V) (i : K) (x : V) :
+    get? m i = none → m ⊆ insert m i x := by
+  intro hi k v hk
+  by_cases hik : i = k
+  · subst hik
+    simp [hi] at hk
+  · simp [get?_insert_ne _ _ _ _ hik, hk]
+
+/-- Corresponds to Rocq's `insert_subset`. -/
+theorem subset_insert_of_not_mem (m : M V) (i : K) (x : V) :
+    get? m i = none → m ⊆ insert m i x ∧ m ≠ insert m i x := by
+  intro hi
+  constructor
+  · exact subset_insert m i x hi
+  · intro heq
+    have h2 : get? (insert m i x) i = some x := get?_insert_same m i x
+    rw [← heq] at h2
+    rw [hi] at h2
+    exact Option.noConfusion h2
+
+/-- Corresponds to Rocq's `delete_mono`. -/
+theorem delete_subset_delete (m₁ m₂ : M V) (i : K) :
+    m₁ ⊆ m₂ → delete m₁ i ⊆ delete m₂ i := by
+  intro hsub k v hk
+  by_cases hik : i = k
+  · subst hik
+    simp [get?_delete_same] at hk
+  · simp [get?_delete_ne _ _ _ hik] at hk ⊢
+    exact hsub k v hk
+
+/-- Corresponds to Rocq's `insert_mono`. -/
+theorem insert_subset_insert (m₁ m₂ : M V) (i : K) (x : V) :
+    m₁ ⊆ m₂ → insert m₁ i x ⊆ insert m₂ i x := by
+  intro hsub k v hk
+  by_cases hik : i = k
+  · subst hik
+    simp [get?_insert_same] at hk ⊢
+    exact hk
+  · simp [get?_insert_ne _ _ _ _ hik] at hk ⊢
+    exact hsub k v hk
+
+/-- Corresponds to Rocq's `map_non_empty_singleton`. -/
+theorem singleton_ne_empty (i : K) (x : V) :
+    {[i := x]} ≠ (∅ : M V) := by
+  exact insert_ne_empty ∅ i x
+
+/-- Corresponds to Rocq's `delete_singleton_eq`. -/
+theorem delete_singleton_same (i : K) (x : V) :
+    delete ({[i := x]} : M V) i = ∅ := by
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro j
+  simp [FiniteMap.singleton, get?_delete, get?_insert, get?_empty]
+
+/-- Corresponds to Rocq's `delete_singleton_ne`. -/
+theorem delete_singleton_of_ne (i j : K) (x : V) :
+    i ≠ j → delete ({[j := x]} : M V) i = {[j := x]} := by
+  intro hij
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro k
+  simp [FiniteMap.singleton, get?_delete, get?_insert, get?_empty]
+  intro hik
+  intro hjk
+  subst hik hjk
+  exact hij rfl
+
+/-- Corresponds to Rocq's `map_Forall_to_list`. -/
+theorem forall_iff_toList (P : K → V → Prop) (m : M V) :
+    FiniteMap.Forall P m ↔ ∀ kv ∈ toList m, P kv.1 kv.2 := by
+  constructor
+  · intro hfa kv hmem
+    have := (mem_toList m kv.1 kv.2).mp hmem
+    exact hfa kv.1 kv.2 this
+  · intro hlist k v hget
+    have := (mem_toList m k v).mpr hget
+    exact hlist (k, v) this
+
+/-- Corresponds to Rocq's `map_Forall_empty`. -/
+theorem forall_empty (P : K → V → Prop) : FiniteMap.Forall P (∅ : M V) := by
+  intro k v h
+  simp [get?_empty] at h
+
+omit [DecidableEq K] [FiniteMapLaws K M] in
+/-- Corresponds to Rocq's `map_Forall_impl`. -/
+theorem forall_mono (P Q : K → V → Prop) (m : M V) :
+    FiniteMap.Forall P m → (∀ k v, P k v → Q k v) → FiniteMap.Forall Q m := by
+  intro hp himpl k v hget
+  exact himpl k v (hp k v hget)
+
+/-- Corresponds to Rocq's `map_Forall_insert_1_1`. -/
+theorem forall_insert_of_forall (P : K → V → Prop) (m : M V) (i : K) (x : V) :
+    FiniteMap.Forall P (insert m i x) → P i x := by
+  intro hfa
+  exact hfa i x (get?_insert_same m i x)
+
+/-- Corresponds to Rocq's `map_Forall_insert_1_2`. -/
+theorem forall_of_forall_insert (P : K → V → Prop) (m : M V) (i : K) (x : V) :
+    get? m i = none → FiniteMap.Forall P (insert m i x) → FiniteMap.Forall P m := by
+  intro hi hfa k v hget
+  by_cases hik : i = k
+  · subst hik
+    simp [hi] at hget
+  · have : get? (insert m i x) k = some v := by
+      simp [get?_insert_ne _ _ _ _ hik, hget]
+    exact hfa k v this
+
+/-- Corresponds to Rocq's `map_Forall_insert_2`. -/
+theorem forall_insert (P : K → V → Prop) (m : M V) (i : K) (x : V) :
+    P i x → FiniteMap.Forall P m → FiniteMap.Forall P (insert m i x) := by
+  intro hpix hfa k v hget
+  by_cases hik : i = k
+  · subst hik
+    simp [get?_insert_same] at hget
+    rw [← hget]
+    exact hpix
+  · simp [get?_insert_ne _ _ _ _ hik] at hget
+    exact hfa k v hget
+
+/-- Corresponds to Rocq's `map_Forall_insert`. -/
+theorem forall_insert_iff (P : K → V → Prop) (m : M V) (i : K) (x : V) :
+    get? m i = none → (FiniteMap.Forall P (insert m i x) ↔ P i x ∧ FiniteMap.Forall P m) := by
+  intro hi
+  constructor
+  · intro hfa
+    exact ⟨forall_insert_of_forall P m i x hfa, forall_of_forall_insert P m i x hi hfa⟩
+  · intro ⟨hpix, hfa⟩
+    exact forall_insert P m i x hpix hfa
+
+/-- Corresponds to Rocq's `map_Forall_singleton`. -/
+theorem forall_singleton (P : K → V → Prop) (i : K) (x : V) :
+    FiniteMap.Forall P ({[i := x]} : M V) ↔ P i x := by
+  constructor
+  · intro hfa
+    exact hfa i x (get?_singleton_same i x)
+  · intro hpix k v hget
+    simp [get?_singleton] at hget
+    obtain ⟨rfl, rfl⟩ := hget
+    exact hpix
+
+/-- Corresponds to Rocq's `map_Forall_delete`. -/
+theorem forall_delete (P : K → V → Prop) (m : M V) (i : K) :
+    FiniteMap.Forall P m → FiniteMap.Forall P (delete m i) := by
+  intro hfa k v hget
+  by_cases hik : i = k
+  · subst hik
+    simp [get?_delete_same] at hget
+  · simp [get?_delete_ne _ _ _ hik] at hget
+    exact hfa k v hget
+
+omit [DecidableEq K] [FiniteMapLaws K M] in
+/-- Corresponds to Rocq's `map_disjoint_spec`. -/
+theorem disjoint_iff (m₁ m₂ : M V) :
+    m₁ ##ₘ m₂ ↔ ∀ k, get? m₁ k = none ∨ get? m₂ k = none := by
+  constructor
+  · intro hdisj k
+    by_cases h1 : (get? m₁ k).isSome
+    · by_cases h2 : (get? m₂ k).isSome
+      · exact absurd ⟨h1, h2⟩ (hdisj k)
+      · simp only [Option.not_isSome_iff_eq_none] at h2
+        exact Or.inr h2
+    · simp only [Option.not_isSome_iff_eq_none] at h1
+      exact Or.inl h1
+  · intro h k ⟨hs1, hs2⟩
+    cases h k with
+    | inl h1 => simp [h1] at hs1
+    | inr h2 => simp [h2] at hs2
+
+/-- Corresponds to Rocq's `map_disjoint_insert_l`. -/
+theorem disjoint_insert_left (m₁ m₂ : M V) (i : K) (x : V) :
+    get? m₂ i = none →
+    m₁ ##ₘ m₂ →
+    insert m₁ i x ##ₘ m₂ := by
+  intro hi hdisj k ⟨hs1, hs2⟩
+  by_cases hik : i = k
+  · subst hik
+    simp [hi] at hs2
+  · simp [get?_insert_ne _ _ _ _ hik] at hs1
+    exact hdisj k ⟨hs1, hs2⟩
+
+/-- Corresponds to Rocq's `map_disjoint_insert_r`. -/
+theorem disjoint_insert_right (m₁ m₂ : M V) (i : K) (x : V) :
+    get? m₁ i = none →
+    m₁ ##ₘ m₂ →
+    m₁ ##ₘ insert m₂ i x := by
+  intro hi hdisj k ⟨hs1, hs2⟩
+  by_cases hik : i = k
+  · subst hik
+    simp [hi] at hs1
+  · simp [get?_insert_ne _ _ _ _ hik] at hs2
+    exact hdisj k ⟨hs1, hs2⟩
+
+/-- Corresponds to Rocq's `map_disjoint_delete_l`. -/
+theorem disjoint_delete_left (m₁ m₂ : M V) (i : K) :
+    m₁ ##ₘ m₂ → delete m₁ i ##ₘ m₂ := by
+  intro hdisj k ⟨hs1, hs2⟩
+  by_cases hik : i = k
+  · subst hik
+    simp [get?_delete_same] at hs1
+  · simp [get?_delete_ne _ _ _ hik] at hs1
+    exact hdisj k ⟨hs1, hs2⟩
+
+/-- Corresponds to Rocq's `map_disjoint_delete_r`. -/
+theorem disjoint_delete_right (m₁ m₂ : M V) (i : K) :
+    m₁ ##ₘ m₂ → m₁ ##ₘ delete m₂ i := by
+  intro hdisj k ⟨hs1, hs2⟩
+  by_cases hik : i = k
+  · subst hik
+    simp [get?_delete_same] at hs2
+  · simp [get?_delete_ne _ _ _ hik] at hs2
+    exact hdisj k ⟨hs1, hs2⟩
+
+/-- Corresponds to Rocq's `map_disjoint_singleton_l`. -/
+theorem disjoint_singleton_left (m : M V) (i : K) (x : V) :
+    get? m i = none → {[i := x]} ##ₘ m := by
+  intro hi k ⟨hs1, hs2⟩
+  by_cases hik : i = k
+  · subst hik
+    simp [hi] at hs2
+  · simp [FiniteMap.singleton, get?_insert_ne _ _ _ _ hik, get?_empty] at hs1
+
+/-- Corresponds to Rocq's `map_disjoint_singleton_r`. -/
+theorem disjoint_singleton_right (m : M V) (i : K) (x : V) :
+    get? m i = none → m ##ₘ {[i := x]} := by
+  intro hi k ⟨hs1, hs2⟩
+  by_cases hik : i = k
+  · subst hik
+    simp [hi] at hs1
+  · simp [FiniteMap.singleton, get?_insert_ne _ _ _ _ hik, get?_empty] at hs2
+
+/-- toList of map (fmap) is a permutation of mapping over toList. -/
+theorem toList_map [DecidableEq V'] : ∀ (m : M V) (f : V → V'),
+  (toList (FiniteMap.map f m)).Perm
+      ((toList m).map (fun kv => (kv.1, f kv.2))) := by
+  intro m f
+  simp only [FiniteMap.map]
+  apply toList_ofList
+  simp only [List.map_map]
+  show ((toList m).map (fun x => x.1)).Nodup
+  exact nodup_toList_keys m
+
+/-- Lookup in a mapped map. -/
+theorem get?_map [DecidableEq V] {V' : Type _} [DecidableEq V'] (f : V → V') (m : M V) (k : K) :
+    get? (FiniteMap.map f m) k = (get? m k).map f := by
+  simp only [FiniteMap.map]
+  by_cases h : ∃ v, get? m k = some v
+  · obtain ⟨v, hv⟩ := h
+    have hmem : (k, v) ∈ toList m := (mem_toList m k v).mpr hv
+    have hmem' : (k, f v) ∈ (toList m).map (fun (ki, vi) => (ki, f vi)) := by
+      rw [List.mem_map]
+      exact ⟨(k, v), hmem, rfl⟩
+    have hnodup : ((toList m).map (fun (ki, vi) => (ki, f vi))).map Prod.fst |>.Nodup := by
+      simp only [List.map_map]
+      show ((toList m).map Prod.fst).Nodup
+      exact nodup_toList_keys m
+    have := (mem_ofList (M := M) _ k (f v) hnodup).mp hmem'
+    simp [hv, this]
+  · have hk : get? m k = none := by
+      cases hm : get? m k
+      · rfl
+      · exfalso; apply h; exact ⟨_, hm⟩
+    simp [hk]
+    cases h' : get? (ofList ((toList m).map (fun (ki, vi) => (ki, f vi))) : M V') k
+    · rfl
+    · rename_i v'
+      have hnodup : ((toList m).map (fun (ki, vi) => (ki, f vi))).map Prod.fst |>.Nodup := by
+        simp only [List.map_map]
+        show ((toList m).map Prod.fst).Nodup
+        exact nodup_toList_keys m
+      have hmem : (k, v') ∈ (toList m).map (fun (ki, vi) => (ki, f vi)) :=
+        (mem_ofList (M := M) (V := V') _ k v' hnodup).mpr h'
+      rw [List.mem_map] at hmem
+      obtain ⟨⟨k', v''⟩, hmem', heq⟩ := hmem
+      simp at heq
+      cases heq
+      rename_i heq_k heq_v
+      have : get? m k' = some v'' := (mem_toList m k' v'').mp hmem'
+      rw [heq_k, hk] at this
+      cases this
+
+omit [DecidableEq K] in
+/-- filterMap preserves Nodup on keys. -/
+private theorem nodup_map_fst_filterMap
+    (l : List (K × V)) (g : K → V → Option (K × V')) :
+    (l.map Prod.fst).Nodup →
+    (∀ ki vi k' v', g ki vi = some (k', v') → k' = ki) →
+    ((l.filterMap (fun (ki, vi) => g ki vi)).map Prod.fst).Nodup := by
+  intro h_nodup h_preserve_key
+  have aux : ∀ (k_target : K) (l' : List (K × V)),
+      k_target ∈ (l'.filterMap (fun (ki, vi) => g ki vi)).map Prod.fst →
+      k_target ∈ l'.map Prod.fst := by
+    intro k_target l'
+    induction l' with
+    | nil => simp
+    | cons kv' tail' ih_aux =>
+      obtain ⟨k'', v''⟩ := kv'
+      intro hmem_filter
+      simp only [List.filterMap] at hmem_filter
+      cases hg' : g k'' v'' with
+      | none =>
+        simp only [hg'] at hmem_filter
+        exact List.mem_cons_of_mem k'' (ih_aux hmem_filter)
+      | some res' =>
+        obtain ⟨k''', v'''⟩ := res'
+        have : k''' = k'' := h_preserve_key k'' v'' k''' v''' hg'
+        subst this
+        simp only [hg', List.map_cons, List.mem_cons] at hmem_filter
+        rw [List.map_cons, List.mem_cons]
+        cases hmem_filter with
+        | inl heq => left; exact heq
+        | inr hmem' => right; exact ih_aux hmem'
+  induction l with
+  | nil => simp
+  | cons kv tail ih =>
+    obtain ⟨k, v⟩ := kv
+    rw [List.map_cons, List.nodup_cons] at h_nodup
+    simp only [List.filterMap]
+    cases hg : g k v with
+    | none =>
+      exact ih h_nodup.2
+    | some res =>
+      obtain ⟨k', v'⟩ := res
+      have hk_eq : k' = k := h_preserve_key k v k' v' hg
+      rw [List.map_cons, List.nodup_cons]
+      constructor
+      · intro hmem
+        rw [hk_eq] at hmem
+        apply h_nodup.1
+        exact aux k tail hmem
+      · exact ih h_nodup.2
+
+/-- Lookup in zipWith. -/
+theorem get?_zipWith [DecidableEq V] [DecidableEq V'] [DecidableEq V'']
+    (f : V → V' → V'') (m1 : M V) (m2 : M V') (k : K) :
+    get? (FiniteMap.zipWith f m1 m2) k =
+      match get? m1 k, get? m2 k with
+      | some v1, some v2 => some (f v1 v2)
+      | _, _ => none := by
+  simp only [FiniteMap.zipWith]
+  cases h1 : get? m1 k
+  · simp
+    cases h' : get? (ofList ((toList m1).filterMap (fun (ki, vi) =>
+        match get? m2 ki with
+        | some v' => some (ki, f vi v')
+        | none => none)) : M V'') k
+    · rfl
+    · rename_i v_result
+      have hnodup : ((toList m1).filterMap (fun (ki, vi) =>
+          match get? m2 ki with
+          | some v' => some (ki, f vi v')
+          | none => none)).map Prod.fst |>.Nodup := by
+        refine nodup_map_fst_filterMap (V' := V'') (toList m1) (fun ki vi =>
+            match get? m2 ki with
+            | some v' => some (ki, f vi v')
+            | none => none) (nodup_toList_keys m1) ?_
+        intros ki vi k' v' heq
+        cases heq' : get? m2 ki <;> simp [heq'] at heq
+        obtain ⟨rfl, _⟩ := heq
+        rfl
+      have hmem : (k, v_result) ∈ (toList m1).filterMap (fun (ki, vi) =>
+          match get? m2 ki with
+          | some v' => some (ki, f vi v')
+          | none => none) :=
+        (mem_ofList (M := M) (V := V'') _ k v_result hnodup).mpr h'
+      rw [List.mem_filterMap] at hmem
+      obtain ⟨⟨k', v1'⟩, hmem1, hmatch⟩ := hmem
+      simp at hmatch
+      cases hm2 : get? m2 k' <;> simp [hm2] at hmatch
+      · obtain ⟨heq_k, _⟩ := hmatch
+        have : get? m1 k' = some v1' := (mem_toList m1 k' v1').mp hmem1
+        rw [heq_k, h1] at this
+        cases this
+  · rename_i v1
+    cases h2 : get? m2 k
+    · simp
+      cases h' : get? (ofList ((toList m1).filterMap (fun (ki, vi) =>
+          match get? m2 ki with
+          | some v' => some (ki, f vi v')
+          | none => none)) : M V'') k
+      · rfl
+      · rename_i v_result
+        have hnodup : ((toList m1).filterMap (fun (ki, vi) =>
+            match get? m2 ki with
+            | some v' => some (ki, f vi v')
+            | none => none)).map Prod.fst |>.Nodup := by
+          refine nodup_map_fst_filterMap (V' := V'') (toList m1) (fun ki vi =>
+              match get? m2 ki with
+              | some v' => some (ki, f vi v')
+              | none => none) (nodup_toList_keys m1) ?_
+          intros ki vi k' v' heq
+          cases heq' : get? m2 ki <;> simp [heq'] at heq
+          obtain ⟨rfl, _⟩ := heq
+          rfl
+        have hmem : (k, v_result) ∈ (toList m1).filterMap (fun (ki, vi) =>
+            match get? m2 ki with
+            | some v' => some (ki, f vi v')
+            | none => none) :=
+          (mem_ofList (M := M) (V := V'') _ k v_result hnodup).mpr h'
+        rw [List.mem_filterMap] at hmem
+        obtain ⟨⟨k', v1'⟩, hmem1, hmatch⟩ := hmem
+        simp at hmatch
+        cases hm2 : get? m2 k' <;> simp [hm2] at hmatch
+        · obtain ⟨heq_k, _⟩ := hmatch
+          rw [heq_k, h2] at hm2
+          cases hm2
+    · rename_i v2
+      simp
+      have hmem1 : (k, v1) ∈ toList m1 := (mem_toList m1 k v1).mpr h1
+      have hmem_filter : (k, f v1 v2) ∈ (toList m1).filterMap (fun (ki, vi) =>
+          match get? m2 ki with
+          | some v' => some (ki, f vi v')
+          | none => none) := by
+        rw [List.mem_filterMap]
+        refine ⟨(k, v1), hmem1, ?_⟩
+        simp [h2]
+      have hnodup : ((toList m1).filterMap (fun (ki, vi) =>
+          match get? m2 ki with
+          | some v' => some (ki, f vi v')
+          | none => none)).map Prod.fst |>.Nodup := by
+        refine nodup_map_fst_filterMap (V' := V'') (toList m1) (fun ki vi =>
+            match get? m2 ki with
+            | some v' => some (ki, f vi v')
+            | none => none) (nodup_toList_keys m1) ?_
+        intros ki vi k' v' heq
+        cases heq' : get? m2 ki <;> simp [heq'] at heq
+        obtain ⟨rfl, _⟩ := heq
+        rfl
+      exact (mem_ofList (M := M) _ k (f v1 v2) hnodup).mp hmem_filter
+
+/-- Corresponds to Rocq's `map_fmap_zip_with_r`. -/
+theorem map_zipWith_right [DecidableEq V] {V' V'' : Type _} [DecidableEq V'] [DecidableEq V'']
+    (f : V → V' → V'') (g1 : V'' → V) (m1 : M V) (m2 : M V')
+    (hg1 : ∀ x y, g1 (f x y) = x)
+    (hdom : ∀ k, (get? m1 k).isSome ↔ (get? m2 k).isSome) :
+    FiniteMap.map g1 (FiniteMap.zipWith f m1 m2) = m1 := by
+  apply ext
+  intro k
+  rw [get?_map, get?_zipWith]
+  cases h1 : get? m1 k with
+  | none => simp
+  | some x =>
+    have h2 : (get? m2 k).isSome = true := (hdom k).mp (by simp [h1])
+    cases h2' : get? m2 k with
+    | none => simp [h2'] at h2
+    | some y =>
+      simp [hg1]
+
+/-- Corresponds to Rocq's `map_fmap_zip_with_l`. -/
+theorem map_zipWith_left [DecidableEq V] [DecidableEq V'] {V'' : Type _} [DecidableEq V'']
+    (f : V → V' → V'') (g2 : V'' → V') (m1 : M V) (m2 : M V')
+    (hg2 : ∀ x y, g2 (f x y) = y)
+    (hdom : ∀ k, (get? m1 k).isSome ↔ (get? m2 k).isSome) :
+    FiniteMap.map g2 (FiniteMap.zipWith f m1 m2) = m2 := by
+  apply ext
+  intro k
+  rw [get?_map, get?_zipWith]
+  cases h2 : get? m2 k with
+  | none => simp
+  | some y =>
+    have h1 : (get? m1 k).isSome = true := (hdom k).mpr (by simp [h2])
+    cases h1' : get? m1 k with
+    | none => simp [h1'] at h1
+    | some x =>
+      simp [hg2]
+
+/-- Insert distributes over zipWith. -/
+theorem zipWith_insert [DecidableEq V] [DecidableEq V'] [DecidableEq V'']
+    (f : V → V' → V'') (m1 : M V) (m2 : M V') (i : K) (x : V) (y : V') :
+    FiniteMap.zipWith f (insert m1 i x) (insert m2 i y) =
+    insert (FiniteMap.zipWith f m1 m2) i (f x y) := by
+  apply ext
+  intro k
+  by_cases h : k = i
+  · subst h
+    simp only [get?_insert_same, get?_zipWith]
+  · have h' : i ≠ k := Ne.symm h
+    simp only [get?_zipWith, get?_insert_ne _ i k _ h']
+
+/-- Corresponds to Rocq's `map_delete_zip_with`. -/
+theorem zipWith_delete [DecidableEq V] [DecidableEq V'] [DecidableEq V'']
+    (f : V → V' → V'') (m1 : M V) (m2 : M V') (i : K) :
+    FiniteMap.zipWith f (delete m1 i) (delete m2 i) =
+    delete (FiniteMap.zipWith f m1 m2) i := by
+  apply ext
+  intro k
+  by_cases h : k = i
+  · subst h
+    simp only [get?_delete_same, get?_zipWith]
+  · have h' : i ≠ k := Ne.symm h
+    simp only [get?_zipWith, get?_delete_ne _ i k h']
+
+theorem zipWith_comm [DecidableEq V] [DecidableEq V'] [DecidableEq V'']
+    (f : V → V' → V'') (m1 : M V) (m2 : M V') :
+    FiniteMap.zipWith (fun x y => f y x) m2 m1 = FiniteMap.zipWith f m1 m2 := by
+  apply ext
+  intro k
+  rw [get?_zipWith, get?_zipWith]
+  cases get? m1 k <;> cases get? m2 k <;> simp
+
+/-- Corresponds to Rocq's `map_zip_with_flip`. -/
+theorem zip_comm [DecidableEq V] [DecidableEq V']
+    (m1 : M V) (m2 : M V') :
+    FiniteMap.zip m2 m1 = FiniteMap.map Prod.swap (FiniteMap.zip m1 m2) := by
+  apply ext
+  intro k
+  unfold FiniteMap.zip
+  rw [get?_map, get?_zipWith, get?_zipWith]
+  cases get? m1 k <;> cases get? m2 k <;> simp [Prod.swap]
+
+/-- Mapping with id is identity.
+    Corresponds to Rocq's `map_id`. -/
+theorem map_id [DecidableEq V] (m : M V) :
+    FiniteMap.map id m = m := by
+  apply ext
+  intro k
+  rw [get?_map]
+  cases get? m k <;> simp
+
+/-- Mapping over a zip is the same as zipping the mapped maps.
+    Corresponds to Rocq's `map_fmap_zip`. -/
+theorem zip_map [DecidableEq V] [DecidableEq V'] {V'' V''' : Type _} [DecidableEq V''] [DecidableEq V''']
+    (f : V → V'') (g : V' → V''') (m1 : M V) (m2 : M V') :
+    FiniteMap.zip (FiniteMap.map f m1) (FiniteMap.map g m2) =
+    FiniteMap.map (fun (x, y) => (f x, g y)) (FiniteMap.zip m1 m2) := by
+  apply ext
+  intro k
+  unfold FiniteMap.zip
+  rw [get?_zipWith, get?_map, get?_map, get?_map, get?_zipWith]
+  cases h1 : get? m1 k <;> cases h2 : get? m2 k <;> simp
+
+/-- Zipping fst and snd projections of a map recovers the original map.
+    Corresponds to Rocq's `map_zip_fst_snd`. -/
+theorem zip_fst_snd {V' : Type u'} [DecidableEq V] [DecidableEq V'] (m : M (V × V')) :
+    FiniteMap.zip (FiniteMap.map Prod.fst m) (FiniteMap.map Prod.snd m) = m := by
+  apply ext
+  intro k
+  unfold FiniteMap.zip
+  rw [get?_zipWith, get?_map, get?_map]
+  cases h : get? m k with
+  | none => simp
+  | some p => cases p with | mk v1 v2 => simp
+
+/-- Corresponds to part of Rocq's dom lemmas for zip. -/
+theorem isSome_zipWith [DecidableEq V] [DecidableEq V'] [DecidableEq V'']
+    (f : V → V' → V'') (m1 : M V) (m2 : M V') (k : K) :
+    (get? (FiniteMap.zipWith f m1 m2) k).isSome ↔
+    (get? m1 k).isSome ∧ (get? m2 k).isSome := by
+  rw [get?_zipWith]
+  cases get? m1 k <;> cases get? m2 k <;> simp [Option.isSome_some, Option.isSome_none]
+
+/-- Zipping two empty maps yields an empty map.
+    Corresponds to Rocq's `map_zip_empty`. -/
+theorem zip_empty [DecidableEq V] [DecidableEq V'] :
+    FiniteMap.zip (∅ : M V) (∅ : M V') = ∅ := by
+  apply ext
+  intro k
+  unfold FiniteMap.zip
+  rw [get?_zipWith, get?_empty, get?_empty, get?_empty]
+
+/-- Lookup in a zipped map.
+    Corresponds to Rocq's `lookup_zip_with` specialized to `zip`. -/
+theorem get?_zip [DecidableEq V] [DecidableEq V'] (m1 : M V) (m2 : M V') (k : K) :
+    get? (FiniteMap.zip m1 m2) k =
+      match get? m1 k, get? m2 k with
+      | some v1, some v2 => some (v1, v2)
+      | _, _ => none := by
+  unfold FiniteMap.zip
+  rw [get?_zipWith]
+
+/-- Insert distributes over zip.
+    Corresponds to Rocq's `map_zip_insert`. -/
+theorem zip_insert [DecidableEq V] [DecidableEq V']
+    (m1 : M V) (m2 : M V') (i : K) (x : V) (y : V') :
+    get? m1 i = none → get? m2 i = none →
+    FiniteMap.zip (insert m1 i x) (insert m2 i y) =
+    insert (FiniteMap.zip m1 m2) i (x, y) := by
+  intro h1 h2
+  unfold FiniteMap.zip
+  exact zipWith_insert Prod.mk m1 m2 i x y
+
+/-- Delete distributes over zip.
+    Corresponds to Rocq's `map_zip_delete`. -/
+theorem zip_delete [DecidableEq V] [DecidableEq V']
+    (m1 : M V) (m2 : M V') (i : K) :
+    FiniteMap.zip (delete m1 i) (delete m2 i) =
+    delete (FiniteMap.zip m1 m2) i := by
+  unfold FiniteMap.zip
+  exact zipWith_delete Prod.mk m1 m2 i
+
+/-- Domain of a zipped map.
+    Corresponds to part of Rocq's `elem_of_dom_2` for zip. -/
+theorem isSome_zip [DecidableEq V] [DecidableEq V'] (m1 : M V) (m2 : M V') (k : K) :
+    (get? (FiniteMap.zip m1 m2) k).isSome ↔
+    (get? m1 k).isSome ∧ (get? m2 k).isSome := by
+  unfold FiniteMap.zip
+  exact isSome_zipWith Prod.mk m1 m2 k
+
+/-- toList of a zipped map.
+    Corresponds to Rocq's `map_to_list_zip`. -/
+theorem toList_zip [DecidableEq V] [DecidableEq V'] (m1 : M V) (m2 : M V') :
+    (toList (FiniteMap.zip m1 m2)).Perm
+      ((toList m1).filterMap (fun (k, v1) =>
+        match get? m2 k with
+        | some v2 => some (k, (v1, v2))
+        | none => none)) := by
+  unfold FiniteMap.zip
+  simp only [FiniteMap.zipWith]
+  apply toList_ofList
+  refine nodup_map_fst_filterMap (V' := V × V') (toList m1)
+    (fun ki vi => match get? m2 ki with | some v' => some (ki, (vi, v')) | none => none)
+    (nodup_toList_keys m1) ?_
+  intro ki vi k' vp heq
+  cases heq' : get? m2 ki <;> simp [heq'] at heq
+  obtain ⟨rfl, _⟩ := heq
+  rfl
+
+/-- Corresponds to Rocq's `lookup_union_None`. -/
+theorem get?_union_none (m1 m2 : M V) (i : K) :
+    get? (m1 ∪ m2) i = none ↔ get? m1 i = none ∧ get? m2 i = none := by
+  rw [get?_union]
+  cases h1 : get? m1 i <;> cases h2 : get? m2 i <;> simp [Option.orElse]
+
+/-- Corresponds to Rocq's `insert_union_l`. -/
+theorem union_insert_left (m1 m2 : M V) (i : K) (x : V) :
+    get? (insert (m1 ∪ m2) i x) = get? (insert m1 i x ∪ m2) := by
+  funext k
+  by_cases hik : i = k
+  · subst hik
+    simp [get?_insert_same, get?_union]
+  · simp [get?_insert_ne _ _ _ _ hik, get?_union]
+
+end FiniteMapLaws
+
+namespace FiniteMap
+
+variable {K : Type v} {M : Type u → _}  [FiniteMap K M]
+
+/-- Submap is reflexive. -/
+theorem subset_refl (m : M V) : m ⊆ m := fun _ _ h => h
+
+/-- Submap is transitive. -/
+theorem subset_trans {m₁ m₂ m₃ : M V} (h₁ : m₁ ⊆ m₂) (h₂ : m₂ ⊆ m₃) : m₁ ⊆ m₃ :=
+  fun k v hm₁ => h₂ k v (h₁ k v hm₁)
+
+/-- Disjointness is symmetric. -/
+theorem disjoint_comm {m₁ m₂ : M V} (h : disjoint m₁ m₂) : disjoint m₂ m₁ :=
+  fun k ⟨h₂, h₁⟩ => h k ⟨h₁, h₂⟩
+
+theorem disjoint_empty_right [DecidableEq K] [FiniteMapLaws K M] (m : M V) : m ##ₘ (∅ : M V) :=
+  disjoint_comm (FiniteMapLaws.disjoint_empty_left (K:= K) m)
+
+/-- `m₂` and `m₁ \ m₂` are disjoint. -/
+theorem disjoint_difference_right [DecidableEq K] [FiniteMapLaws K M] [FiniteMapLawsSelf K M]
+    (m₁ m₂ : M V) : m₂ ##ₘ (m₁ \ m₂) := by
+  intro k ⟨h_in_m2, h_in_diff⟩
+  rw [FiniteMapLaws.get?_difference] at h_in_diff
+  simp only [h_in_m2, ↓reduceIte, Option.isSome_none, Bool.false_eq_true] at h_in_diff
+
+/-- Corresponds to Rocq's `map_difference_union`. -/
+theorem union_difference_cancel [DecidableEq K] [FiniteMapLaws K M] [FiniteMapLawsSelf K M]
+    (m₁ m₂ : M V) (hsub : m₂ ⊆ m₁) : m₂ ∪ (m₁ \ m₂) = m₁ := by
+  apply FiniteMapLaws.ext (M := M) (K := K) (V := V)
+  intro k
+  rw [FiniteMapLaws.get?_union, FiniteMapLaws.get?_difference]
+  cases hm2 : get? m₂ k with
+  | none =>
+    simp only [Option.isSome_none, Bool.false_eq_true, ↓reduceIte, Option.orElse_none]
+  | some v =>
+    simp only [Option.isSome_some, ↓reduceIte, Option.orElse_some]
+    exact (hsub k v hm2).symm
+
+end FiniteMap
+
+end Iris.Std
diff --git a/src/Iris/Std/List.lean b/src/Iris/Std/List.lean
new file mode 100644
index 00000000..35500711
--- /dev/null
+++ b/src/Iris/Std/List.lean
@@ -0,0 +1,101 @@
+/-
+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.
+    Corresponds to Rocq's `list_equiv`. -/
+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))
+
+/-- For a Nodup list, erasing an element removes it completely. -/
+theorem not_mem_erase_self_of_nodup {α : Type _} [DecidableEq α] (x : α) (l : List α)
+    (hnd : l.Nodup) : x ∉ l.erase x := by
+  induction l with
+  | nil => exact List.not_mem_nil
+  | cons y ys ih =>
+    simp only [List.erase_cons]
+    rw [List.nodup_cons] at hnd
+    split
+    · next h =>
+      have heq : y = x := eq_of_beq h
+      rw [← heq]
+      exact hnd.1
+    · next h =>
+      simp only [List.mem_cons]
+      intro hor
+      cases hor with
+      | inl heq =>
+        have : (y == x) = true := beq_iff_eq.mpr heq.symm
+        exact absurd this h
+      | inr hmem => exact ih hnd.2 hmem
+
+/-- Two Nodup lists with the same membership are permutations of each other.
+    Corresponds to Rocq's `NoDup_Permutation`. -/
+theorem perm_of_nodup_of_mem_iff {α : Type _} [DecidableEq α]
+    {l₁ l₂ : List α} (hnd₁ : l₁.Nodup) (hnd₂ : l₂.Nodup)
+    (hmem : ∀ x, x ∈ l₁ ↔ x ∈ l₂) : l₁.Perm l₂ := by
+  induction l₁ generalizing l₂ with
+  | nil =>
+    cases l₂ with
+    | nil => exact List.Perm.refl []
+    | cons y ys =>
+      have : y ∈ ([] : List α) := (hmem y).mpr List.mem_cons_self
+      exact absurd this List.not_mem_nil
+  | cons x xs ih =>
+    have hx_in_l₂ : x ∈ l₂ := (hmem x).mp List.mem_cons_self
+    have hperm₂ : l₂.Perm (x :: l₂.erase x) := List.perm_cons_erase hx_in_l₂
+    rw [List.nodup_cons] at hnd₁
+    have hx_notin_xs : x ∉ xs := hnd₁.1
+    have hnd_xs : xs.Nodup := hnd₁.2
+    have hnd_erase : (l₂.erase x).Nodup := hnd₂.erase x
+    have hmem_erase : ∀ y, y ∈ xs ↔ y ∈ l₂.erase x := by
+      intro y
+      constructor
+      · intro hy
+        have hne : y ≠ x := fun heq => hx_notin_xs (heq ▸ hy)
+        have hy_l₂ : y ∈ l₂ := (hmem y).mp (List.mem_cons_of_mem x hy)
+        exact (List.mem_erase_of_ne hne).mpr hy_l₂
+      · intro hy
+        have hne : y ≠ x := by
+          intro heq
+          rw [heq] at hy
+          exact not_mem_erase_self_of_nodup x l₂ hnd₂ hy
+        have hy_l₂ : y ∈ l₂ := List.mem_of_mem_erase hy
+        have hy_l₁ : y ∈ x :: xs := (hmem y).mpr hy_l₂
+        cases List.mem_cons.mp hy_l₁ with
+        | inl heq => exact absurd heq hne
+        | inr h => exact h
+    have hperm_xs : xs.Perm (l₂.erase x) := ih hnd_xs hnd_erase hmem_erase
+    exact (List.Perm.cons x hperm_xs).trans hperm₂.symm
+
+
+theorem nodup_of_nodup_map_fst {α β : Type _} (l : List (α × β))
+    (h : (l.map Prod.fst).Nodup) : l.Nodup := by
+  induction l with
+  | nil => exact List.nodup_nil
+  | cons x xs ih =>
+    rw [List.nodup_cons]
+    constructor
+    · intro hx
+      rw [List.map_cons, List.nodup_cons] at h
+      have : x.1 ∈ xs.map Prod.fst := List.mem_map_of_mem (f := Prod.fst) hx
+      exact h.1 this
+    · rw [List.map_cons, List.nodup_cons] at h
+      exact ih h.2
+
+end Iris.Std.List