diff --git a/PORTING.md b/PORTING.md
index 8d7045bf..fe78f619 100644
--- a/PORTING.md
+++ b/PORTING.md
@@ -69,9 +69,9 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] CMRA
   - [ ] Functors
 - [x] `local_updates.v`
-- [ ] `max_prefix_list.v` 
-  - [ ] Lemmas
-  - [ ] Functors
+- [x] `max_prefix_list.v` 
+  - [x] Lemmas
+  - [x] Functors
 - [ ] `monoid.v`
 - [ ] `mra.v`
 - [x] `numbers.v`
@@ -132,9 +132,9 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] Functors
 - [ ] `lib/gset_bij.v` 
 - [ ] `lib/mono_Z.v` (nb. generalize to `MonoNumbers.lean`)
-- [ ] `lib/mono_list.v` 
-  - [ ] Lemmas
-  - [ ] Functors
+- [x] `lib/mono_list.v` 
+  - [x] Lemmas
+  - [x] Functors
 - [ ] `lib/mono_nat.v` (nb. generalize to `MonoNumbers.lean`)
 - [ ] `lib/ufrac_auth.v` 
   - [ ] Lemmas
diff --git a/src/Iris/Algebra.lean b/src/Iris/Algebra.lean
index 30043dc5..c75ec81f 100644
--- a/src/Iris/Algebra.lean
+++ b/src/Iris/Algebra.lean
@@ -7,6 +7,8 @@ import Iris.Algebra.Frac
 import Iris.Algebra.GenMap
 import Iris.Algebra.LocalUpdates
 import Iris.Algebra.IProp
+import Iris.Algebra.MaxPrefixList
+import Iris.Algebra.MonoList
 import Iris.Algebra.OFE
 import Iris.Algebra.Updates
 import Iris.Algebra.UPred
