diff --git a/lake-manifest.json b/lake-manifest.json
index eba3e5fe..6ef99b0f 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,11 +1,21 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/quote4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "509ad12ac4efd70d96418b481521296f9619bcf0",
+   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.27.0",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "bf4cd323a0d088f361a94fcadb8db5cf1e9f3768",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "stable",
diff --git a/lakefile.toml b/lakefile.toml
index f1c790ac..4313f823 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -7,6 +7,11 @@ name = "Qq"
 scope = "leanprover-community"
 version = "git#stable"
 
+[[require]]
+name = "batteries"
+scope = "leanprover-community"
+rev = "v4.27.0"
+
 [[lean_lib]]
 name = "Iris"
 
diff --git a/src/Iris/Std/FromMathlib.lean b/src/Iris/Std/FromMathlib.lean
new file mode 100644
index 00000000..acda1317
--- /dev/null
+++ b/src/Iris/Std/FromMathlib.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Zongyuan Liu, Markus de Medeiros. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+
+namespace FromMathlib
+
+/-- NB. Copied from Mathlib -/
+theorem List.Nodup.of_map (f : α → β) {l : List α} : List.Nodup (List.map f l) → List.Nodup l := by
+  refine (List.Pairwise.of_map f) fun _ _ => mt <| fun a => (congrArg f ∘ fun _ => a) α
+
+/-- NB. Copied from Mathlib -/
+theorem Pairwise.forall {l : List α} {R : α → α → Prop} (hR : ∀ {a b}, R a b ↔ a ≠ b)
+    (hl : l.Pairwise (· ≠ ·)) : ∀ ⦃a⦄, a ∈ l → ∀ ⦃b⦄, b ∈ l → a ≠ b → R a b := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [List.mem_cons]
+    rintro x (rfl | hx) y (rfl | hy)
+    · simp
+    · exact fun a => hR.mpr a
+    · exact fun a => hR.mpr a
+    · refine ih (List.Pairwise.of_cons hl) hx hy
+
+/-- NB. Copied from Mathlib -/
+theorem inj_on_of_nodup_map {f : α → β} {l : List α} (d : List.Nodup (List.map f l)) :
+    ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → f x = f y → x = y := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.map, List.nodup_cons, List.mem_map, not_exists, not_and, ← Ne.eq_def] at d
+    simp only [List.mem_cons]
+    rintro _ (rfl | h₁) _ (rfl | h₂) h₃
+    · rfl
+    · apply (d.1 _ h₂ h₃.symm).elim
+    · apply (d.1 _ h₁ h₃).elim
+    · apply ih d.2 h₁ h₂ h₃
+
+/-- NB. Copied from Mathlib -/
+theorem Nodup.map_on {f : α → β} (H : ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y) (d : List.Nodup l) :
+    (List.map f l).Nodup :=
+  List.Pairwise.map _ (fun a b ⟨ma, mb, n⟩ e => n (H a ma b mb e)) (List.Pairwise.and_mem.1 d)
+
+/-- NB. Copied from Mathlib -/
+ theorem Nodup.filterMap {f : α → Option β} (h : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') :
+    List.Nodup l → List.Nodup (List.filterMap f l) :=
+  (List.Pairwise.filterMap f) @fun a a' n b bm b' bm' e => n <| h a a' b' (by rw [← e]; exact bm) bm'
+
+/-- NB. Copied from Mathlib -/
+theorem Nodup.filter (p : α → Bool) {l} : List.Nodup l → List.Nodup (List.filter p l) := by
+  simpa using List.Pairwise.filter p
+
+end FromMathlib
diff --git a/src/Iris/Std/HeapInstances.lean b/src/Iris/Std/HeapInstances.lean
index e7d6660a..72ca1d26 100644
--- a/src/Iris/Std/HeapInstances.lean
+++ b/src/Iris/Std/HeapInstances.lean
@@ -392,6 +392,32 @@ instance : LawfulPartialMap (TreeMap K · compare) K where
   get?_bindAlter := by simp [Iris.Std.get?, Iris.Std.bindAlter]
   get?_merge := getElem?_mergeWith'
 
+instance : FiniteMap (TreeMap K · compare) K where
+  toList t := t.toList
+
+instance : LawfulFiniteMap (TreeMap K · compare) K where
+  toList_empty := rfl
+  toList_noDupKeys := by
+    intro V m
+    have h' : Pairwise (fun a b => ¬compare a b = eq) (m.toList.map (·.1)) := by
+      refine pairwise_map.mpr ?_
+      refine (distinct_keys_toList (t := m)).imp ?_
+      intro _ _ hab
+      exact hab
+    refine h'.imp ?_
+    intro a b hab
+    rw [compare_eq_iff_eq] at hab
+    exact hab
+  toList_get := by
+    intro V m k v
+    constructor
+    · intro h
+      exact getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList.mpr ⟨k, compare_self, h⟩
+    · intro h
+      obtain ⟨_, hcmp, hmem⟩ := getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList.mp h
+      rw [compare_eq_iff_eq.mp hcmp]
+      exact hmem
+
 end HeapInstance
 
 end Std.TreeMap
diff --git a/src/Iris/Std/PartialMap.lean b/src/Iris/Std/PartialMap.lean
index ea687dc9..bb52582b 100644
--- a/src/Iris/Std/PartialMap.lean
+++ b/src/Iris/Std/PartialMap.lean
@@ -1,3 +1,6 @@
+import Batteries.Data.List.Perm
+import Iris.Std.FromMathlib
+
 /-
 Copyright (c) 2026 Zongyuan Liu, Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -17,12 +20,13 @@ This class does not re-use the GetElem? class from the standard library, because
 of the validity predicate `valid`.
 
 Additionally, this class is only defined for containers which can hold elements of
-any given type (ie. containers of the type `Type _ → Type _`). The reason for this is
-that the resource algebra construction only applies to these types anyways.
+any given type (ie. containers of the type `Type _ → Type _`). The reason for this
+is that the resource algebra construction only applies to these types anyways.
 
 The PartialMap interface does not require that the representation of a partial map
 be unique, ie. all constructions reason extensionally about the get? function rather
-than intensionally about map equalities. PartialMaps are free to be non-uniquely represented.
+than intensionally about map equalities. PartialMaps are free to be non-uniquely
+represented.
 -/
 namespace Iris.Std
 
@@ -36,16 +40,23 @@ class PartialMap (M : Type _ → Type _) (K : outParam (Type _)) where
   merge (op : K → V → V → V) : M V → M V → M V
 export PartialMap (get? insert delete empty bindAlter merge)
 
-/-- RepFunMap: The map T is capable of representing all partial functions out of K. -/
+/-- A FiniteMap is a PartialMap with a toList operation. Like in Stdpp, the order in
+which the elements are passed into the list is unspecified. -/
+class FiniteMap M K extends PartialMap M K where
+  toList : M V → List (K × V)
+export FiniteMap (toList)
+
+/-- RepFunMap: The map T is capable of representing all partial functions out of
+K. -/
 class RepFunMap (T : Type _ → Type _) (K : outParam (Type _)) [PartialMap T K] where
   of_fun : (K → Option V) → T V
   get_of_fun (f : K → Option V) (k : K) : get? (of_fun f) k = f k
 export RepFunMap (of_fun get_of_fun)
 
-/-- IsoFunStore: The map T is isomorphic to the type of functions out of `K`. In other words,
-    equality of T is the same as equality of functions, so the CMRA on these partial functions
-    is leibniz. -/
-class IsoFunMap (T : Type _  → Type _) (K : outParam (Type _)) [PartialMap T K]
+/-- IsoFunStore: The map T is isomorphic to the type of functions out of `K`. In
+other words, equality of T is the same as equality of functions, so the CMRA on
+these partial functions is leibniz. -/
+class IsoFunMap (T : Type _ → Type _) (K : outParam (Type _)) [PartialMap T K]
   extends RepFunMap T K where
   of_fun_get {t : T V} : of_fun (get? t) = t
 export IsoFunMap (of_fun_get)
@@ -71,11 +82,11 @@ class UnboundedHeap (M : Type _ → Type _) (K : outParam (Type _)) extends Heap
   notFull_insert_fresh {m : M V} {H : notFull m} : notFull (insert m (fresh H) v)
 export UnboundedHeap (notFull_empty notFull_insert_fresh)
 
-
 namespace PartialMap
 
 variable {K V M} [PartialMap M K]
 
+/-- The empty partial map can be written as `∅`. -/
 instance : EmptyCollection (M V) := ⟨PartialMap.empty⟩
 
 /-- Singleton map containing exactly one key-value pair. -/
@@ -87,11 +98,17 @@ def disjoint (m₁ m₂ : M V) : Prop := ∀ k, ¬((get? m₁ k).isSome ∧ (get
 /-- 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
 
+/-- Construct a map from a list of key-value pairs. Later entries override earlier ones. -/
+def ofList (l : List (K × V)) : M V :=
+  l.foldr (fun (k, v) acc => insert acc k v) empty
+
+/-- Partial maps support the subset relation `⊆` via the submap relation. -/
 instance : HasSubset (M V) := ⟨submap⟩
 
 /-- Membership: a key is in the map if it has a value. -/
 def mem (m : M V) (k : K) : Prop := (get? m k).isSome
 
+/-- Keys can be tested for membership in partial maps using `∈`. -/
 instance : Membership K (M V) := ⟨fun m k => (get? m k).isSome⟩
 
 /-- Universal quantification over map entries. -/
@@ -104,17 +121,44 @@ def dom (m : M V) : K → Prop := fun k => (get? m k).isSome
 -- Should this be part of the typeclass, or should we use this derived one?
 @[simp] def union : M V → M V → M V := merge (fun _ v _ => v)
 
-/-- Two PartalMaps are pointwise equivalent. -/
+/-- Partial maps support the union operation `∪`, with left-biased merge. -/
+instance : Union (M V) := ⟨union⟩
+
+/-- Map a function over all values in the map. -/
+def map (f : V → V') : M V → M V' :=
+  bindAlter (fun _ v => some (f v))
+
+/-- Filter and map: apply a function that can optionally drop entries. -/
+def filterMap (f : V → Option V) : M V → M V :=
+  bindAlter (fun _ v => f v)
+
+/-- Filter entries by a predicate on key-value pairs. -/
+def filter (φ : K → V → Bool) : M V → M V :=
+  bindAlter (fun k v => if φ k v then some v else none)
+
+/-- Difference: remove all keys in `m₂` from `m₁`. -/
+def difference (m₁ m₂ : M V) : M V :=
+  bindAlter (fun k v => if (get? m₂ k).isSome then none else some v) m₁
+
+def zipWith (f : V → V' → V'') (m₁ : M V) (m₂ : M V') : M V'' :=
+  bindAlter (fun k v => (get? m₂ k).bind fun v' => some <| f v v') m₁
+
+def zip (m₁ : M V) (m₂ : M V') : M (V × V') :=
+  zipWith (fun x y => (x, y)) m₁ m₂
+
+/-- Partial maps support the set difference operation `\` via difference. -/
+instance : SDiff (M V) := ⟨difference⟩
+
+/-- Two PartialMaps are pointwise equivalent. -/
 @[simp] def equiv (m1 m2 : M V) : Prop := ∀ k, get? m1 k = get? m2 k
 
+/-- Pointwise equivalence is transitive. -/
 instance instEquivTrans : Trans equiv (@equiv K V M _) equiv := ⟨by simp_all⟩
 
 scoped syntax term " ≡ₘ " term : term
 scoped macro_rules
   | `($m₁ ≡ₘ $m₂) => `(PartialMap.equiv $m₁ $m₂)
 
-end PartialMap
-
 /-- Iris notation for singleton map: `{[k := v]}` -/
 scoped syntax "{[" term " := " term "]}" : term
 scoped macro_rules
@@ -123,22 +167,6 @@ scoped macro_rules
 /-- Iris notation for map disjointness: `m₁ ##ₘ m₂` -/
 scoped infix:50 " ##ₘ " => PartialMap.disjoint
 
-/-- Laws that a partial map implementation must satisfy. -/
-class LawfulPartialMap (M : Type _ → Type _) (K : outParam (Type _)) extends PartialMap M K where
-  get?_empty k : get? (empty : M V) k = none
-  get?_insert_eq {m : M V} {k k' v} : k = k' → 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_eq {m : M V} {k k'} : k = 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'
-  get?_bindAlter {m : M V} {f : K → V → Option V'} : get? (bindAlter f m) k = (get? m k).bind (f k)
-  get?_merge : get? (merge op m₁ m₂) k = Option.merge (op k) (get? m₁ k) (get? m₂ k)
-export LawfulPartialMap (get?_empty get?_insert_eq get?_insert_ne get?_delete_eq get?_delete_ne
-  get?_bindAlter get?_merge)
-
-namespace PartialMap
-
-variable {K : Type _} {M : Type _ → Type _} [PartialMap M K]
-
 /-- Submap is reflexive. -/
 theorem subset_refl (m : M V) : m ⊆ m := fun _ _ h => h
 
@@ -150,9 +178,10 @@ theorem subset_trans {m₁ m₂ m₃ : M V} (h₁ : m₁ ⊆ m₂) (h₂ : m₂
 theorem disjoint_comm {m₁ m₂ : M V} (h : disjoint m₁ m₂) : disjoint m₂ m₁ :=
   fun k ⟨h₂, h₁⟩ => h k ⟨h₁, h₂⟩
 
-theorem all_mono (P Q : K → V → Prop) {m : M V} :
-    PartialMap.all P m → (∀ k v, P k v → Q k v) → PartialMap.all Q m :=
-  fun hp himpl k v hget => himpl k v (hp k v hget)
+theorem all_mono (P Q : K → V → Prop) {m : M V}
+    (hp : PartialMap.all P m) (himpl : ∀ k v, P k v → Q k v) :
+    PartialMap.all Q m :=
+  fun k v hget => himpl k v (hp k v hget)
 
 theorem disjoint_iff (m₁ m₂ : M V) :
     m₁ ##ₘ m₂ ↔ ∀ k, get? m₁ k = none ∨ get? m₂ k = none := by
@@ -170,15 +199,56 @@ theorem disjoint_iff (m₁ m₂ : M V) :
 
 end PartialMap
 
-class ExtensionalPartialMap (M : Type _ → Type _) (K : outParam (Type _)) extends PartialMap M K where
+/-- An association list has no duplicate keys -/
+def NoDupKeys (L : List (K × A)) : Prop := L.map (·.1) |>.Nodup
+
+class ExtensionalPartialMap (M : Type _ → Type _) (K : outParam (Type _))
+    extends PartialMap M K where
   equiv_iff_eq {m₁ m₂ : M V} : PartialMap.equiv m₁ m₂ ↔ m₁ = m₂
 
+/-- Laws that a partial map implementation must satisfy. -/
+class LawfulPartialMap (M : Type _ → Type _) (K : outParam (Type _))
+    extends PartialMap M K where
+  get?_empty k : get? (empty : M V) k = none
+  get?_insert_eq {m : M V} {k k' v} : k = k' → 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_eq {m : M V} {k k'} : k = 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'
+  get?_bindAlter {m : M V} {f : K → V → Option V'} :
+      get? (bindAlter f m) k = (get? m k).bind (f k)
+  get?_merge :
+      get? (merge op m₁ m₂) k = Option.merge (op k) (get? m₁ k) (get? m₂ k)
+export LawfulPartialMap (get?_empty get?_insert_eq get?_insert_ne get?_delete_eq
+  get?_delete_ne get?_bindAlter get?_merge)
+
+class LawfulFiniteMap M K extends LawfulPartialMap M K, FiniteMap M K where
+  toList_empty : toList (∅ : M V) = []
+  toList_noDupKeys : NoDupKeys (toList (m : M V))
+  toList_get : (k, v) ∈ toList m ↔ get? m k = some v
+export LawfulFiniteMap (toList_empty toList_noDupKeys toList_get)
+
+namespace FiniteMap
+
+variable {K V : Type _} {M : Type _ → Type _} [FiniteMap M K]
+
+-- /-- Convert the map to a list of key-value pairs. The order is unspecified. -/
+-- def toList (m : M V) : List (K × V) :=
+--   mapFold (fun k v acc => (k, v) :: acc) [] m
+
+def mapFold {A : Type _} (f : K → V → A → A) (a : A) (m : M V) : A :=
+  List.foldl (fun a' ⟨k, v⟩ => f k v a') a (toList (K := K) m)
+
+/-- Convert a list to a map with sequential natural number keys starting from `start`. -/
+def map_seq [FiniteMap M Nat] (start : Nat) (l : List V) : M V :=
+  PartialMap.ofList (l.mapIdx (fun i v => (start + i, v)))
+
+end FiniteMap
+
 namespace LawfulPartialMap
 
 open PartialMap
 
-variable {K V : Type _} {M : Type _ → Type _}
-variable [LawfulPartialMap M K]
+variable {K V : Type _} {M : Type _ → Type _} [LawfulPartialMap M K]
 
 theorem get?_insert [DecidableEq K] {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
@@ -227,23 +297,19 @@ theorem disjoint_empty_right (m : M V) : m ##ₘ (∅ : M V) := by
   intro k ⟨_, h₂⟩
   simp [show get? (∅ : M V) k = none from get?_empty k] at h₂
 
-open Classical in
-theorem get?_insert_some_iff {m : M V} {i j : K} {x y : V} :
+theorem get?_insert_some_iff [DecidableEq K] {m : M V} {i j : K} {x y : V} :
     get? (insert m i x) j = some y ↔ (i = j ∧ x = y) ∨ (i ≠ j ∧ get? m j = some y) := by
   rw [get?_insert]; split <;> simp_all
 
-open Classical in
-theorem get?_insert_none_iff {m : M V} {i j : K} {x : V} :
+theorem get?_insert_none_iff [DecidableEq K] {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
 
-open Classical in
-theorem get?_delete_some_iff {m : M V} {i j : K} {y : V} :
+theorem get?_delete_some_iff [DecidableEq K] {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
 
-open Classical in
-theorem get?_delete_none_iff {m : M V} {i j : K} :
+theorem get?_delete_none_iff [DecidableEq K] {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
 
@@ -392,22 +458,23 @@ theorem all_empty (P : K → V → Prop) : PartialMap.all P (empty : M V) := by
   rw [get?_empty k] at h
   cases h
 
-theorem all_insert_of_all (P : K → V → Prop) {m : M V} {i : K} {x : V} :
-    PartialMap.all P (insert m i x) → P i x :=
-  fun h => h _ _ (get?_insert_eq rfl)
+theorem all_insert_of_all (P : K → V → Prop) {m : M V} {i : K} {x : V}
+    (h : PartialMap.all P (insert m i x)) : P i x :=
+  h _ _ (get?_insert_eq rfl)
 
-theorem all_of_all_insert (P : K → V → Prop) {m : M V} {i : K} {x : V} :
-    get? m i = none → PartialMap.all P (insert m i x) → PartialMap.all P m := by
-  intro hi h k v hget
+theorem all_of_all_insert (P : K → V → Prop) {m : M V} {i : K} {x : V}
+    (hi : get? m i = none) (h : PartialMap.all P (insert m i x)) :
+    PartialMap.all P m := by
+  intro k v hget
   by_cases hik : i = k
   · subst hik
     simp [hi] at hget
   · apply h k v
     simp [get?_insert_ne hik, hget]
 
-theorem all_insert (P : K → V → Prop) {m : M V} {i : K} {x : V} :
-    P i x → PartialMap.all P m → PartialMap.all P (insert m i x) := by
-  intro hpix h k v hget
+theorem all_insert (P : K → V → Prop) {m : M V} {i : K} {x : V}
+    (hpix : P i x) (h : PartialMap.all P m) : PartialMap.all P (insert m i x) := by
+  intro k v hget
   by_cases hik : i = k
   · subst hik
     simp [get?_insert_eq] at hget
@@ -432,69 +499,549 @@ theorem all_singleton (P : K → V → Prop) {i : K} {x : V} :
       exact hget ▸ h ▸ hpix
     · simp [get?_singleton_ne h] at hget
 
-theorem all_delete (P : K → V → Prop) {m : M V} {i : K} :
-    PartialMap.all P m → PartialMap.all P (delete m i) := by
-  intro h k v hget
+theorem all_delete (P : K → V → Prop) {m : M V} {i : K}
+    (h : PartialMap.all P m) : PartialMap.all P (delete m i) := by
+  intro k v hget
   by_cases hik : i = k
   · simp [get?_delete_eq hik] at hget
   · rw [get?_delete_ne hik] at hget
     exact h k v hget
 
-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⟩
+theorem disjoint_insert_left {m₁ m₂ : M V} {i : K} {x : V}
+    (hi : get? m₂ i = none) (hdisj : m₁ ##ₘ m₂) : insert m₁ i x ##ₘ m₂ := by
+  intro 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⟩
+theorem disjoint_insert_right {m₁ m₂ : M V} {i : K} {x : V}
+    (hi : get? m₁ i = none) (hdisj : m₁ ##ₘ m₂) : m₁ ##ₘ insert m₂ i x := by
+  intro 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⟩
+theorem disjoint_delete_left {m₁ m₂ : M V} {i : K}
+    (hdisj : m₁ ##ₘ m₂) : delete m₁ i ##ₘ m₂ := by
+  intro k ⟨hs1, hs2⟩
   by_cases hik : i = k
   · subst hik
     simp [get?_delete_eq] 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⟩
+theorem disjoint_delete_right {m₁ m₂ : M V} {i : K}
+    (hdisj : m₁ ##ₘ m₂) : m₁ ##ₘ delete m₂ i := by
+  intro k ⟨hs1, hs2⟩
   by_cases hik : i = k
   · subst hik
     simp [get?_delete_eq] 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⟩
+theorem disjoint_singleton_left {m : M V} {i : K} {x : V}
+    (hi : get? m i = none) : {[i := x]} ##ₘ m := by
+  intro k ⟨hs1, hs2⟩
   by_cases hik : i = k
   · subst hik
     simp [hi] at hs2
   · simp [PartialMap.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⟩
+theorem disjoint_singleton_right {m : M V} {i : K} {x : V}
+    (hi : get? m i = none) : m ##ₘ {[i := x]} := by
+  intro k ⟨hs1, hs2⟩
   by_cases hik : i = k
   · subst hik
     simp [hi] at hs1
   · simp [PartialMap.singleton, get?_insert_ne hik, get?_empty] at hs2
 
+theorem get?_insert_isSome [DecidableEq K] {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?_delete_isSome [DecidableEq K] {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?_difference {m₁ m₂ : M V} {k : K} :
+    get? (m₁ \ m₂) k = if (get? m₂ k).isSome then none else get? m₁ k := by
+  simp only [SDiff.sdiff, PartialMap.difference, get?_bindAlter]
+  cases hm2 : get? m₂ k <;> cases hm1 : get? m₁ k <;> simp
+
+theorem disjoint_difference_right {m₁ m₂ : M V} :
+    m₂ ##ₘ (m₁ \ m₂) := by
+  intro k ⟨h_in_m2, h_in_diff⟩
+  rw [get?_difference] at h_in_diff
+  simp only [h_in_m2, ↓reduceIte] at h_in_diff
+  cases h_in_diff
+
+theorem union_difference_cancel {m₁ m₂ : M V} (h : m₂ ⊆ m₁) :
+    union m₂ (m₁ \ m₂) ≡ₘ m₁ := by
+  intro k
+  simp only [PartialMap.union, get?_merge, get?_difference]
+  cases hm2 : get? m₂ k with
+  | none =>
+    cases get? m₁ k <;> simp [Option.merge]
+  | some v =>
+    simp [Option.merge]
+    exact (h k v hm2).symm
+
+theorem get?_union {m₁ m₂ : M V} {k : K} :
+    get? (union m₁ m₂) k = (get? m₁ k).orElse (fun _ => get? m₂ k) := by
+  simp only [PartialMap.union, get?_merge]
+  cases get? m₁ k <;> cases get? m₂ k <;> simp [Option.merge, Option.orElse]
+
+theorem get?_union_none {m₁ m₂ : M V} {i : K} :
+    get? (union m₁ m₂) i = none ↔ get? m₁ i = none ∧ get? m₂ i = none := by
+  rw [get?_union]
+  cases h1 : get? m₁ i <;> cases h2 : get? m₂ i <;> simp [Option.orElse]
+
+theorem union_insert_left {m₁ m₂ : M V} {i : K} {x : V} :
+    insert (union m₁ m₂) i x ≡ₘ union (insert m₁ i x) m₂ := by
+  intro k
+  by_cases hik : i = k
+  · subst hik
+    cases h : get? m₂ i <;> simp [get?_insert_eq rfl, PartialMap.union, get?_merge, Option.merge, h]
+  · simp [get?_insert_ne hik, PartialMap.union, get?_merge]
+
+theorem get?_map {f : V → V'} {m : M V} {k : K} :
+    get? (PartialMap.map f m) k = (get? m k).map f := by
+  simp only [PartialMap.map, get?_bindAlter]
+  cases get? m k <;> simp
+
+theorem map_id {m : M V} :
+    PartialMap.map id m ≡ₘ m := by
+  intro k
+  rw [get?_map]
+  cases get? m k <;> simp
+
+theorem get?_filterMap {f : V → Option V} {m : M V} {k : K} :
+    get? (filterMap f m) k = (get? m k).bind f := by
+  simp [filterMap, get?_bindAlter]
+
+theorem get?_filter {φ : K → V → Bool} {m : M V} {k : K} :
+    get? (filter φ m) k = (get? m k).bind (fun v => if φ k v then some v else none) := by
+  simp [Option.bind, filter, get?_bindAlter]
+
+theorem get?_zipWith {f : V → V' → V''} {m₁ : M V} {m₂ : M V'} {k : K} :
+    get? (zipWith f m₁ m₂) k = (get? m₁ k).bind fun v₁ => (get? m₂ k).map fun v₂ => f v₁ v₂ := by
+  simp [zipWith, get?_bindAlter]
+  cases h1 : get? m₁ k <;> cases h2 : get? m₂ k <;> simp [Option.bind]
+
+theorem get?_zip {m₁ : M V} {m₂ : M V'} {k : K} :
+    get? (zip m₁ m₂) k = (get? m₁ k).bind fun v₁ => (get? m₂ k).map fun v₂ => (v₁, v₂) := by
+  simp [zip, zipWith, get?_bindAlter]
+  cases h1 : get? m₁ k <;> cases h2 : get? m₂ k <;> simp [Option.bind]
+
+theorem map_zipWith_right {f : V → V' → V''} {g : V''' → V'} {m₁ : M V} {m₂ : M V'''} :
+    PartialMap.map (fun (v, w) => f v (g w)) (zip m₁ m₂) ≡ₘ
+      zipWith f m₁ (PartialMap.map g m₂) := by
+  intro k
+  simp [get?_map, get?_zip, get?_zipWith]
+  cases get? m₁ k <;> cases get? m₂ k <;> simp [Option.bind, Option.map]
+
+theorem map_zipWith_left {f : V → V' → V''} {g : V''' → V} {m₁ : M V'''} {m₂ : M V'} :
+    PartialMap.map (fun (w, v) => f (g w) v) (zip m₁ m₂) ≡ₘ
+      zipWith f (PartialMap.map g m₁) m₂ := by
+  intro k
+  simp [get?_map, get?_zip, get?_zipWith]
+  cases get? m₁ k <;> cases get? m₂ k <;> simp [Option.bind, Option.map]
+
+theorem zipWith_insert {f : V → V' → V''} {m₁ : M V} {m₂ : M V'} {k : K} {v : V} {v' : V'} :
+    zipWith f (insert m₁ k v) (insert m₂ k v') ≡ₘ
+      insert (zipWith f m₁ m₂) k (f v v') := by
+  intro k'
+  by_cases h : k = k'
+  · subst h
+    simp [get?_zipWith, get?_insert_eq rfl]
+  · simp [get?_zipWith, get?_insert_ne h]
+
+theorem zipWith_delete {f : V → V' → V''} {m₁ : M V} {m₂ : M V'} {k : K} :
+    zipWith f (delete m₁ k) (delete m₂ k) ≡ₘ delete (zipWith f m₁ m₂) k := by
+  intro k'
+  by_cases h : k = k'
+  · subst h
+    simp [get?_zipWith, get?_delete_eq rfl]
+  · simp [get?_zipWith, get?_delete_ne h]
+
+theorem zipWith_comm {f : V → V' → V''} {m₁ : M V} {m₂ : M V'} :
+    (∀ v v', f v v' = f v v') →
+    zipWith f m₁ m₂ ≡ₘ zipWith f m₁ m₂ := by
+  intro _; intro _; rfl
+
+-- -- FIXME: universe issue
+-- theorem zip_comm {m₁ : M V} {m₂ : M V'} :
+--     PartialMap.map Prod.swap (zip m₁ m₂) ≡ₘ zip m₂ m₁ := by
+--   sorry
+
+theorem zip_map {f : V → V'} {g : V → V''} {m : M V} :
+    zip (PartialMap.map f m) (PartialMap.map g m) ≡ₘ
+      PartialMap.map (fun v => (f v, g v)) m := by
+  intro k
+  simp [zip, get?_map, zipWith, get?_bindAlter]
+  cases get? m k <;> simp [Option.bind, Option.map]
+
+theorem zip_fst_snd {m : M (V × V')} :
+    zip (PartialMap.map Prod.fst m) (PartialMap.map Prod.snd m) ≡ₘ m := by
+  intro k
+  simp [zip, zipWith, get?_map, get?_bindAlter]
+  cases h : get? m k <;> simp [Option.bind, Option.map]
+
+theorem isSome_zipWith {f : V → V' → V''} {m₁ : M V} {m₂ : M V'} {k : K} :
+    (get? (zipWith f m₁ m₂) k).isSome ↔
+      (get? m₁ k).isSome ∧ (get? m₂ k).isSome := by
+  rw [get?_zipWith]
+  cases h1 : get? m₁ k <;> cases h2 : get? m₂ k <;> simp
+
+theorem zip_empty_left {m : M V'} :
+    zip (empty : M V) m ≡ₘ empty := by
+  intro k
+  simp only [zip, zipWith, get?_bindAlter, get?_empty, Option.bind]
+
+theorem zip_empty_right {m : M V} :
+    zip m (empty : M V') ≡ₘ empty := by
+  intro k
+  simp only [zip, zipWith, get?_bindAlter, get?_empty, Option.bind]
+  cases h : get? m k <;> simp
+
+-- -- FIXME: universe issue
+-- theorem zip_insert {m₁ : M V} {m₂ : M V'} {k : K} {v : V} {v' : V'} :
+--     zip (insert m₁ k v) (insert m₂ k v') ≡ₘ insert (zip m₁ m₂) k (v, v') := by
+--   sorry
+
+-- FIXME: universe issue
+-- theorem zip_delete {m₁ : M V} {m₂ : M V'} {k : K} :
+--     zip (delete m₁ k) (delete m₂ k) ≡ₘ delete (zip m₁ m₂) k := by
+--   sorry
+
+theorem isSome_zip {m₁ : M V} {m₂ : M V'} {k : K} :
+    (get? (zip m₁ m₂) k).isSome ↔ (get? m₁ k).isSome ∧ (get? m₂ k).isSome := by
+  rw [get?_zip]
+  cases h1 : get? m₁ k <;> cases h2 : get? m₂ k <;> simp
+
+theorem ofList_cons {L : List (K × V)} : ofList (M := M) ((k, v) :: L) = insert (ofList L) k v :=
+  rfl
+
+theorem noDupKeys_cons {L : List (K × V)} : NoDupKeys (h :: L) → NoDupKeys L := by
+  unfold NoDupKeys
+  grind
+
+theorem noDupKeys_inj {L : List (K × V)} (Hdup : NoDupKeys L) (Hin : (k, v) ∈ L)
+    (Hin' : (k, v') ∈ L) : v = v' := by
+  induction L with
+  | nil => cases Hin
+  | cons h t IH =>
+    obtain ⟨k₀, v₀⟩ := h
+    simp [NoDupKeys, List.map_cons] at Hdup
+    obtain ⟨hnotin, ht⟩ := Hdup
+    simp at Hin Hin'
+    cases Hin with
+    | inl heq =>
+      cases Hin' with
+      | inl heq' => exact heq.2.trans heq'.2.symm
+      | inr hmem => grind
+    | inr hmem =>
+      cases Hin' with
+      | inl heq' => grind
+      | inr hmem' => exact IH ht hmem hmem'
+
+theorem get?_ofList_some [DecidableEq K] {L : List (K × V)}
+    (Hin : (k, v) ∈ L) (Hdup : NoDupKeys L) : get? (ofList (M := M) L) k = some v := by
+  induction L
+  · simp at Hin
+  rename_i h t IH
+  obtain ⟨k', v'⟩ := h
+  rw [ofList_cons]
+  rcases List.eq_or_mem_of_mem_cons Hin with ⟨rfl, rfl⟩|Hin'
+  · rw [get?_insert_eq rfl]
+  · rw [get?_insert_some_iff]
+    by_cases Hk : k' = k
+    · exact .inl ⟨Hk, (noDupKeys_inj Hdup Hin (Hk ▸ List.mem_cons_self)).symm⟩
+    · exact .inr ⟨Ne.intro Hk, IH Hin' (noDupKeys_cons Hdup)⟩
+
+theorem get?_ofList_none {L : List (K × V)}
+    (Hin : ¬ ∃ v, (k, v) ∈ L) (Hdup : NoDupKeys L) :
+    get? (ofList (M := M) L) k = none  := by
+  induction L
+  · simp [ofList, get?_empty]
+  rename_i h t IH
+  obtain ⟨k', v'⟩ := h
+  rw [ofList_cons]
+  by_cases h : k' = k
+  · exact (Hin ⟨v', h ▸ List.mem_cons_self⟩).elim
+  · rw [get?_insert_ne h]
+    exact IH (by grind) (noDupKeys_cons Hdup)
+
 end LawfulPartialMap
+
+namespace LawfulFiniteMap
+
+variable {K V : Type _} {M : Type _ → Type _} [LawfulFiniteMap M K]
+
+open FiniteMap LawfulFiniteMap PartialMap LawfulPartialMap
+
+-- TODO: These should be theorems
+-- mapFold_empty {f : K → V → A → A} : mapFold f a ∅ = a
+-- mapFold_ind {P : M A → Prop}:
+--   P ∅ →
+--   (∀ i x m,
+--     get? m i = none →
+--     (∀ A' B (f : K → A' → B → B) (g : A → A') b x',
+--       mapFold f b (insert (PartialMap.map g m) i x') =
+--         f i x' (mapFold f b (PartialMap.map g m))) →
+--     P m →
+--     P (insert m i x)) →
+--   ∀ m, P m
+
+theorem toList_get?_none {m : M V} : (∀ v, (k, v) ∉ toList (K := K) m) ↔ get? m k = none := by
+  constructor
+  · intro Hn
+    refine Option.eq_none_iff_forall_ne_some.mpr ?_
+    exact fun v' Hsome => Hn v' <| toList_get.mpr Hsome
+  · intro Hn v Hk
+    cases Hn ▸ toList_get.mp Hk
+
+theorem NoDupKeys_noDup {L : List (K × V)} : NoDupKeys L → L.Nodup := by
+  refine fun H => FromMathlib.List.Nodup.of_map (fun x => x.fst) ?_
+  exact H
+
+theorem nodup_toList {m : M V} : (toList (K := K) m).Nodup :=
+  NoDupKeys_noDup toList_noDupKeys
+
+theorem ofList_toList [DecidableEq K] {m : M V} :
+    PartialMap.equiv (ofList (toList (K := K) m)) m := by
+  intro k
+  rcases h : get? m k with _|v
+  · refine get?_ofList_none ?_ toList_noDupKeys
+    intro ⟨v, Hk⟩
+    cases h ▸ toList_get.mp Hk
+  · exact get?_ofList_some (toList_get.mpr h) toList_noDupKeys
+
+theorem mem_of_mem_ofList [DecidableEq K] {l : List (K × V)} {i : K} {x : V}
+    (H : get? (ofList l : M V) i = some x) : (i, x) ∈ l := by
+  induction l
+  · simp [ofList, get?_empty] at H
+  · rename_i h t IH
+    obtain ⟨k, v⟩ := h
+    rw [ofList_cons] at H
+    by_cases He : k = i
+    · subst He
+      rw [get?_insert_eq rfl] at H
+      obtain ⟨rfl⟩ := H
+      exact List.mem_cons_self
+    · rw [get?_insert_ne He] at H
+      exact List.mem_cons_of_mem (k, v) (IH H)
+
+theorem toList_ofList [DecidableEq K] {l : List (K × V)} (Hdup : NoDupKeys l) :
+    (toList (M := M) (K := K) (ofList l : M V)).Perm l := by
+  refine (List.perm_ext_iff_of_nodup nodup_toList ?_).mpr fun ⟨k, v⟩ => ⟨?_, ?_⟩
+  · exact NoDupKeys_noDup Hdup
+  · exact (mem_of_mem_ofList <| toList_get.mp ·)
+  · exact (toList_get.mpr <| get?_ofList_some · Hdup)
+
+theorem toList_perm_of_get?_eq {m₁ m₂ : M V} (h : ∀ k, get? m₁ k = get? m₂ k) :
+    (toList (M := M) (K := K) m₁).Perm (toList (M := M) (K := K) m₂) := by
+  refine (List.perm_ext_iff_of_nodup nodup_toList nodup_toList).mpr fun ⟨k, v⟩ => ⟨?_, ?_⟩
+  · intro H
+    refine toList_get.mpr ?_
+    rw [← h k]
+    exact toList_get.mp H
+  · intro H
+    refine toList_get.mpr ?_
+    rw [h k]
+    exact toList_get.mp H
+
+theorem toList_insert {m : M V} {k : K} {v : V} (h : get? m k = none) :
+    (toList (M := M) (K := K) (insert m k v)).Perm ((k, v) :: toList (M := M) (K := K) m) := by
+  refine (List.perm_ext_iff_of_nodup nodup_toList ?_).mpr fun ⟨k', v'⟩ => ⟨?_, ?_⟩
+  · refine  List.nodup_cons.mpr ⟨?_, nodup_toList⟩
+    exact fun H => Option.some_ne_none _ (h ▸ toList_get.mp H).symm
+  · intro H
+    have H' := toList_get.mp H
+    by_cases He : k = k'
+    · rw [get?_insert_eq He] at H'
+      obtain ⟨rfl⟩ := H'
+      rw [He]
+      exact List.mem_cons_self
+    · refine List.mem_cons_of_mem (k, v) ?_
+      refine toList_get.mpr ?_
+      rw [get?_insert_ne He] at H'
+      exact H'
+  · intro H
+    cases H
+    · exact toList_get.mpr (get?_insert_eq rfl)
+    · rename_i H
+      by_cases He : k = k'
+      · exfalso
+        subst He
+        cases h ▸ toList_get.mp H
+      · refine toList_get.mpr ?_
+        rw [get?_insert_ne He]
+        refine toList_get.mp H
+
+theorem toList_delete {m : M V} {k : K} {v : V} (h : get? m k = some v) :
+    (toList (M := M) (K := K) m).Perm ((k, v) :: toList (M := M) (K := K) (delete m k)) := by
+  refine (List.perm_ext_iff_of_nodup nodup_toList ?_).mpr fun ⟨k', v'⟩ => ⟨?_, ?_⟩
+  · refine List.nodup_cons.mpr ⟨?_, nodup_toList⟩
+    intro H
+    have Hget := toList_get.mp H
+    rw [get?_delete_eq rfl] at Hget
+    cases Hget
+  · intro H
+    by_cases He : k = k'
+    · subst He
+      obtain ⟨rfl⟩ := h ▸ toList_get.mp H
+      exact List.mem_cons_self
+    · refine List.mem_cons_of_mem (k, v) ?_
+      refine toList_get.mpr ?_
+      rw [get?_delete_ne He]
+      refine toList_get.mp H
+  · intro H
+    cases H
+    · exact toList_get.mpr h
+    · rename_i H'
+      refine toList_get.mpr ?_
+      have H'' := toList_get.mp H'
+      by_cases He : k = k'
+      · rw [get?_delete_eq He] at H''
+        cases H''
+      · rw [get?_delete_ne He] at H''
+        exact H''
+
+theorem all_iff_toList {P : K → V → Prop} {m : M V} :
+    PartialMap.all P m ↔ ∀ kv ∈ toList m, P kv.1 kv.2 :=
+  ⟨fun H ⟨k, v⟩ Hm => H k v (toList_get.mp Hm),
+   fun H k v hg => H (k, v) (toList_get.mpr hg)⟩
+
+theorem mem_ofList [DecidableEq K] {l : List (K × V)} {i : K} {x : V}
+    (hnodup : (l.map Prod.fst).Nodup) :
+    (i, x) ∈ l ↔ get? (ofList l : M V) i = some x :=
+  ⟨(get?_ofList_some · hnodup), mem_of_mem_ofList⟩
+
+theorem ofList_injective [DecidableEq K] {l₁ l₂ : List (K × V)}
+    (hnodup1 : (l₁.map Prod.fst).Nodup) (hnodup2 : (l₂.map Prod.fst).Nodup) :
+    PartialMap.equiv (ofList l₁ : M V) (ofList l₂) → l₁.Perm l₂ := by
+  intro He
+  refine (List.perm_ext_iff_of_nodup (NoDupKeys_noDup hnodup1) (NoDupKeys_noDup hnodup2)).mpr ?_
+  refine fun ⟨k, v⟩ => ⟨fun H => ?_, fun H => ?_⟩
+  · apply mem_of_mem_ofList (M := M)
+    rw [← He k]
+    exact get?_ofList_some H (List.nodup_iff_pairwise_ne.mpr hnodup1)
+  · apply mem_of_mem_ofList (M := M)
+    rw [He k]
+    exact get?_ofList_some H (List.nodup_iff_pairwise_ne.mpr hnodup2)
+
+theorem toList_insert_delete {m : M V} {k : K} {v : V} :
+    (toList (M := M) (K := K) (insert m k v)).Perm
+      (toList (M := M) (K := K) (insert (delete m k) k v)) := by
+  apply toList_perm_of_get?_eq
+  intro k'
+  by_cases h : k = k'
+  · simp [LawfulPartialMap.get?_insert_eq h]
+  · simp [LawfulPartialMap.get?_insert_ne h, LawfulPartialMap.get?_delete_ne h]
+
+theorem toList_map {f : V → V'} {m : M V}  :
+    (toList (M := M) (K := K) (PartialMap.map f m)).Perm
+      ((toList m).map (fun kv => (kv.1, f kv.2))) := by
+  refine (List.perm_ext_iff_of_nodup nodup_toList ?_).mpr fun ⟨k, v⟩ => ⟨?_, ?_⟩
+  · refine FromMathlib.Nodup.map_on ?_ nodup_toList
+    rintro ⟨x₁, y₁⟩ H₁ ⟨x₂, y₂⟩ H₂
+    simp only [Prod.mk.injEq, and_imp]
+    rintro rfl _
+    exact ⟨rfl, noDupKeys_inj toList_noDupKeys H₁ H₂⟩
+  · intro H
+    refine List.mem_map.mpr ?_
+    have H' := toList_get.mp H
+    rw [get?_map] at H'
+    obtain ⟨v, Ha₁, Ha₂⟩ := Option.map_eq_some_iff.mp H'
+    exact ⟨⟨k, v⟩, toList_get.mpr Ha₁, Prod.ext rfl Ha₂⟩
+  · intro H
+    obtain ⟨a, Ha₁, Ha₂⟩ := List.mem_map.mp H
+    obtain ⟨rfl, H⟩ := Ha₂
+    refine toList_get.mpr ?_
+    rw [get?_map, toList_get.mp Ha₁]
+    rfl
+
+theorem toList_filterMap {f : V → Option V} {m : M V} (HI : Function.Injective f) :
+    (toList (M := M) (K := K) (PartialMap.filterMap f m)).Perm
+      ((toList m).filterMap (fun kv => (f kv.2).map (kv.1, ·))) := by
+  refine (List.perm_ext_iff_of_nodup nodup_toList ?_).mpr fun ⟨k, v⟩ => ⟨?_, ?_⟩
+  · refine FromMathlib.Nodup.filterMap ?_ nodup_toList
+    simp only [Option.mem_def, Option.map_eq_some_iff, forall_exists_index, and_imp,
+      forall_apply_eq_imp_iff₂, Prod.mk.injEq, Prod.forall]
+    rintro _ _ _ _ _ H1 _ H2 rfl rfl
+    exact ⟨rfl, HI (H2 ▸ H1)⟩
+  · intro H
+    refine List.mem_filterMap.mpr ?_
+    have H' := toList_get.mp H
+    simp [get?_filterMap] at H'
+    obtain ⟨v', Ha₁, Ha₂⟩ := Option.bind_eq_some_iff.mp H'
+    simp only [Option.map_eq_some_iff]
+    exact ⟨(k, v'), toList_get.mpr Ha₁, v, Ha₂, rfl⟩
+  · intro H
+    obtain ⟨a, Ha₁, Ha₂⟩ := List.mem_filterMap.mp H
+    refine toList_get.mpr ?_
+    rw [get?_filterMap]
+    refine Option.bind_eq_some_iff.mpr ?_
+    simp at Ha₂
+    obtain ⟨H', rfl⟩ := Ha₂
+    refine ⟨a.snd, toList_get.mp Ha₁, H'⟩
+
+theorem toList_filter {φ : K → V → Bool} {m : M V} :
+    (toList (M := M) (K := K) (PartialMap.filter φ m)).Perm
+      ((toList m).filter (fun kv => φ kv.1 kv.2)) := by
+  refine (List.perm_ext_iff_of_nodup nodup_toList ?_).mpr fun ⟨k, v⟩ => ⟨?_, ?_⟩
+  · exact FromMathlib.Nodup.filter ?_ (nodup_toList (M := M) (K := K))
+  · intro H
+    refine List.mem_filter.mpr ?_
+    have H' := toList_get.mp H
+    simp only [get?_filter] at H'
+    obtain ⟨v', Ha₁, Ha₂⟩ := Option.bind_eq_some_iff.mp H'
+    by_cases h : φ k v'
+    · simp only [h, ↓reduceIte, Option.some.injEq] at Ha₂
+      subst Ha₂
+      exact ⟨toList_get.mpr Ha₁, h⟩
+    · simp [h] at Ha₂
+  · intro H
+    refine toList_get.mpr ?_
+    simp only [List.mem_filter] at H
+    simp [get?_filter, toList_get.mp H.1, H.2]
+
+theorem toList_zip {m₁ : M V} {m₂ : M V'} :
+    (toList (M := M) (K := K) (PartialMap.zip m₁ m₂)).Perm
+      ((toList m₁).filterMap fun kv₁ =>
+        (get? m₂ kv₁.1).map fun v₂ => (kv₁.1, (kv₁.2, v₂))) := by
+  refine (List.perm_ext_iff_of_nodup nodup_toList ?_).mpr fun ⟨k, v⟩ => ⟨?_, ?_⟩
+  · refine FromMathlib.Nodup.filterMap ?_ nodup_toList
+    simp only [Option.mem_def, Option.map_eq_some_iff, forall_exists_index, and_imp,
+      forall_apply_eq_imp_iff₂, Prod.mk.injEq, Prod.forall]
+    rintro _ _ _ _ _ _ _ _ rfl rfl rfl; exact ⟨rfl, rfl⟩
+  · intro H
+    refine List.mem_filterMap.mpr ?_
+    have H' := toList_get.mp H
+    simp [get?_zip] at H'
+    obtain ⟨v', Ha₁, Ha₂⟩ := Option.bind_eq_some_iff.mp H'
+    simp only [Option.map_eq_some_iff]
+    simp only [Option.map_eq_some_iff] at Ha₂
+    obtain ⟨b, Hb₁, Hb₂⟩ := Ha₂
+    exact ⟨(k, v'), toList_get.mpr Ha₁, _, Hb₁, Prod.ext rfl Hb₂⟩
+  · intro H
+    obtain ⟨a, Ha₁, Ha₂⟩ := List.mem_filterMap.mp H
+    refine toList_get.mpr ?_
+    rw [get?_zip]
+    refine Option.bind_eq_some_iff.mpr ?_
+    simp at Ha₂
+    obtain ⟨b, Hb₁, rfl, rfl⟩ := Ha₂
+    refine ⟨a.2, toList_get.mp Ha₁, ?_⟩
+    simp [Hb₁]
+
+end LawfulFiniteMap
+
+
 end Iris.Std