diff --git a/src/Iris/Std/FiniteMap.lean b/src/Iris/Std/FiniteMap.lean
new file mode 100644
index 00000000..ea7f9b61
--- /dev/null
+++ b/src/Iris/Std/FiniteMap.lean
@@ -0,0 +1,1240 @@
+/-
+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. -/
+  get? : M V → K → Option V
+  /-- Insert or update a key-value pair. -/
+  insert : M V → K → V → M V
+  /-- Remove a key from the map. -/
+  delete : M V → K → M V
+  /-- Convert the map to a list of key-value pairs. -/
+  toList : M V → List (K × V)
+  /-- Construct a map from a list of key-value pairs. -/
+  ofList : List (K × V) → M V
+  /-- Fold over all key-value pairs in the map.
+      The order of folding depends on the internal representation. -/
+  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]
+
+def empty : M V := ofList []
+
+/-- Empty map instance for `∅` notation. -/
+instance : EmptyCollection (M V) := ⟨empty⟩
+
+/-- Singleton map containing exactly one key-value pair. -/
+def singleton (k : K) (v : V) : M V := insert ∅ k v
+
+/-- Union of two maps (left-biased: values from `m₁` take precedence). -/
+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. -/
+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₂`. -/
+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. -/
+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. -/
+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. -/
+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. -/
+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. -/
+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₁`. -/
+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. -/
+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`. -/
+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. -/
+def firstKey (m : M V) (i : K) : Prop :=
+  ∃ x, (toList m).head? = some (i, x)
+
+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
+  ext : ∀ (m₁ m₂ : M V), (∀ i, get? m₁ i = get? m₂ i) → m₁ = m₂
+  get?_empty : ∀ k, get? (∅ : M V) k = none
+  get?_insert_same : ∀ (m : M V) k v, get? (insert m k v) k = some v
+  get?_insert_ne : ∀ (m : M V) k k' v, k ≠ k' → get? (insert m k v) k' = get? m k'
+  get?_delete_same : ∀ (m : M V) k, get? (delete m k) k = none
+  get?_delete_ne : ∀ (m : M V) k k', k ≠ k' → get? (delete m k) k' = get? m k'
+  ofList_nil : (ofList [] : M V) = ∅
+  ofList_cons : ∀ (k : K) (v : V) (l : List (K × V)),
+    (ofList ((k, v) :: l) : M V) = insert (ofList l) k v
+  toList_spec (m : M V) :
+    (toList m).Nodup ∧ (∀ i x, (i, x) ∈ toList m ↔ get? m i = some x)
+
+/-- 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. -/
+  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. -/
+  toList_map_seq : ∀ (start : Nat) (l : List V),
+    (toList (FiniteMap.map_seq start l : M V)).Perm
+      ((List.range' start l.length).zip l)
+
+export FiniteMapLaws (ext
+get?_empty
+get?_insert_same get?_insert_ne
+get?_delete_same get?_delete_ne
+ofList_nil ofList_cons
+toList_spec)
+
+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
+    · suffices kv = (k, v) by rw [← this]; exact List.Mem.head _
+      ext <;> simp [heq]
+      exact Option.some.inj (by rw [heq, get?_insert_same] at h; exact h)
+    · exact List.Mem.tail _ (ih (by rw [get?_insert_ne _ _ _ _ heq] at h; exact h))
+
+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
+
+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
+
+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]
+
+theorem nodup_toList (m : M V): (toList m).Nodup :=
+  (toList_spec m).1
+
+
+private theorem mem_of_get?_ofList' (l : List (K × V)) (k : K) (v : V) (hnodup: (l.map Prod.fst).Nodup):
+   (k, v) ∈ l → get? (ofList l : M V) k = some v := by
+  intro h
+  induction l with
+  | nil => simp [] at h
+  | cons kv kvs ih =>
+    rw [ofList_cons, get?_insert]
+    simp only [List.mem_cons, List.map_cons, List.nodup_cons] at h hnodup
+    split
+    · next heq =>
+      rcases h with ⟨rfl, rfl⟩ | hmem
+      · rfl
+      · exfalso
+        have : k ∈ kvs.map Prod.fst := by
+          rw [List.mem_map]
+          exact ⟨(k, v), hmem, rfl⟩
+        rw [← heq] at this
+        exact hnodup.1 this
+    · next hne =>
+      rcases h with ⟨rfl, rfl⟩ | hmem
+      · contradiction
+      · exact ih hnodup.2 hmem
+
+/-- 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 =>
+    simp only [List.map_cons, List.nodup_cons] at hnodup ⊢
+    refine ⟨?_, ih hnodup.2 fun a b ha hb => hinj a b (.tail _ ha) (.tail _ hb)⟩
+    intro h; rw [List.mem_map] at h
+    obtain ⟨y, hy_mem, heq⟩ := h
+    exact hnodup.1 (hinj x y (.head _) (.tail _ hy_mem) heq.symm ▸ hy_mem)
+
+/-- 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
+  ext <;> simp [heq]
+  have hv1 := (hmem k₁ v₁).mp h1
+  have hv2 := (hmem k₂ v₂).mp h2
+  rw [heq] at hv1
+  rw [hv1] at hv2
+  cases hv2;rfl
+
+theorem mem_toList (m : M V) : ∀ k v, (k, v) ∈ toList m ↔ get? m k = some v :=
+  (toList_spec m).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 => simp [ofList_nil, get?_empty]
+  | cons kv l ih =>
+    obtain ⟨k, v⟩ := kv
+    simp [ofList_cons, get?_insert]
+    intro h; split at h
+    · next heq => cases h; simp [← heq]
+    · next _ => exact .inr (ih h)
+
+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
+    simp [ofList_cons, List.map_cons, List.nodup_cons] at hnodup hmem ⊢
+    rcases hmem with ⟨rfl, rfl⟩ | hmem
+    · rw [get?_insert_same]
+    · rw [get?_insert_ne, ih hnodup.2 hmem]
+      intro heq; subst heq
+      exact hnodup.1 _ hmem
+
+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
+
+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
+  apply List.perm_of_nodup_of_mem_iff
+  · exact List.nodup_of_nodup_map_fst l1 hnodup1
+  · exact List.nodup_of_nodup_map_fst l2 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]
+
+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
+      cases 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]
+
+ 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. -/
+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. -/
+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. -/
+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. -/
+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. -/
+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]
+
+theorem empty_subset (m : M V) : (∅ : M V) ⊆ m := by
+  intro k v h
+  simp [get?_empty] at h
+
+theorem disjoint_empty_left (m : M V) : (∅ : M V) ##ₘ m := by
+  intro k ⟨h₁, _⟩
+  simp [get?_empty] at h₁
+
+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
+
+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
+
+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
+
+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]
+
+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]
+
+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
+
+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
+
+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
+
+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]
+
+theorem toList_empty : toList (∅ : M V) = [] := by
+  apply List.eq_nil_iff_forall_not_mem.mpr
+  intro ⟨i, x⟩ hmem
+  rw [mem_toList, get?_empty] at hmem
+  cases hmem
+
+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
+  refine ofList_injective (M := M) (K := K) _ _ (nodup_toList_keys _) ?_ ?_
+  · simp only [List.map_cons, List.nodup_cons, nodup_toList_keys m]
+    simp [mem_toList, hk_none]
+  · rw [ofList_toList, ofList_cons, ofList_toList]
+
+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
+
+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]
+
+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]
+
+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, *]
+
+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]
+
+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]
+
+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]
+
+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]
+
+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]
+
+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]
+
+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
+theorem insert_empty (i : K) (x : V) :
+    insert (∅ : M V) i x = {[i := x]} := rfl
+
+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
+
+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
+
+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
+
+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]
+
+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
+  · apply 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, hi] at h2
+    cases h2
+
+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
+
+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
+    simp [get?_insert_same, hk]
+  · simp [get?_insert_ne _ _ _ _ hik] at hk
+    simp [get?_insert_ne _ _ _ _ hik]
+    exact hsub k v hk
+
+theorem singleton_ne_empty (i : K) (x : V) :
+    {[i := x]} ≠ (∅ : M V) := insert_ne_empty ∅ i x
+
+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]
+
+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 hjk
+  subst hik hjk
+  trivial
+
+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
+    apply hfa kv.1 kv.2 ((mem_toList m kv.1 kv.2).mp hmem)
+  · intro hlist k v hget
+    apply hlist (k, v) ((mem_toList m k v).mpr hget)
+
+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
+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
+  apply himpl
+  apply hp k v hget
+
+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
+  apply hfa
+  apply get?_insert_same m i x
+
+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
+  · apply hfa k v
+    simp [get?_insert_ne _ _ _ _ hik, hget]
+
+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]
+    assumption
+  · apply hfa
+    simp [get?_insert_ne _ _ _ _ hik] at hget
+    assumption
+
+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
+
+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
+    apply hfa i x (get?_singleton_same i x)
+  · intro hpix k v hget
+    simp [get?_singleton] at hget
+    obtain ⟨rfl, rfl⟩ := hget
+    exact hpix
+
+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
+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; right; assumption
+    · simp only [Option.not_isSome_iff_eq_none] at h1; left; assumption
+  · intro h k ⟨hs1, hs2⟩
+    cases h k with
+    | inl h1 => simp [h1] at hs1
+    | inr h2 => simp [h2] at hs2
+
+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⟩
+
+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⟩
+
+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⟩
+
+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⟩
+
+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
+
+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
+
+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
+  apply nodup_toList_keys
+
+/-- 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]
+  have hnodup : ((toList m).map (fun (ki, vi) => (ki, f vi))).map Prod.fst |>.Nodup := by
+    simp only [List.map_map]; exact nodup_toList_keys m
+  cases hm : get? m k <;> simp
+  · apply Option.eq_none_iff_forall_not_mem.mpr
+    intro v' hv'
+    have := (mem_ofList _ _ _ hnodup).mpr hv'
+    rw [List.mem_map] at this
+    obtain ⟨⟨k', v⟩, hmem, heq⟩ := this
+    simp at heq
+    have : get? m k' = some v := (mem_toList m k' v).mp hmem
+    rw [heq.1, hm] at this
+    cases this
+  · rename_i v
+    rw [(mem_ofList _ _ _ hnodup).mp]
+    rw [List.mem_map]
+    exact ⟨(k, v), (mem_toList m k v).mpr hm, rfl⟩
+
+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
+  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 : k' = k := h_preserve_key k v k' v' hg
+      subst this
+      rw [List.map_cons, List.nodup_cons]
+      refine ⟨fun hmem => h_nodup.1 ?_, ih h_nodup.2⟩
+      clear h_nodup ih
+      induction tail with
+      | nil => cases hmem
+      | cons kv' tail' ih_aux =>
+        obtain ⟨k'', v''⟩ := kv'
+        simp only [List.filterMap] at hmem
+        cases hg' : g k'' v'' with
+        | none => simp only [hg'] at hmem; exact List.mem_cons_of_mem k'' (ih_aux hmem)
+        | some res' =>
+          obtain ⟨k''', v'''⟩ := res'
+          have hk_eq : k''' = k'' := h_preserve_key k'' v'' k''' v''' hg'
+          simp only [hg', List.map_cons, List.mem_cons] at hmem
+          rcases hmem with rfl | hmem'
+          · rw [List.map_cons, List.mem_cons, hk_eq]; simp
+          · rw [List.map_cons, List.mem_cons]; right; exact ih_aux hmem'
+
+/-- 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]
+  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
+    exact heq.1.symm
+  cases h1 : get? m1 k
+  · simp; cases h' : get? (ofList _ : M V'') k
+    · rfl
+    · rename_i v_result
+      have hmem := (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
+      have : get? m1 k' = some v1' := (mem_toList m1 k' v1').mp hmem1
+      rw [hmatch.1, h1] at this
+      cases this
+  · rename_i v1
+    cases h2 : get? m2 k
+    · simp; cases h' : get? (ofList _ : M V'') k
+      · rfl
+      · rename_i v_result
+        have hmem := (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
+        rw [hmatch.1, h2] at hm2
+        cases hm2
+    · rename_i v2
+      simp
+      apply (mem_ofList _ k (f v1 v2) hnodup).mp
+      rw [List.mem_filterMap]
+      exact ⟨(k, v1), (mem_toList m1 k v1).mpr h1, by simp [h2]⟩
+
+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 =>
+    cases h2' : get? m2 k with
+    | none =>
+      have : (get? m2 k).isSome = true := (hdom k).mp (by simp [h1])
+      simp [h2'] at this
+    | some y => simp [hg1]
+
+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 =>
+    cases h1' : get? m1 k with
+    | none =>
+      have : (get? m1 k).isSome = true := (hdom k).mpr (by simp [h2])
+      simp [h1'] at this
+    | 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 _ _ _ _ h']
+
+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
+
+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. -/
+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. -/
+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. -/
+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; simp
+
+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. -/
+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. -/
+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. -/
+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. -/
+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. -/
+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. -/
+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
+
+theorem 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 := by
+  rw [(ofList_toList m).symm]
+  have hnodup : (toList m).map Prod.fst |>.Nodup := nodup_toList_keys m
+  generalize hgen : toList m = l
+  rw [hgen] at hnodup
+  clear hgen m
+  induction l with
+  | nil => rw [ofList_nil]; exact hemp
+  | cons kv l ih =>
+    obtain ⟨k, v⟩ := kv
+    simp only [List.map_cons, List.nodup_cons] at hnodup
+    rw [ofList_cons]
+    apply hins
+    · cases hget : get? (ofList l : M V) k
+      · rfl
+      · rename_i v'
+        exfalso
+        apply hnodup.1
+        rw [List.mem_map]
+        exact ⟨(k, v'), (mem_of_mem_ofList l k v' hget), rfl⟩
+    · exact ih hnodup.2
+
+theorem get?_union : ∀ (m₁ m₂ : M V) k,
+    get? (m₁ ∪ m₂) k = (get? m₁ k).orElse (fun _ => get? m₂ k) := by
+  intro m₁ m₂ k
+  simp only [Union.union, FiniteMap.union]
+  have h : ∀ (l : List (K × V)) (hnodup : (l.map Prod.fst).Nodup) (m : M V),
+        get? (l.foldl (fun acc x => insert acc x.fst x.snd) m) k =
+        (l.lookup k).orElse (fun _ => get? m k) := by
+    intro l hnodup m
+    induction l generalizing m with
+    | nil => simp
+    | cons p tail ih =>
+      obtain ⟨k', v'⟩ := p
+      rw [List.map_cons, List.nodup_cons] at hnodup
+      simp only [List.foldl, List.lookup]
+      rw [ih hnodup.2, get?_insert]
+      by_cases heq : k = k'
+      · subst heq
+        have : List.lookup k tail = none := by
+          cases h : List.lookup k tail
+          · rfl
+          · rename_i v
+            simp at hnodup
+            have hmem : (k, v) ∈ tail := List.list_lookup_some_mem k v tail h
+            exact absurd hmem (hnodup.1 v)
+        simp [this]
+      · have : (k == k') = false := by simp [heq]
+        simp [this, Ne.symm heq]
+  show get? ((toList m₁).foldl (fun acc x => insert acc x.fst x.snd) m₂) k = _
+  rw [h (toList m₁) (nodup_toList_keys m₁) m₂]
+  congr 1
+  cases hlookup : (toList m₁).lookup k
+  · cases hget : get? m₁ k
+    · rfl
+    · rename_i v
+      have : (toList m₁).lookup k = some v :=
+        List.list_mem_lookup_some k v _ (nodup_toList_keys m₁) (((toList_spec m₁).2 k v).mpr hget)
+      cases this ▸ hlookup
+  · rename_i v
+    exact (((toList_spec m₁).2 k v).mp (List.list_lookup_some_mem k v _ hlookup)).symm
+
+theorem get?_difference : ∀ (m₁ m₂ : M V) k,
+    get? (m₁ \ m₂) k = if (get? m₂ k).isSome then none else get? m₁ k := by
+  intro m₁ m₂ k
+  simp only [SDiff.sdiff, FiniteMap.difference]
+  split
+  · rename_i h
+    obtain ⟨v₂, hv₂⟩ := Option.isSome_iff_exists.mp h
+    have : k ∉ (List.filter (fun x => (get? m₂ x.fst).isNone) (toList m₁)).map Prod.fst := by
+      intro hmem
+      obtain ⟨⟨k', v'⟩, hmem_filter, rfl⟩ := List.mem_map.mp hmem
+      simp [List.mem_filter, hv₂] at hmem_filter
+    cases hget : get? (ofList (List.filter (fun x => (get? m₂ x.fst).isNone) (toList m₁)) : M V) k
+    · rfl
+    · exact absurd (List.mem_map_of_mem (mem_of_mem_ofList _ k _ hget)) this
+  · rename_i h
+    have hm₂ : get? m₂ k = none := by
+      cases h' : get? m₂ k <;> simp_all [Option.isSome_some]
+    cases hm₁ : get? m₁ k
+    · cases hget : get? (ofList (List.filter (fun x => (get? m₂ x.fst).isNone) (toList m₁)) : M V) k
+      · rfl
+      · have := (mem_toList m₁ k _).mp (List.mem_filter.mp (mem_of_mem_ofList _ k _ hget)).1
+        rw [hm₁] at this; cases this
+    · rename_i v₁
+      apply mem_ofList_of_mem _ k v₁
+      · apply List.Nodup.map_of_injective ((nodup_toList m₁).filter _)
+        intro ⟨k₁, v₁⟩ ⟨k₂, v₂⟩ h₁ h₂ heq; simp at heq
+        have hv₁ := (mem_toList m₁ k₁ v₁).mp (List.mem_filter.mp h₁).1
+        have hv₂ := (mem_toList m₁ k₂ v₂).mp (List.mem_filter.mp h₂).1
+        ext <;> simp [heq]
+        rw [← heq] at hv₂; rw [hv₁] at hv₂; cases hv₂; rfl
+      · exact List.mem_filter.mpr ⟨(mem_toList m₁ k v₁).mpr hm₁, by simp [hm₂]⟩
+
+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]
+
+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
+
+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/FiniteMapInstances.lean b/src/Iris/Std/FiniteMapInstances.lean
new file mode 100644
index 00000000..d4a1582a
--- /dev/null
+++ b/src/Iris/Std/FiniteMapInstances.lean
@@ -0,0 +1,165 @@
+/-
+Copyright (c) 2025 Zongyuan Liu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zongyuan Liu
+-/
+import Iris.Std.FiniteMap
+import Iris.Std.List
+import Std
+
+/-! ## FiniteMap Instance for Std.ExtTreeMap
+
+This file instantiates the abstract finite map interface `Iris.Std.FiniteMap` with Lean's `Std.ExtTreeMap`.
+-/
+namespace Iris.Std
+
+/-- Instance of FiniteMap for Std.ExtTreeMap. -/
+instance {K : Type u} [Ord K] [Std.TransCmp (α := K) compare] [Std.LawfulEqCmp (α := K) compare] [DecidableEq K]:
+    FiniteMap K (Std.ExtTreeMap K) where
+  get? m k := m.get? k
+  insert m k v := m.insert k v
+  delete m k := m.erase k
+  toList m := m.toList
+  ofList l := Std.ExtTreeMap.ofList l.reverse
+  fold := fun f init m => m.foldr f init
+
+namespace FiniteMapInst
+
+variable {K : Type _} [Ord K] [Std.TransCmp (α := K) compare] [Std.LawfulEqCmp (α := K) compare] [DecidableEq K]
+
+/-- The FiniteMapLaws instance for ExtTreeMap. -/
+instance : FiniteMapLaws K (Std.ExtTreeMap K) where
+  ext := by
+    intro m₁ m₂ h
+    apply Std.ExtTreeMap.ext_getElem?
+
+  get?_empty := by
+    intro k
+    simp [FiniteMap.get?]
+
+  get?_insert_same := by
+    intro m k v
+    simp [FiniteMap.get?, FiniteMap.insert]
+
+  get?_insert_ne := by
+    intro m _ k k' h
+    simp [FiniteMap.get?, FiniteMap.insert, Std.ExtTreeMap.getElem?_insert]
+    intro h h'
+    trivial
+
+  get?_delete_same := by
+    intro m k
+    simp [FiniteMap.get?, FiniteMap.delete]
+
+  get?_delete_ne := by
+    intro m k k' h h'
+    simp [FiniteMap.get?, FiniteMap.delete, Std.ExtTreeMap.getElem?_erase]
+    intro h h'
+    trivial
+
+  ofList_nil := by
+    simp [FiniteMap.ofList]
+
+  ofList_cons := by
+    intro k v l l_1
+    simp only [FiniteMap.ofList, FiniteMap.insert]
+    rw [List.reverse_cons, Std.ExtTreeMap.ofList_eq_insertMany_empty, Std.ExtTreeMap.ofList_eq_insertMany_empty, Std.ExtTreeMap.insertMany_append, Std.ExtTreeMap.insertMany_list_singleton]
+
+  toList_spec := by
+    intro V m
+    constructor
+    · simp only [FiniteMap.toList]
+      have hdistinct : m.toList.Pairwise (fun a b => ¬compare a.1 b.1 = .eq) :=
+        Std.ExtTreeMap.distinct_keys_toList
+      apply hdistinct.imp
+      intro a b hne heq
+      subst heq
+      have : compare a.1 a.1 = .eq := Std.LawfulEqCmp.compare_eq_iff_eq.mpr rfl
+      exact hne this
+    · intro i x
+      simp only [FiniteMap.toList, FiniteMap.get?]
+      exact Std.ExtTreeMap.mem_toList_iff_getElem?_eq_some
+
+
+/-- The FiniteMapLawsSelf instance for ExtTreeMap. -/
+instance : FiniteMapLawsSelf K (Std.ExtTreeMap K) where
+  toList_filterMap := by
+    intro V m f
+    haveI : DecidableEq V := Classical.typeDecidableEq V
+    simp only [FiniteMap.toList, FiniteMap.filterMap, FiniteMap.ofList]
+
+    obtain H := FiniteMapLaws.toList_ofList (M := (Std.ExtTreeMap K)) (K := K) (V := V) (l := (List.filterMap (fun kv => Option.map (fun x => (kv.fst, x)) (f kv.snd)) m.toList))
+
+    simp only [FiniteMap.toList, FiniteMap.ofList] at H
+    apply H
+    rw [List.map_filterMap]
+    have eq_goal : (List.filterMap (fun x => Option.map Prod.fst (Option.map (fun x_1 => (x.fst, x_1)) (f x.snd))) m.toList) =
+                   (List.filterMap (fun x => Option.map (fun _ => x.fst) (f x.snd)) m.toList) := by
+      congr 1
+      ext x
+      rw [Option.map_map]
+      rfl
+    rw [eq_goal]
+    have nodup_keys : (m.toList.map Prod.fst).Nodup := by
+      rw [Std.ExtTreeMap.map_fst_toList_eq_keys]
+      exact Std.ExtTreeMap.nodup_keys
+    exact List.nodup_filterMap_of_nodup_keys m.toList f nodup_keys
+
+  toList_filter := by
+    intro V m φ
+    simp [FiniteMap.toList, FiniteMap.filter, FiniteMap.ofList]
+    haveI : DecidableEq V := Classical.typeDecidableEq V
+    obtain H := FiniteMapLaws.toList_ofList (M := (Std.ExtTreeMap K)) (K := K) (V := V) (l := (List.filter (fun x => φ x.fst x.snd) m.toList))
+
+    simp only [FiniteMap.toList, FiniteMap.ofList] at H
+    apply H
+
+    have nodup_keys : (m.toList.map Prod.fst).Nodup := by
+      rw [Std.ExtTreeMap.map_fst_toList_eq_keys]
+      exact Std.ExtTreeMap.nodup_keys
+
+    exact List.nodup_map_fst_filter m.toList (fun x => φ x.fst x.snd) nodup_keys
+
+/-- The FiniteMapKmapLaws instance for ExtTreeMap with key type transformation. -/
+instance {K' : Type _} [Ord K'] [Std.TransCmp (α := K') compare] [Std.LawfulEqCmp (α := K') compare] [DecidableEq K'] :
+    FiniteMapKmapLaws K K' (Std.ExtTreeMap K) (Std.ExtTreeMap K') where
+  toList_kmap := by
+    intro V f m hinj
+    simp [FiniteMap.toList, FiniteMap.kmap, FiniteMap.ofList]
+    haveI : DecidableEq V := Classical.typeDecidableEq V
+    obtain H := FiniteMapLaws.toList_ofList (M := (Std.ExtTreeMap K')) (K := K') (V := V) (l := (List.map (fun x => (f x.fst, x.snd)) m.toList))
+
+    simp only [FiniteMap.toList, FiniteMap.ofList] at H
+    apply H
+
+    have nodup_keys : (m.toList.map Prod.fst).Nodup := by
+      rw [Std.ExtTreeMap.map_fst_toList_eq_keys]
+      exact Std.ExtTreeMap.nodup_keys
+
+    exact List.nodup_map_fst_map_injective m.toList f hinj nodup_keys
+
+/-- The FiniteMapSeqLaws instance for ExtTreeMap with Nat keys. -/
+instance [Std.TransCmp (α := Nat) compare] [Std.LawfulEqCmp (α := Nat) compare] :
+    FiniteMapSeqLaws (Std.ExtTreeMap Nat) where
+  toList_map_seq := by
+    intro V start l
+    simp [FiniteMap.toList, FiniteMap.map_seq, FiniteMap.ofList]
+    haveI : DecidableEq V := Classical.typeDecidableEq V
+
+    have heq : List.mapIdx (fun i v => (start + i, v)) l = (List.range' start l.length).zip l :=
+      List.mapIdx_add_eq_zip_range' start l
+
+    rw [heq]
+
+    obtain H := FiniteMapLaws.toList_ofList (M := (Std.ExtTreeMap Nat)) (K := Nat) (V := V) (l := ((List.range' start l.length).zip l))
+
+    simp only [FiniteMap.toList, FiniteMap.ofList] at H
+    apply H
+
+    -- The keys from range' are all distinct
+    rw [← heq]
+    exact List.nodup_map_fst_mapIdx_add start l
+
+end FiniteMapInst
+
+end Iris.Std
diff --git a/src/Iris/Std/List.lean b/src/Iris/Std/List.lean
new file mode 100644
index 00000000..3f79ee93
--- /dev/null
+++ b/src/Iris/Std/List.lean
@@ -0,0 +1,212 @@
+/-
+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
+
+/-- Bidirectional relationship between lookup and membership for lists with no duplicate keys.
+    For a list with no duplicate keys, `List.lookup k l = some v` if and only if `(k, v) ∈ l`. -/
+theorem list_lookup_some_iff_mem {A B : Type _} [DecidableEq A]
+    (k : A) (v : B) (l : List (A × B))
+    (hnodup : (l.map Prod.fst).Nodup) :
+    List.lookup k l = some v ↔ (k, v) ∈ l := by
+  induction l with
+  | nil => simp [List.lookup]
+  | cons hd tl ih =>
+    simp only [List.lookup, List.mem_cons]
+    rw [List.map_cons, List.nodup_cons] at hnodup
+    split
+    · next heq =>
+      constructor
+      · intro h; left; cases Option.some.inj h; ext
+        · apply eq_of_beq heq
+        · rfl
+      · intro h; cases h with
+        | inl h => cases h; rfl
+        | inr h => have : k ∈ tl.map Prod.fst := by simp; exact ⟨v, h⟩
+                   exact absurd (by rw [← eq_of_beq heq]; exact this) hnodup.1
+    · next hneq =>
+      rw [ih hnodup.2]; constructor
+      · intro h; exact Or.inr h
+      · intro h; cases h with
+        | inl h => cases h; simp at hneq
+        | inr h => exact h
+
+/-- If lookup returns some value, the key-value pair is in the list. -/
+theorem list_lookup_some_mem {A B : Type _} [DecidableEq A]
+    (k : A) (v : B) (l : List (A × B)) :
+    List.lookup k l = some v → (k, v) ∈ l := by
+  intro h
+  induction l with
+  | nil => contradiction
+  | cons hd tl ih =>
+    simp only [List.lookup, List.mem_cons] at h ⊢
+    split at h
+    · next heq => left; cases Option.some.inj h; ext; apply eq_of_beq heq; rfl
+    · exact Or.inr (ih h)
+
+/-- If a key-value pair is in the list with no duplicate keys, lookup returns that value. -/
+theorem list_mem_lookup_some {A B : Type _} [DecidableEq A]
+    (k : A) (v : B) (l : List (A × B))
+    (hnodup : (l.map Prod.fst).Nodup) :
+    (k, v) ∈ l → List.lookup k l = some v := by
+  exact (list_lookup_some_iff_mem k v l hnodup).mpr
+
+/-- 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 => rw [← eq_of_beq h]; exact hnd.1
+    · next h => simp; exact ⟨fun heq => absurd (beq_iff_eq.mpr heq.symm) h, ih hnd.2⟩
+
+/-- 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 => exact absurd ((hmem y).mpr List.mem_cons_self) List.not_mem_nil
+  | cons x xs ih =>
+    rw [List.nodup_cons] at hnd₁
+    have hmem_erase : ∀ y, y ∈ xs ↔ y ∈ l₂.erase x := fun y => ⟨
+      fun hy => (List.mem_erase_of_ne (fun (heq : y = x) => hnd₁.1 (heq ▸ hy))).mpr ((hmem y).mp (List.mem_cons_of_mem x hy)),
+      fun hy => by
+        have hy_l₁ : y ∈ x :: xs := (hmem y).mpr (List.mem_of_mem_erase hy)
+        cases List.mem_cons.mp hy_l₁ with
+        | inl heq => exact absurd (heq ▸ hy) (not_mem_erase_self_of_nodup x l₂ hnd₂)
+        | inr h => exact h⟩
+    exact (List.Perm.cons x (ih hnd₁.2 (hnd₂.erase x) hmem_erase)).trans
+          (List.perm_cons_erase ((hmem x).mp List.mem_cons_self)).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
+
+/-- If a list has no duplicate keys (Nodup on first components),
+    then filtering preserves this property on the first components. -/
+theorem nodup_map_fst_filter {α β : Type _}
+    (l : List (α × β)) (p : α × β → Bool)
+    (h : (l.map Prod.fst).Nodup) :
+    ((List.filter p l).map Prod.fst).Nodup := by
+  induction l with
+  | nil => simp
+  | cons kv tail ih =>
+    rw [List.map_cons, List.nodup_cons] at h
+    simp only [List.filter]; split
+    · rw [List.map_cons, List.nodup_cons]
+      refine ⟨fun hmem => h.1 ?_, ih h.2⟩
+      clear h ih; induction tail with
+      | nil => simp at hmem
+      | cons kv' tail' ih_tail =>
+        simp only [List.filter] at hmem
+        split at hmem
+        · rw [List.map_cons, List.mem_cons] at hmem
+          rcases hmem with heq | hmem'
+          · rw [List.map_cons, List.mem_cons]; exact Or.inl heq
+          · rw [List.map_cons, List.mem_cons]; exact Or.inr (ih_tail hmem')
+        · rw [List.map_cons, List.mem_cons]; exact Or.inr (ih_tail hmem)
+    · exact ih h.2
+
+/-- If a list has no duplicate keys (Nodup on first components) and we map keys
+    with an injective function, the result also has no duplicate keys. -/
+theorem nodup_map_fst_map_injective {α β γ : Type _}
+    (l : List (α × β)) (f : α → γ)
+    (hinj : ∀ {x y : α}, f x = f y → x = y)
+    (h : (l.map Prod.fst).Nodup) :
+    ((List.map (fun x => (f x.fst, x.snd)) l).map Prod.fst).Nodup := by
+  rw [List.map_map]
+  induction l with
+  | nil => constructor
+  | cons kv tail ih =>
+    rw [List.map_cons, List.nodup_cons] at h ⊢
+    refine ⟨fun hmem => h.1 ?_, ih h.2⟩
+    clear h ih; induction tail with
+    | nil => simp at hmem
+    | cons kv' tail' ih_tail =>
+      rw [List.map_cons, List.mem_cons] at hmem
+      rcases hmem with heq | hmem'
+      · simp [hinj heq]
+      · simp [ih_tail hmem']
+
+/-- mapIdx with addition creates the same result as zipping with range'. -/
+theorem mapIdx_add_eq_zip_range' {α : Type _} (start : Nat) (l : List α) :
+    List.mapIdx (fun i v => (start + i, v)) l = (List.range' start l.length).zip l := by
+  induction l generalizing start with
+  | nil =>
+    rw [List.mapIdx_nil, List.length_nil, List.range'_zero, List.zip_nil_left]
+  | cons hd tl ih =>
+    rw [List.mapIdx_cons, List.length_cons, List.range'_succ, List.zip_cons_cons]
+    congr 1
+    have heq : (fun (i : Nat) (v : α) => (start + (i + 1), v)) = (fun (i : Nat) (v : α) => (start + 1 + i, v)) := by
+      funext i v
+      simp only [Nat.add_assoc, Nat.add_comm 1]
+    rw [heq]
+    exact ih (start + 1)
+
+/-- The keys from mapIdx with addition are all distinct. -/
+theorem nodup_map_fst_mapIdx_add {α : Type _} (start : Nat) (l : List α) :
+    (List.mapIdx (fun i v => (start + i, v)) l).map Prod.fst |>.Nodup := by
+  rw [mapIdx_add_eq_zip_range', List.map_fst_zip]
+  · exact List.nodup_range' (step := 1)
+  · rw [List.length_range']
+    omega
+
+/-- If a list has no duplicate keys (Nodup on first components),
+    then filtering by mapping the second components preserves this property. -/
+theorem nodup_filterMap_of_nodup_keys {α β : Type _}
+    (l : List (α × β)) (f : β → Option β)
+    (h : (l.map Prod.fst).Nodup) :
+    (List.filterMap (fun x => Option.map (fun _ => x.fst) (f x.snd)) l).Nodup := by
+  induction l with
+  | nil => simp
+  | cons kv tail ih =>
+    rw [List.map_cons, List.nodup_cons] at h
+    simp only [List.filterMap]; split
+    · exact ih h.2
+    · next b heq =>
+      have hb : b = kv.fst := by
+        obtain ⟨_, _, hf⟩ := Option.map_eq_some_iff.1 heq; exact hf.symm
+      subst hb; constructor
+      · intro a' hmem heq; subst heq; apply h.1; clear h ih heq
+        induction tail with
+        | nil => simp at hmem
+        | cons kv' tail' ih_tail =>
+          simp only [List.filterMap] at hmem; split at hmem
+          · simp [ih_tail hmem]
+          · next b' heq' =>
+            have hb' : b' = kv'.fst := by
+              obtain ⟨_, _, hf⟩ := Option.map_eq_some_iff.1 heq'; exact hf.symm
+            subst hb'; simp only [List.mem_cons] at hmem
+            rcases hmem with heq | hmem'
+            · simp [heq]
+            · simp [ih_tail hmem']
+      · exact ih h.2
+
+end Iris.Std.List