diff --git a/src/Iris/Algebra/MaxPrefixList.lean b/src/Iris/Algebra/MaxPrefixList.lean
new file mode 100644
index 00000000..cfbac490
--- /dev/null
+++ b/src/Iris/Algebra/MaxPrefixList.lean
@@ -0,0 +1,321 @@
+import Iris.Algebra.Agree
+import Iris.Algebra.GenMap
+import Iris.Algebra.LocalUpdates
+
+namespace Iris
+
+open OFE CMRA
+
+abbrev MaxPrefixList (A : Type _) [OFE A] := GenMap Nat (Agree A)
+
+def toMaxPrefixList {A : Type _} [OFE A] (l : List A) : MaxPrefixList A :=
+  ⟨fun i => (l[i]?).map toAgree⟩
+
+def shiftMaxPrefixList {A : Type _} [OFE A] (start : Nat) (l : List A) : MaxPrefixList A :=
+  ⟨fun i => if _h : start ≤ i then (l[i - start]?).map toAgree else none⟩
+
+instance {A : Type _} [OFE A] (m : MaxPrefixList A) : CoreId m := by
+  rw [CMRA.coreId_iff_core_eqv_self]
+  show (core m).car ≡ m.car
+  intro i
+  change core (m.car i) ≡ m.car i
+  cases h : m.car i <;> rfl
+
+instance toMaxPrefixList_ne {A : Type _} [OFE A] : NonExpansive (toMaxPrefixList (A := A)) where
+  ne := by
+    intro n x1 x2 h i
+    unfold toMaxPrefixList
+    specialize h i
+    cases h1 : x1[i]? <;> cases h2 : x2[i]? <;> simp [h1, h2] at h ⊢
+    exact OFE.NonExpansive.ne h
+
+theorem toMaxPrefixList_valid {A : Type _} [OFE A] (l : List A) : ✓ toMaxPrefixList l := by
+  constructor
+  · intro i
+    unfold toMaxPrefixList
+    cases h : l[i]? <;> simp [h, CMRA.Valid, Agree.valid, Agree.validN, toAgree]
+  · refine ⟨fun n => l.length + n, ?_, ?_⟩
+    · intro n
+      unfold IsFree toMaxPrefixList
+      simp [Nat.le_add_right]
+    · intro n m h
+      omega
+
+theorem toMaxPrefixList_validN {A : Type _} [OFE A] (n : Nat) (l : List A) : ✓{n} toMaxPrefixList l :=
+  (toMaxPrefixList_valid (A := A) l).validN
+
+theorem toMaxPrefixList_dist_inj {A : Type _} [OFE A] {l1 l2 : List A} :
+    toMaxPrefixList (A := A) l1 ≡{n}≡ toMaxPrefixList l2 → l1 ≡{n}≡ l2 := by
+  intro h
+  intro i
+  specialize h i
+  unfold toMaxPrefixList at h
+  cases h1 : l1[i]? <;> cases h2 : l2[i]? <;> simp [h1, h2] at h ⊢
+  exact Agree.toAgree_injN h
+
+theorem toMaxPrefixList_inj {A : Type _} [OFE A] {l1 l2 : List A} :
+    toMaxPrefixList (A := A) l1 ≡ toMaxPrefixList l2 → l1 ≡ l2 := by
+  intro h
+  intro i
+  specialize h i
+  unfold toMaxPrefixList at h
+  cases h1 : l1[i]? <;> cases h2 : l2[i]? <;> simp [h1, h2] at h ⊢
+  exact Agree.toAgree_inj h
+
+theorem toMaxPrefixList_app {A : Type _} [OFE A] (l1 l2 : List A) :
+    toMaxPrefixList (A := A) (l1 ++ l2) ≡
+      toMaxPrefixList l1 • shiftMaxPrefixList l1.length l2 := by
+  intro i
+  simp [toMaxPrefixList, shiftMaxPrefixList, CMRA.op]
+  by_cases h : i < l1.length
+  · rw [List.getElem?_append_left h]
+    simp [h, Nat.not_le_of_gt h]
+  · have hle : l1.length ≤ i := Nat.le_of_not_lt h
+    rw [List.getElem?_append_right hle]
+    simp [h, hle]
+
+theorem toMaxPrefixList_op_l {A : Type _} [OFE A] {l1 l2 : List A} :
+    l1 <+: l2 → toMaxPrefixList l1 • toMaxPrefixList l2 ≡ toMaxPrefixList l2 := by
+  intro h
+  have hl : l1 ++ List.drop l1.length l2 = l2 := List.prefix_iff_eq_append.mp h
+  have happ : toMaxPrefixList (A := A) (l1 ++ List.drop l1.length l2) ≡
+      toMaxPrefixList l1 • shiftMaxPrefixList l1.length (List.drop l1.length l2) :=
+    toMaxPrefixList_app (A := A) l1 (List.drop l1.length l2)
+  have hidem : toMaxPrefixList (A := A) l1 • toMaxPrefixList l1 ≡ toMaxPrefixList l1 := by
+    intro i
+    unfold toMaxPrefixList
+    cases h : l1[i]? <;> simp [h, CMRA.op, Agree.idemp]
+  calc
+    toMaxPrefixList l1 • toMaxPrefixList l2
+        ≡ toMaxPrefixList l1 • toMaxPrefixList (l1 ++ List.drop l1.length l2) := by rw [hl]
+    _ ≡ toMaxPrefixList l1 • (toMaxPrefixList l1 • shiftMaxPrefixList l1.length (List.drop l1.length l2)) := happ.op_r
+    _ ≡ (toMaxPrefixList l1 • toMaxPrefixList l1) • shiftMaxPrefixList l1.length (List.drop l1.length l2) := assoc
+    _ ≡ toMaxPrefixList l1 • shiftMaxPrefixList l1.length (List.drop l1.length l2) := hidem.op_l
+    _ ≡ toMaxPrefixList (l1 ++ List.drop l1.length l2) := happ.symm
+    _ ≡ toMaxPrefixList l2 := by rw [hl]
+
+theorem toMaxPrefixList_op_r {A : Type _} [OFE A] {l1 l2 : List A} :
+    l1 <+: l2 → toMaxPrefixList l2 • toMaxPrefixList l1 ≡ toMaxPrefixList l2 := by
+  intro h
+  exact comm.trans (toMaxPrefixList_op_l (A := A) h)
+
+theorem maxPrefixList_included_includedN {A : Type _} [OFE A] (m1 m2 : MaxPrefixList A) :
+    m1 ≼ m2 ↔ ∀ n, m1 ≼{n} m2 := by
+  constructor
+  · intro h n
+    exact CMRA.incN_of_inc n h
+  · intro h
+    refine ⟨m2, ?_⟩
+    exact OFE.equiv_dist.2 fun n => by
+      rcases h n with ⟨z, hz⟩
+      have hm : m1 • m2 ≡{n}≡ m2 := by
+        calc
+          m1 • m2 ≡{n}≡ m1 • (m1 • z) := hz.op_r
+          _ ≡{n}≡ (m1 • m1) • z := CMRA.op_assocN
+          _ ≡{n}≡ m1 • z := (CMRA.op_self (m1 : MaxPrefixList A)).dist.op_l
+          _ ≡{n}≡ m2 := hz.symm
+      exact hm.symm
+
+theorem toMaxPrefixList_op_validN_aux {A : Type _} [OFE A] (n : Nat) (l1 l2 : List A) :
+    l1.length ≤ l2.length →
+      ✓{n} (toMaxPrefixList (A := A) l1 • toMaxPrefixList l2) →
+        l2 ≡{n}≡ l1 ++ List.drop l1.length l2 := by
+  intro hlen hvalid
+  intro i
+  by_cases hi : i < l1.length
+  · have hi2 : i < l2.length := Nat.lt_of_lt_of_le hi hlen
+    have hv : ✓{n} (Option.map toAgree l1[i]? • Option.map toAgree l2[i]?) := by
+      simpa [toMaxPrefixList, CMRA.op] using hvalid.1 i
+    have h1 : l1[i]? = some l1[i] := List.getElem?_eq_getElem hi
+    have h2 : l2[i]? = some l2[i] := List.getElem?_eq_getElem hi2
+    rw [List.getElem?_append_left hi, h1, h2]
+    rw [h1, h2] at hv
+    exact (Agree.toAgree_op_validN_iff_dist (a := l1[i]) (b := l2[i])).1 hv |>.symm
+  · have hge : l1.length ≤ i := Nat.le_of_not_lt hi
+    rw [List.getElem?_append_right hge, List.getElem?_drop]
+    have hs : l1.length + (i - l1.length) = i := Nat.add_sub_of_le hge
+    simp [hs]
+
+theorem toMaxPrefixList_op_validN {A : Type _} [OFE A] (n : Nat) (l1 l2 : List A) :
+    ✓{n} (toMaxPrefixList (A := A) l1 • toMaxPrefixList l2) ↔
+      (∃ t, l2 ≡{n}≡ l1 ++ t) ∨ (∃ t, l1 ≡{n}≡ l2 ++ t) := by
+  constructor
+  · intro h
+    by_cases hlen : l1.length ≤ l2.length
+    · left
+      exact ⟨List.drop l1.length l2, toMaxPrefixList_op_validN_aux (A := A) n l1 l2 hlen h⟩
+    · right
+      have hcomm : ✓{n} (toMaxPrefixList (A := A) l2 • toMaxPrefixList l1) := CMRA.validN_ne (CMRA.comm.dist) h
+      have hlen' : l2.length ≤ l1.length := Nat.le_of_lt (Nat.lt_of_not_ge hlen)
+      exact ⟨List.drop l2.length l1, toMaxPrefixList_op_validN_aux (A := A) n l2 l1 hlen' hcomm⟩
+  · rintro (⟨t, ht⟩ | ⟨t, ht⟩)
+    · have hp : l1 <+: l1 ++ t := ⟨t, rfl⟩
+      have hEqMap : toMaxPrefixList (A := A) l2 ≡{n}≡ toMaxPrefixList (l1 ++ t) := toMaxPrefixList_ne.ne ht
+      have hvalid : ✓{n} (toMaxPrefixList (A := A) l1 • toMaxPrefixList (l1 ++ t)) :=
+        (toMaxPrefixList_op_l (A := A) hp).dist.validN.mpr (toMaxPrefixList_validN (A := A) n (l1 ++ t))
+      exact CMRA.validN_ne ((hEqMap.op_r).symm) hvalid
+    · have hp : l2 <+: l2 ++ t := ⟨t, rfl⟩
+      have hEqMap : toMaxPrefixList (A := A) l1 ≡{n}≡ toMaxPrefixList (l2 ++ t) := toMaxPrefixList_ne.ne ht
+      have hvalid : ✓{n} (toMaxPrefixList (A := A) (l2 ++ t) • toMaxPrefixList l2) :=
+        (toMaxPrefixList_op_r (A := A) hp).dist.validN.mpr (toMaxPrefixList_validN (A := A) n (l2 ++ t))
+      exact CMRA.validN_ne ((hEqMap.op_l).symm) hvalid
+
+theorem toMaxPrefixList_op_valid {A : Type _} [OFE A] (l1 l2 : List A) :
+    ✓ (toMaxPrefixList (A := A) l1 • toMaxPrefixList l2) ↔
+      (∃ t, l2 ≡ l1 ++ t) ∨ (∃ t, l1 ≡ l2 ++ t) := by
+  rw [CMRA.valid_iff_validN]
+  constructor
+  · intro h
+    by_cases hlen : l1.length ≤ l2.length
+    · left
+      refine ⟨List.drop l1.length l2, ?_⟩
+      exact OFE.equiv_dist.2 fun n => toMaxPrefixList_op_validN_aux (A := A) n l1 l2 hlen (h n)
+    · right
+      have hlen' : l2.length ≤ l1.length := Nat.le_of_lt (Nat.lt_of_not_ge hlen)
+      refine ⟨List.drop l2.length l1, ?_⟩
+      exact OFE.equiv_dist.2 fun n =>
+        toMaxPrefixList_op_validN_aux (A := A) n l2 l1 hlen' (CMRA.validN_ne (CMRA.comm.dist) (h n))
+  · intro h n
+    exact (toMaxPrefixList_op_validN (A := A) n l1 l2).2 <|
+      match h with
+      | Or.inl ⟨t, ht⟩ => Or.inl ⟨t, ht.dist⟩
+      | Or.inr ⟨t, ht⟩ => Or.inr ⟨t, ht.dist⟩
+
+theorem toMaxPrefixList_mono {A : Type _} [OFE A] {l1 l2 : List A} :
+    l1 <+: l2 → toMaxPrefixList l1 ≼ toMaxPrefixList l2 := by
+  intro h
+  have hl : l1 ++ List.drop l1.length l2 = l2 := List.prefix_iff_eq_append.mp h
+  let z := shiftMaxPrefixList (A := A) l1.length (List.drop l1.length l2)
+  have happ : toMaxPrefixList (A := A) (l1 ++ List.drop l1.length l2) ≡
+      toMaxPrefixList l1 • z := by
+    simpa [z] using toMaxPrefixList_app (A := A) l1 (List.drop l1.length l2)
+  refine ⟨z, ?_⟩
+  exact (OFE.Equiv.of_eq (by simp [hl])).trans happ
+
+theorem toMaxPrefixList_includedN {A : Type _} [OFE A] (n : Nat) (l1 l2 : List A) :
+    toMaxPrefixList (A := A) l1 ≼{n} toMaxPrefixList l2 ↔ ∃ t, l2 ≡{n}≡ l1 ++ t := by
+  constructor
+  · intro h
+    rcases h with ⟨z, hz⟩
+    refine ⟨List.drop l1.length l2, ?_⟩
+    intro i
+    by_cases hi : i < l1.length
+    · have h1 : l1[i]? = some l1[i] := List.getElem?_eq_getElem hi
+      rw [List.getElem?_append_left hi, h1]
+      have hiinc : some (toAgree l1[i]) ≼{n} (toMaxPrefixList (A := A) l2).car i := by
+        refine ⟨z.car i, ?_⟩
+        simpa [toMaxPrefixList, CMRA.op, h1] using hz i
+      cases h2 : l2[i]? with
+      | none =>
+          have : some (toAgree l1[i]) ≼{n} none := by simpa [toMaxPrefixList, h2] using hiinc
+          rcases this with ⟨w, hEq⟩
+          cases w with
+          | none => exact False.elim (not_none_dist_some hEq)
+          | some val => exact False.elim (not_none_dist_some hEq)
+      | some y =>
+          have hiinc' : some (toAgree l1[i]) ≼{n} some (toAgree y) := by
+            simpa [toMaxPrefixList, h2] using hiinc
+          have hagree : toAgree l1[i] ≼{n} toAgree y := Option.some_incN_some_iff_isTotal.mp hiinc'
+          have hy : l1[i] ≡{n}≡ y := Agree.toAgree_includedN.mp hagree
+          have hi2 : i < l2.length := (List.getElem?_eq_some_iff.mp h2).1
+          simpa [List.getElem?_eq_getElem hi2, h2] using hy.symm
+    · have hge : l1.length ≤ i := Nat.le_of_not_lt hi
+      rw [List.getElem?_append_right hge, List.getElem?_drop]
+      have hs : l1.length + (i - l1.length) = i := Nat.add_sub_of_le hge
+      simp [hs]
+  · rintro ⟨t, ht⟩
+    have happ : toMaxPrefixList (A := A) (l1 ++ t) ≡{n}≡
+        (toMaxPrefixList l1 • shiftMaxPrefixList l1.length t) := (toMaxPrefixList_app (A := A) l1 t).dist
+    have hbase : toMaxPrefixList (A := A) l1 ≼{n} (toMaxPrefixList l1 • shiftMaxPrefixList l1.length t) :=
+      CMRA.incN_op_left n _ _
+    have hstep : toMaxPrefixList (A := A) l1 ≼{n} toMaxPrefixList (l1 ++ t) := (happ.incN_r).mpr hbase
+    have hmap : toMaxPrefixList (A := A) (l1 ++ t) ≡{n}≡ toMaxPrefixList l2 := toMaxPrefixList_ne.ne ht.symm
+    exact (hmap.incN_r).mp hstep
+
+theorem toMaxPrefixList_included {A : Type _} [OFE A] (l1 l2 : List A) :
+    toMaxPrefixList (A := A) l1 ≼ toMaxPrefixList l2 ↔ ∃ t, l2 ≡ l1 ++ t := by
+  constructor
+  · intro h
+    rcases h with ⟨z, hz⟩
+    refine ⟨List.drop l1.length l2, ?_⟩
+    intro i
+    by_cases hi : i < l1.length
+    · have h1 : l1[i]? = some l1[i] := List.getElem?_eq_getElem hi
+      rw [List.getElem?_append_left hi, h1]
+      have hiinc : some (toAgree l1[i]) ≼ (toMaxPrefixList (A := A) l2).car i := by
+        refine ⟨z.car i, ?_⟩
+        simpa [toMaxPrefixList, CMRA.op, h1] using hz i
+      cases h2 : l2[i]? with
+      | none =>
+          have : some (toAgree l1[i]) ≼ none := by simpa [toMaxPrefixList, h2] using hiinc
+          rcases this with ⟨w, hEq⟩
+          cases w with
+          | none => exact False.elim (not_none_eqv_some hEq)
+          | some val => exact False.elim (not_none_eqv_some hEq)
+      | some y =>
+          have hiinc' : some (toAgree l1[i]) ≼ some (toAgree y) := by
+            simpa [toMaxPrefixList, h2] using hiinc
+          have hagree : toAgree l1[i] ≼ toAgree y := Option.some_inc_some_iff_isTotal.mp hiinc'
+          have hy : l1[i] ≡ y := Agree.toAgree_included.mp hagree
+          have hi2 : i < l2.length := (List.getElem?_eq_some_iff.mp h2).1
+          simpa [List.getElem?_eq_getElem hi2, h2] using hy.symm
+    · have hge : l1.length ≤ i := Nat.le_of_not_lt hi
+      rw [List.getElem?_append_right hge, List.getElem?_drop]
+      have hs : l1.length + (i - l1.length) = i := Nat.add_sub_of_le hge
+      simp [hs]
+  · rintro ⟨t, ht⟩
+    refine ⟨shiftMaxPrefixList (A := A) l1.length t, ?_⟩
+    calc
+      toMaxPrefixList (A := A) l2 ≡ toMaxPrefixList (l1 ++ t) := OFE.NonExpansive.eqv ht
+      _ ≡ toMaxPrefixList l1 • shiftMaxPrefixList l1.length t := toMaxPrefixList_app (A := A) l1 t
+
+theorem toMaxPrefixList_included_L {A : Type _} [OFE A] [Leibniz A] (l1 l2 : List A) :
+    toMaxPrefixList (A := A) l1 ≼ toMaxPrefixList l2 ↔ l1 <+: l2 := by
+  rw [toMaxPrefixList_included]
+  constructor
+  · rintro ⟨t, ht⟩
+    exact ⟨t, Leibniz.eq_of_eqv ht.symm⟩
+  · rintro ⟨t, rfl⟩
+    exact ⟨t, Equiv.rfl⟩
+
+theorem maxPrefixList_localUpdate {A : Type _} [OFE A] {l1 l2 : List A} :
+    l1 <+: l2 →
+      (toMaxPrefixList l1, toMaxPrefixList l1) ~l~>
+        (toMaxPrefixList l2, toMaxPrefixList l2) := by
+  intro h
+  have hl : l1 ++ List.drop l1.length l2 = l2 := List.prefix_iff_eq_append.mp h
+  let z := shiftMaxPrefixList (A := A) l1.length (List.drop l1.length l2)
+  have happ := toMaxPrefixList_app (A := A) l1 (List.drop l1.length l2)
+  have hzEq : z • toMaxPrefixList l1 ≡ toMaxPrefixList l2 := by
+    calc
+      z • toMaxPrefixList l1 ≡ toMaxPrefixList l1 • z := comm
+      _ ≡ toMaxPrefixList (l1 ++ List.drop l1.length l2) := happ.symm
+      _ ≡ toMaxPrefixList l2 := by rw [hl]
+  have hz : ∀ n, ✓{n} toMaxPrefixList l1 → ✓{n} (z • toMaxPrefixList l1) := by
+    intro n _
+    exact hzEq.dist.validN.mpr (toMaxPrefixList_valid (A := A) l2).validN
+  exact LocalUpdate.equiv_right (x := (toMaxPrefixList l1, toMaxPrefixList l1))
+    (y := (z • toMaxPrefixList l1, z • toMaxPrefixList l1))
+    (z := (toMaxPrefixList l2, toMaxPrefixList l2))
+    ⟨hzEq, hzEq⟩
+    (LocalUpdate.op (x := toMaxPrefixList l1) (y := toMaxPrefixList l1) (z := z) hz)
+
+abbrev MaxPrefixListURF (F : COFE.OFunctorPre) [RFunctor F] : COFE.OFunctorPre :=
+  GenMapOF Nat (AgreeRF F)
+
+instance {F} [RFunctor F] : URFunctor (MaxPrefixListURF F) := by
+  simpa [MaxPrefixListURF] using (inferInstance : URFunctor (GenMapOF Nat (AgreeRF F)))
+
+instance {F} [RFunctorContractive F] : URFunctorContractive (MaxPrefixListURF F) := by
+  simpa [MaxPrefixListURF] using (inferInstance : URFunctorContractive (GenMapOF Nat (AgreeRF F)))
+
+abbrev MaxPrefixListRF (F : COFE.OFunctorPre) [RFunctor F] : COFE.OFunctorPre :=
+  GenMapOF Nat (AgreeRF F)
+
+instance {F} [RFunctor F] : RFunctor (MaxPrefixListRF F) := by
+  simpa [MaxPrefixListRF] using (inferInstance : RFunctor (GenMapOF Nat (AgreeRF F)))
+
+instance {F} [RFunctorContractive F] : RFunctorContractive (MaxPrefixListRF F) := by
+  simpa [MaxPrefixListRF] using (inferInstance : RFunctorContractive (GenMapOF Nat (AgreeRF F)))
+
+end Iris
diff --git a/src/Iris/Algebra/MonoList.lean b/src/Iris/Algebra/MonoList.lean
new file mode 100644
index 00000000..f278801a
--- /dev/null
+++ b/src/Iris/Algebra/MonoList.lean
@@ -0,0 +1,447 @@
+import Iris.Algebra.Auth
+import Iris.Algebra.MaxPrefixList
+
+namespace Iris
+
+open OFE CMRA Auth
+
+abbrev MonoListRes (Q : Type _) (A : Type _) [UFraction Q] [OFE A] := Auth Q (MaxPrefixList A)
+
+namespace MonoList
+
+variable {Q A : Type _} [UFraction Q] [OFE A]
+
+def monoListAuth (dq : DFrac Q) (l : List A) : MonoListRes Q A :=
+  (Auth.auth dq (toMaxPrefixList l)) • Auth.frag (toMaxPrefixList l)
+
+def monoListLb (l : List A) : MonoListRes Q A :=
+  Auth.frag (toMaxPrefixList l)
+
+instance monoListAuth_ne (dq : DFrac Q) : NonExpansive (@monoListAuth Q A _ _ dq) where
+  ne := by
+    intro n x y h
+    unfold monoListAuth
+    exact (Auth.auth_ne (F := Q) (dq := dq)).ne (toMaxPrefixList_ne.ne h) |>.op
+      ((Auth.frag_ne (F := Q)).ne (toMaxPrefixList_ne.ne h))
+
+instance monoListLb_ne : NonExpansive (@monoListLb Q A _ _) where
+  ne := by
+    intro n x y h
+    unfold monoListLb
+    exact (Auth.frag_ne (F := Q)).ne (toMaxPrefixList_ne.ne h)
+
+instance monoListLb_coreId (l : List A) : CoreId (monoListLb (Q := Q) l) := by
+  unfold monoListLb
+  infer_instance
+
+instance monoListAuth_coreId (l : List A) : CoreId (monoListAuth (Q := Q) DFrac.discard l) := by
+  unfold monoListAuth
+  infer_instance
+
+theorem monoListLbDistInj {l1 l2 : List A} :
+    monoListLb (Q := Q) l1 ≡{n}≡ monoListLb l2 → l1 ≡{n}≡ l2 := by
+  intro h
+  exact toMaxPrefixList_dist_inj (A := A) ((Auth.frag_dist_inj (F := Q) h))
+
+theorem monoListLbInj {l1 l2 : List A} :
+    monoListLb (Q := Q) l1 ≡ monoListLb l2 → l1 ≡ l2 := by
+  intro h
+  exact toMaxPrefixList_inj (A := A) ((Auth.frag_inj (F := Q) h))
+
+theorem monoListAuthDfracValidN (n : Nat) (dq : DFrac Q) (l : List A) :
+    ✓{n} (monoListAuth (Q := Q) dq l) ↔ ✓ dq := by
+  unfold monoListAuth
+  rw [Auth.both_dfrac_validN]
+  constructor
+  · rintro ⟨hdq, _, _⟩
+    exact hdq
+  · intro hdq
+    exact ⟨hdq, CMRA.incN_refl _, toMaxPrefixList_validN (A := A) n l⟩
+
+theorem monoListAuthDfracValid (dq : DFrac Q) (l : List A) :
+    ✓ (monoListAuth (Q := Q) dq l) ↔ ✓ dq := by
+  unfold monoListAuth
+  rw [Auth.both_dfrac_valid]
+  constructor
+  · rintro ⟨hdq, _, _⟩
+    exact hdq
+  · intro hdq
+    exact ⟨hdq, fun _ => CMRA.incN_refl _, toMaxPrefixList_valid (A := A) l⟩
+
+theorem monoListAuthValid (l : List A) :
+    ✓ (monoListAuth (Q := Q) (DFrac.own (1 : Q)) l) := by
+  rw [monoListAuthDfracValid]
+  exact DFrac.valid_own_one
+
+theorem monoListAuthValidN (n : Nat) (l : List A) :
+    ✓{n} (monoListAuth (Q := Q) (DFrac.own (1 : Q)) l) := by
+  rw [monoListAuthDfracValidN]
+  exact DFrac.valid_own_one
+
+theorem monoListAuthLbOp (dq : DFrac Q) (l : List A) :
+    monoListAuth (Q := Q) dq l ≡ monoListAuth dq l • monoListLb l := by
+  simpa [monoListAuth, monoListLb] using
+    (CMRA.op_core_left_of_inc
+      (x := monoListLb (Q := Q) l)
+      (y := monoListAuth (Q := Q) dq l)
+      (by
+        unfold monoListLb monoListAuth
+        exact ⟨Auth.auth dq (toMaxPrefixList l), comm⟩)).symm
+
+theorem monoListAuthDfracOp (dq1 dq2 : DFrac Q) (l : List A) :
+    monoListAuth (Q := Q) (dq1 • dq2) l ≡
+      monoListAuth dq1 l • monoListAuth dq2 l := by
+  let a : MaxPrefixList A := toMaxPrefixList (A := A) l
+  let x1 : MonoListRes Q A := Auth.auth (F := Q) dq1 a
+  let x2 : MonoListRes Q A := Auth.auth (F := Q) dq2 a
+  let f : MonoListRes Q A := Auth.frag a
+  have hGroup : ((x1 • f) • (x2 • f) : MonoListRes Q A) ≡ ((x1 • x2) • (f • f) : MonoListRes Q A) := by
+    calc
+      ((x1 • f) • (x2 • f) : MonoListRes Q A) ≡ (((x1 • f) • x2) • f : MonoListRes Q A) := assoc
+      _ ≡ (((x1 • x2) • f) • f : MonoListRes Q A) := by
+            exact (calc
+              (((x1 • f) • x2) : MonoListRes Q A) ≡ (x1 • (f • x2) : MonoListRes Q A) := assoc.symm
+              _ ≡ (x1 • (x2 • f) : MonoListRes Q A) := by exact OFE.Equiv.op_r comm
+              _ ≡ (((x1 • x2) • f) : MonoListRes Q A) := assoc).op_l
+      _ ≡ ((x1 • x2) • (f • f) : MonoListRes Q A) := assoc.symm
+  change ((Auth.auth (F := Q) (dq1 • dq2) a) • f : MonoListRes Q A) ≡ ((x1 • f) • (x2 • f) : MonoListRes Q A)
+  calc
+    ((Auth.auth (F := Q) (dq1 • dq2) a) • f : MonoListRes Q A)
+        ≡ ((x1 • x2) • f : MonoListRes Q A) := (Auth.auth_dfrac_op (F := Q) (dq1 := dq1) (dq2 := dq2) (a := a)).op_l
+    _ ≡ ((x1 • x2) • (f • f) : MonoListRes Q A) := (CMRA.op_self f).symm.op_r
+    _ ≡ ((x1 • f) • (x2 • f) : MonoListRes Q A) := hGroup.symm
+
+theorem monoListLbOpL {l1 l2 : List A} :
+    l1 <+: l2 → monoListLb (Q := Q) l1 • monoListLb l2 ≡ monoListLb l2 := by
+  intro h
+  unfold monoListLb
+  calc
+    ((Auth.frag (toMaxPrefixList l1) • Auth.frag (toMaxPrefixList l2)) : MonoListRes Q A)
+        ≡ (Auth.frag (toMaxPrefixList l1 • toMaxPrefixList l2) : MonoListRes Q A) := by
+            exact OFE.Equiv.of_eq (Auth.frag_op (F := Q)
+              (b1 := toMaxPrefixList l1) (b2 := toMaxPrefixList l2)).symm
+    _ ≡ (Auth.frag (toMaxPrefixList l2) : MonoListRes Q A) := OFE.NonExpansive.eqv (toMaxPrefixList_op_l (A := A) h)
+
+theorem monoListLbOpR {l1 l2 : List A} :
+    l1 <+: l2 → monoListLb (Q := Q) l2 • monoListLb l1 ≡ monoListLb l2 := by
+  intro h
+  unfold monoListLb
+  calc
+    ((Auth.frag (toMaxPrefixList l2) • Auth.frag (toMaxPrefixList l1)) : MonoListRes Q A)
+        ≡ (Auth.frag (toMaxPrefixList l2 • toMaxPrefixList l1) : MonoListRes Q A) := by
+            exact OFE.Equiv.of_eq (Auth.frag_op (F := Q)
+              (b1 := toMaxPrefixList l2) (b2 := toMaxPrefixList l1)).symm
+    _ ≡ (Auth.frag (toMaxPrefixList l2) : MonoListRes Q A) := OFE.NonExpansive.eqv (toMaxPrefixList_op_r (A := A) h)
+
+theorem monoListLbMono {l1 l2 : List A} :
+    l1 <+: l2 → monoListLb (Q := Q) l1 ≼ monoListLb (Q := Q) l2 := by
+  intro h
+  exact Auth.frag_inc_of_inc (toMaxPrefixList_mono (A := A) h)
+
+theorem monoListLbOpValidN (n : Nat) (l1 l2 : List A) :
+    ✓{n} (monoListLb (Q := Q) l1 • monoListLb l2) ↔
+      (∃ t, l2 ≡{n}≡ l1 ++ t) ∨ (∃ t, l1 ≡{n}≡ l2 ++ t) := by
+  unfold monoListLb
+  constructor
+  · intro h
+    have hEq : ✓{n} (Auth.frag (toMaxPrefixList l1 • toMaxPrefixList l2) : MonoListRes Q A) := by
+      exact (OFE.Equiv.of_eq (Auth.frag_op (F := Q)
+        (b1 := toMaxPrefixList l1) (b2 := toMaxPrefixList l2)).symm).dist.validN.mpr h
+    exact (Auth.frag_validN (F := Q) (b := toMaxPrefixList l1 • toMaxPrefixList l2)).1 hEq |>
+      (toMaxPrefixList_op_validN (A := A) n l1 l2).1
+  · intro h
+    have hEq : ✓{n} (toMaxPrefixList (A := A) l1 • toMaxPrefixList l2) := (toMaxPrefixList_op_validN (A := A) n l1 l2).2 h
+    exact (OFE.Equiv.of_eq (Auth.frag_op (F := Q)
+      (b1 := toMaxPrefixList l1) (b2 := toMaxPrefixList l2)).symm).dist.validN.mp <|
+      (Auth.frag_validN (F := Q) (b := toMaxPrefixList l1 • toMaxPrefixList l2)).2 hEq
+
+theorem monoListLbOpValid (l1 l2 : List A) :
+    ✓ (monoListLb (Q := Q) l1 • monoListLb l2) ↔
+      (∃ t, l2 ≡ l1 ++ t) ∨ (∃ t, l1 ≡ l2 ++ t) := by
+  unfold monoListLb
+  constructor
+  · intro h
+    have hEq : ✓ (Auth.frag (toMaxPrefixList l1 • toMaxPrefixList l2) : MonoListRes Q A) := by
+      exact CMRA.valid_of_eqv
+        (OFE.Equiv.of_eq (Auth.frag_op (F := Q)
+          (b1 := toMaxPrefixList l1) (b2 := toMaxPrefixList l2)).symm)
+        h
+    exact (Auth.frag_valid (F := Q) (b := toMaxPrefixList l1 • toMaxPrefixList l2)).1 hEq |>
+      (toMaxPrefixList_op_valid (A := A) l1 l2).1
+  · intro h
+    have hEq : ✓ (toMaxPrefixList (A := A) l1 • toMaxPrefixList l2) := (toMaxPrefixList_op_valid (A := A) l1 l2).2 h
+    exact CMRA.valid_of_eqv
+      (OFE.Equiv.of_eq (Auth.frag_op (F := Q)
+        (b1 := toMaxPrefixList l1) (b2 := toMaxPrefixList l2)).symm)
+      ((Auth.frag_valid (F := Q) (b := toMaxPrefixList l1 • toMaxPrefixList l2)).2 hEq)
+
+theorem monoListBothDfracValidN (n : Nat) (dq : DFrac Q) (l1 l2 : List A) :
+    ✓{n} (monoListAuth (Q := Q) dq l1 • monoListLb (Q := Q) l2) ↔
+      ✓ dq ∧ ∃ t, l1 ≡{n}≡ l2 ++ t := by
+  let a := toMaxPrefixList (A := A) l1
+  let b := toMaxPrefixList (A := A) l2
+  have hEq : monoListAuth (Q := Q) dq l1 • monoListLb (Q := Q) l2 ≡
+      (((Auth.auth dq a) • Auth.frag ((a • b : MaxPrefixList A)) : MonoListRes Q A)) := by
+    unfold monoListAuth monoListLb
+    have hAssoc : (((Auth.auth dq a) • Auth.frag a) • Auth.frag b : MonoListRes Q A) ≡
+        ((Auth.auth dq a) • (Auth.frag a • Auth.frag b) : MonoListRes Q A) := assoc.symm
+    have hFrag : ((Auth.auth dq a) • (Auth.frag a • Auth.frag b) : MonoListRes Q A) ≡
+        (((Auth.auth dq a) • Auth.frag ((a • b : MaxPrefixList A)) : MonoListRes Q A)) :=
+      (OFE.Equiv.of_eq (Auth.frag_op (F := Q) (b1 := a) (b2 := b)).symm).op_r
+    exact hAssoc.trans hFrag
+  constructor
+  · intro h
+    have h' : ✓{n} (((Auth.auth dq a) • Auth.frag ((a • b : MaxPrefixList A)) : MonoListRes Q A)) := hEq.dist.validN.mp h
+    have hBoth := (Auth.both_dfrac_validN (F := Q) (dq := dq) (a := a) (b := (a • b))).1 h'
+    have hvalidAB : ✓{n} (a • b) := CMRA.validN_of_incN hBoth.2.1 (toMaxPrefixList_validN (A := A) n l1)
+    rcases (toMaxPrefixList_op_validN (A := A) n l1 l2).1 hvalidAB with hleft | hright
+    · rcases hleft with ⟨t, ht⟩
+      have hp : l1 <+: l1 ++ t := ⟨t, rfl⟩
+      have hmap : b ≡{n}≡ toMaxPrefixList (A := A) (l1 ++ t) := toMaxPrefixList_ne.ne ht
+      have hop : a • toMaxPrefixList (A := A) (l1 ++ t) ≡{n}≡ toMaxPrefixList (A := A) (l1 ++ t) :=
+        (toMaxPrefixList_op_l (A := A) hp).dist
+      have hab_eq : a • b ≡{n}≡ b := (hmap.op_r).trans (hop.trans hmap.symm)
+      have hbinc : b ≼{n} a := (hab_eq.incN_l).1 hBoth.2.1
+      rcases (toMaxPrefixList_includedN (A := A) n l2 l1).1 hbinc with ⟨u, hu⟩
+      exact ⟨hBoth.1, ⟨u, hu⟩⟩
+    · exact ⟨hBoth.1, hright⟩
+  · rintro ⟨hdq, ⟨t, ht⟩⟩
+    have hmap : a ≡{n}≡ toMaxPrefixList (A := A) (l2 ++ t) := toMaxPrefixList_ne.ne ht
+    have hp : l2 <+: l2 ++ t := ⟨t, rfl⟩
+    have hop : toMaxPrefixList (A := A) (l2 ++ t) • b ≡{n}≡ toMaxPrefixList (A := A) (l2 ++ t) :=
+      (toMaxPrefixList_op_r (A := A) hp).dist
+    have hincl : a • b ≼{n} a := by
+      refine ⟨CMRA.unit, ?_⟩
+      calc
+        a ≡{n}≡ toMaxPrefixList (A := A) (l2 ++ t) := hmap
+        _ ≡{n}≡ toMaxPrefixList (A := A) (l2 ++ t) • b := hop.symm
+        _ ≡{n}≡ a • b := (hmap.op_l).symm
+        _ ≡{n}≡ (a • b) • CMRA.unit := (CMRA.unit_right_id_dist (a • b)).symm
+    have hBoth : ✓{n} (((Auth.auth dq a) • Auth.frag ((a • b : MaxPrefixList A)) : MonoListRes Q A)) :=
+      (Auth.both_dfrac_validN (F := Q) (dq := dq) (a := a) (b := (a • b))).2 ⟨hdq, hincl, toMaxPrefixList_validN (A := A) n l1⟩
+    exact hEq.dist.validN.mpr hBoth
+
+theorem monoListBothValidN (n : Nat) (l1 l2 : List A) :
+    ✓{n} (monoListAuth (Q := Q) (DFrac.own (1 : Q)) l1 • monoListLb (Q := Q) l2) ↔
+      ∃ t, l1 ≡{n}≡ l2 ++ t := by
+  rw [monoListBothDfracValidN]
+  constructor
+  · rintro ⟨_, ht⟩
+    exact ht
+  · intro ht
+    exact ⟨DFrac.valid_own_one, ht⟩
+
+theorem monoListBothDfracValid (dq : DFrac Q) (l1 l2 : List A) :
+    ✓ (monoListAuth (Q := Q) dq l1 • monoListLb (Q := Q) l2) ↔
+      ✓ dq ∧ ∃ t, l1 ≡ l2 ++ t := by
+  let a : MaxPrefixList A := toMaxPrefixList (A := A) l1
+  let b : MaxPrefixList A := toMaxPrefixList (A := A) l2
+  have hEq : monoListAuth (Q := Q) dq l1 • monoListLb (Q := Q) l2 ≡
+      ((Auth.auth (F := Q) dq a) • Auth.frag (a • b) : MonoListRes Q A) := by
+    unfold monoListAuth monoListLb
+    calc
+      (((Auth.auth (F := Q) dq a) • Auth.frag a) • Auth.frag b : MonoListRes Q A)
+          ≡ ((Auth.auth (F := Q) dq a) • (Auth.frag a • Auth.frag b) : MonoListRes Q A) := assoc.symm
+      _ ≡ ((Auth.auth (F := Q) dq a) • Auth.frag (a • b) : MonoListRes Q A) := by
+            exact (OFE.Equiv.of_eq (Auth.frag_op (F := Q) (b1 := a) (b2 := b)).symm).op_r
+  rw [CMRA.valid_iff hEq, Auth.both_dfrac_valid]
+  constructor
+  · rintro ⟨hdq, hinc, _⟩
+    refine ⟨hdq, ?_⟩
+    have hbincN : ∀ n, b ≼{n} a := fun n => CMRA.incN_trans (CMRA.incN_op_right n a b) (hinc n)
+    exact (toMaxPrefixList_included (A := A) l2 l1).1 <|
+      (maxPrefixList_included_includedN (A := A) b a).2 hbincN
+  · rintro ⟨hdq, hprefix⟩
+    refine ⟨hdq, ?_, toMaxPrefixList_valid (A := A) l1⟩
+    intro n
+    have hbinc : b ≼ a := (toMaxPrefixList_included (A := A) l2 l1).2 hprefix
+    have hab : a • b ≼ a := by
+      calc
+        a • b ≼ a • a := CMRA.op_mono_right a hbinc
+        _ ≡ a := CMRA.op_self a
+    exact CMRA.incN_of_inc n hab
+
+theorem monoListBothValid (l1 l2 : List A) :
+    ✓ (monoListAuth (Q := Q) (DFrac.own (1 : Q)) l1 • monoListLb (Q := Q) l2) ↔
+      ∃ t, l1 ≡ l2 ++ t := by
+  rw [monoListBothDfracValid]
+  constructor
+  · rintro ⟨_, ht⟩
+    exact ht
+  · intro ht
+    exact ⟨DFrac.valid_own_one, ht⟩
+
+theorem monoListBothDfracValid_L [Leibniz A] (dq : DFrac Q) (l1 l2 : List A) :
+    ✓ (monoListAuth (Q := Q) dq l1 • monoListLb (Q := Q) l2) ↔
+      ✓ dq ∧ l2 <+: l1 := by
+  rw [monoListBothDfracValid]
+  constructor
+  · rintro ⟨hdq, ⟨t, ht⟩⟩
+    exact ⟨hdq, ⟨t, Leibniz.eq_of_eqv ht.symm⟩⟩
+  · rintro ⟨hdq, ⟨t, rfl⟩⟩
+    exact ⟨hdq, ⟨t, Equiv.rfl⟩⟩
+
+theorem monoListBothValid_L [Leibniz A] (l1 l2 : List A) :
+    ✓ (monoListAuth (Q := Q) (DFrac.own (1 : Q)) l1 • monoListLb (Q := Q) l2) ↔
+      l2 <+: l1 := by
+  rw [monoListBothValid]
+  constructor
+  · rintro ⟨t, ht⟩
+    exact ⟨t, Leibniz.eq_of_eqv ht.symm⟩
+  · rintro ⟨t, rfl⟩
+    exact ⟨t, Equiv.rfl⟩
+
+theorem monoListLbOpValid_L [Leibniz A] (l1 l2 : List A) :
+    ✓ (monoListLb (Q := Q) l1 • monoListLb l2) ↔ l1 <+: l2 ∨ l2 <+: l1 := by
+  rw [monoListLbOpValid]
+  constructor
+  · rintro (⟨t, ht⟩ | ⟨t, ht⟩)
+    · exact Or.inl ⟨t, Leibniz.eq_of_eqv ht.symm⟩
+    · exact Or.inr ⟨t, Leibniz.eq_of_eqv ht.symm⟩
+  · rintro (⟨t, rfl⟩ | ⟨t, rfl⟩)
+    · exact Or.inl ⟨t, Equiv.rfl⟩
+    · exact Or.inr ⟨t, Equiv.rfl⟩
+
+theorem monoListLbOpValid_1_L [Leibniz A] (l1 l2 : List A) :
+    ✓ (monoListLb (Q := Q) l1 • monoListLb l2) → l1 <+: l2 ∨ l2 <+: l1 :=
+  (monoListLbOpValid_L (Q := Q) l1 l2).1
+
+theorem monoListLbOpValid_2_L [Leibniz A] (l1 l2 : List A) :
+    l1 <+: l2 ∨ l2 <+: l1 → ✓ (monoListLb (Q := Q) l1 • monoListLb l2) :=
+  (monoListLbOpValid_L (Q := Q) l1 l2).2
+
+theorem monoListAuthDfracOpValidN (n : Nat) (dq1 dq2 : DFrac Q) (l1 l2 : List A) :
+    ✓{n} (monoListAuth (Q := Q) dq1 l1 • monoListAuth dq2 l2) ↔
+      ✓ (dq1 • dq2) ∧ l1 ≡{n}≡ l2 := by
+  let a : MaxPrefixList A := toMaxPrefixList (A := A) l1
+  let b : MaxPrefixList A := toMaxPrefixList (A := A) l2
+  let x1 : MonoListRes Q A := Auth.auth (F := Q) dq1 a
+  let x2 : MonoListRes Q A := Auth.auth (F := Q) dq2 b
+  let f1 : MonoListRes Q A := Auth.frag a
+  let f2 : MonoListRes Q A := Auth.frag b
+  have hEq : ((x1 • f1) • (x2 • f2) : MonoListRes Q A) ≡ ((x1 • x2) • (f1 • f2) : MonoListRes Q A) := by
+    calc
+      ((x1 • f1) • (x2 • f2) : MonoListRes Q A) ≡ (((x1 • f1) • x2) • f2 : MonoListRes Q A) := assoc
+      _ ≡ (((x1 • x2) • f1) • f2 : MonoListRes Q A) := by
+            exact (calc
+              (((x1 • f1) • x2) : MonoListRes Q A) ≡ (x1 • (f1 • x2) : MonoListRes Q A) := assoc.symm
+              _ ≡ (x1 • (x2 • f1) : MonoListRes Q A) := by exact OFE.Equiv.op_r comm
+              _ ≡ (((x1 • x2) • f1) : MonoListRes Q A) := assoc).op_l
+      _ ≡ ((x1 • x2) • (f1 • f2) : MonoListRes Q A) := assoc.symm
+  change ✓{n} ((x1 • f1) • (x2 • f2) : MonoListRes Q A) ↔ ✓ (dq1 • dq2) ∧ l1 ≡{n}≡ l2
+  constructor
+  · intro h
+    have h' : ✓{n} (((x1 • x2) • (f1 • f2)) : MonoListRes Q A) := hEq.symm.dist.validN.mp h
+    have hxx : ✓{n} ((x1 • x2) : MonoListRes Q A) := CMRA.validN_op_left h'
+    obtain ⟨hdq, hab, _⟩ := (Auth.auth_dfrac_op_validN (F := Q) (a1 := a) (a2 := b)).1 hxx
+    exact ⟨hdq, toMaxPrefixList_dist_inj (A := A) hab⟩
+  · rintro ⟨hdq, hl⟩
+    have hab : a ≡{n}≡ b := toMaxPrefixList_ne.ne hl
+    have hxxeq : ((x1 • x2) : MonoListRes Q A) ≡{n}≡ (Auth.auth (F := Q) (dq1 • dq2) a : MonoListRes Q A) := by
+      calc
+        ((x1 • x2) : MonoListRes Q A) ≡{n}≡ ((Auth.auth (F := Q) dq1 a) • Auth.auth dq2 a : MonoListRes Q A) := by
+          exact (Auth.auth_ne (F := Q) (dq := dq2)).ne hab.symm |>.op_r
+        _ ≡{n}≡ (Auth.auth (F := Q) (dq1 • dq2) a : MonoListRes Q A) :=
+          (Auth.auth_dfrac_op (F := Q) (dq1 := dq1) (dq2 := dq2) (a := a)).dist.symm
+    have hffeq : ((f1 • f2) : MonoListRes Q A) ≡{n}≡ (f1 : MonoListRes Q A) := by
+      calc
+        ((f1 • f2) : MonoListRes Q A) ≡{n}≡ ((f1 • f1) : MonoListRes Q A) := by
+          exact (Auth.frag_ne (F := Q)).ne hab.symm |>.op_r
+        _ ≡{n}≡ (f1 : MonoListRes Q A) := (CMRA.op_self f1).dist
+    have hmono :
+        ((x1 • x2) • (f1 • f2) : MonoListRes Q A) ≡{n}≡
+          ((Auth.auth (F := Q) (dq1 • dq2) a) • f1 : MonoListRes Q A) :=
+      hxxeq.op hffeq
+    have hvalid : ✓{n} (((Auth.auth (F := Q) (dq1 • dq2) a) • f1) : MonoListRes Q A) := by
+      change ✓{n} (monoListAuth (Q := Q) (dq1 • dq2) l1)
+      rw [monoListAuthDfracValidN]
+      exact hdq
+    exact hEq.dist.validN.mpr <| hmono.validN.mpr hvalid
+
+theorem monoListAuthOpValidN (n : Nat) (l1 l2 : List A) :
+    ✓{n} (monoListAuth (Q := Q) (DFrac.own (1 : Q)) l1 • monoListAuth (DFrac.own (1 : Q)) l2) ↔ False := by
+  rw [monoListAuthDfracOpValidN]
+  constructor
+  · rintro ⟨hdq, _⟩
+    exact (UFraction.one_whole (α := Q)).2 <| DFrac.valid_own_op (dq := DFrac.own (1 : Q)) (q := (1 : Q)) hdq
+  · intro h
+    exact False.elim h
+
+theorem monoListAuthDfracOpValid (dq1 dq2 : DFrac Q) (l1 l2 : List A) :
+    ✓ (monoListAuth (Q := Q) dq1 l1 • monoListAuth dq2 l2) ↔
+      ✓ (dq1 • dq2) ∧ l1 ≡ l2 := by
+  rw [CMRA.valid_iff_validN]
+  constructor
+  · intro h
+    refine ⟨((monoListAuthDfracOpValidN (Q := Q) 0 dq1 dq2 l1 l2).1 (h 0)).1, ?_⟩
+    exact OFE.equiv_dist.2 fun n => ((monoListAuthDfracOpValidN (Q := Q) n dq1 dq2 l1 l2).1 (h n)).2
+  · rintro ⟨hdq, hl⟩ n
+    exact (monoListAuthDfracOpValidN (Q := Q) n dq1 dq2 l1 l2).2 ⟨hdq, hl.dist⟩
+
+theorem monoListAuthOpValid (l1 l2 : List A) :
+    ✓ (monoListAuth (Q := Q) (DFrac.own (1 : Q)) l1 • monoListAuth (DFrac.own (1 : Q)) l2) ↔ False := by
+  rw [CMRA.valid_iff_validN]
+  constructor
+  · intro h
+    exact (monoListAuthOpValidN (Q := Q) 0 l1 l2).1 (h 0)
+  · intro h n
+    exact False.elim h
+
+theorem monoListAuthDfracOpValid_L [Leibniz A] (dq1 dq2 : DFrac Q) (l1 l2 : List A) :
+    ✓ (monoListAuth (Q := Q) dq1 l1 • monoListAuth dq2 l2) ↔
+      ✓ (dq1 • dq2) ∧ l1 = l2 := by
+  rw [monoListAuthDfracOpValid]
+  simp
+
+theorem monoListAuthOpValid_L [Leibniz A] (l1 l2 : List A) :
+    ✓ (monoListAuth (Q := Q) (DFrac.own (1 : Q)) l1 • monoListAuth (DFrac.own (1 : Q)) l2) ↔ False := by
+  exact monoListAuthOpValid (Q := Q) l1 l2
+
+theorem monoListIncluded (dq : DFrac Q) (l : List A) :
+    monoListLb (Q := Q) l ≼ monoListAuth (Q := Q) dq l := by
+  unfold monoListLb monoListAuth
+  exact ⟨Auth.auth dq (toMaxPrefixList l), comm⟩
+
+theorem monoListUpdate {l1 l2 : List A} :
+    l1 <+: l2 →
+      monoListAuth (Q := Q) (DFrac.own (1 : Q)) l1 ~~>
+        monoListAuth (DFrac.own (1 : Q)) l2 := by
+  intro h
+  unfold monoListAuth
+  exact Auth.auth_update (maxPrefixList_localUpdate (A := A) h)
+
+theorem monoListAuthPersist (dq : DFrac Q) (l : List A) :
+    monoListAuth (Q := Q) dq l ~~> monoListAuth DFrac.discard l := by
+  unfold monoListAuth
+  exact Update.op (Auth.auth_update_auth_persist (F := Q) (dq := dq) (a := toMaxPrefixList l)) Update.id
+
+theorem monoListAuthUnpersist [IsSplitFraction Q] (l : List A) :
+    monoListAuth (Q := Q) DFrac.discard l ~~>:
+      fun k => ∃ q, k = monoListAuth (Q := Q) (DFrac.own q) l := by
+  unfold monoListAuth
+  simpa using (Auth.auth_updateP_both_unpersist (F := Q)
+    (a := toMaxPrefixList l) (b := toMaxPrefixList l))
+
+abbrev MonoListURF (T : COFE.OFunctorPre) [RFunctor T] : COFE.OFunctorPre :=
+  AuthURF (F := Q) (MaxPrefixListURF T)
+
+instance {T} [RFunctor T] : URFunctor (MonoListURF (Q := Q) T) := by
+  simpa [MonoListURF] using (inferInstance : URFunctor (AuthURF (F := Q) (MaxPrefixListURF T)))
+
+instance {T} [RFunctorContractive T] : URFunctorContractive (MonoListURF (Q := Q) T) := by
+  simpa [MonoListURF] using
+    (inferInstance : URFunctorContractive (AuthURF (F := Q) (MaxPrefixListURF T)))
+
+abbrev MonoListRF (T : COFE.OFunctorPre) [RFunctor T] : COFE.OFunctorPre :=
+  AuthRF (F := Q) (MaxPrefixListURF T)
+
+instance {T} [RFunctor T] : RFunctor (MonoListRF (Q := Q) T) := by
+  simpa [MonoListRF] using (inferInstance : RFunctor (AuthRF (F := Q) (MaxPrefixListURF T)))
+
+instance {T} [RFunctorContractive T] : RFunctorContractive (MonoListRF (Q := Q) T) := by
+  simpa [MonoListRF] using
+    (inferInstance : RFunctorContractive (AuthRF (F := Q) (MaxPrefixListURF T)))
+
+end MonoList
+
+end Iris
diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index 95af9ff2..fe11d0cc 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -307,6 +307,37 @@ instance Option.merge_ne [OFE α] {op : α → α → α} [NonExpansive₂ op] :
     rcases x1, x2, y1, y2 with ⟨_|_, _|_, _|_, _|_⟩ <;> simp_all
     exact NonExpansive₂.ne Hx Hy
 
+instance [OFE α] : OFE (List α) where
+  Equiv xs ys := ∀ i : Nat, xs[i]? ≡ ys[i]?
+  Dist n xs ys := ∀ i : Nat, xs[i]? ≡{n}≡ ys[i]?
+  dist_eqv := {
+    refl := by intro xs i; exact Dist.rfl
+    symm := by intro xs ys h i; exact Dist.symm (h i)
+    trans := by intro xs ys zs h1 h2 i; exact Dist.trans (h1 i) (h2 i)
+  }
+  equiv_dist := by
+    refine ⟨?_, ?_⟩
+    · intro h n i
+      exact (h i).dist
+    · intro h i
+      exact OFE.equiv_dist.2 fun n => h n i
+  dist_lt := fun h hm i => Dist.lt (h i) hm
+
+instance [OFE α] [OFE.Discrete α] : OFE.Discrete (List α) where
+  discrete_0 h := by
+    intro i
+    exact OFE.Discrete.discrete_0 (h (i : Nat))
+
+instance [OFE α] [Leibniz α] : Leibniz (List α) where
+  eq_of_eqv h := by
+    apply List.ext_getElem?
+    intro i
+    exact OFE.Leibniz.eq_of_eqv (α := Option α) (h (i : Nat))
+
+theorem List.equiv_getElem? [OFE α] {xs ys : List α} : xs ≡ ys ↔ ∀ i : Nat, xs[i]? ≡ ys[i]? := .rfl
+
+theorem List.dist_getElem? [OFE α] {xs ys : List α} : xs ≡{n}≡ ys ↔ ∀ i : Nat, xs[i]? ≡{n}≡ ys[i]? := .rfl
+
 abbrev OFEFun {α : Type _} (β : α → Type _) := ∀ a, OFE (β a)
 
 instance [OFEFun (β : α → _)] : OFE ((x : α) → β x) where