diff --git a/src/Iris/Algebra/Agree.lean b/src/Iris/Algebra/Agree.lean
index 409f620a..21c3f51b 100644
--- a/src/Iris/Algebra/Agree.lean
+++ b/src/Iris/Algebra/Agree.lean
@@ -19,6 +19,8 @@ structure Agree where
   car : List α
   not_nil : car ≠ []
 
+attribute [simp] Agree.not_nil
+
 def toAgree (a : α) : Agree α := ⟨[a], by simp⟩
 
 theorem mem_of_agree (x : Agree α) : ∃ a, a ∈ x.car := by
@@ -34,28 +36,25 @@ def Agree.dist (n : Nat) (x y : Agree α) : Prop :=
   (∀ b ∈ y.car, ∃ a ∈ x.car, a ≡{n}≡ b)
 
 theorem Agree.dist_equiv : Equivalence (dist (α := α) n) where
-  refl := by
-    rintro ⟨x, h⟩; constructor
-    · rintro a ha; exists a
-    · rintro b hb; exists b
-  symm := by
-    rintro  _ _ ⟨h₁, h₂⟩
-    simp only [dist] at h₁ h₂ ⊢
+  refl := fun ⟨x, h⟩ => by
+    constructor
+    · intro a ha; exists a
+    · intro b hb; exists b
+  symm := fun ⟨h₁, h₂⟩ => by
     constructor
-    · rintro a ha
+    · intro a ha
       obtain ⟨b, hb, hd⟩ := h₂ a ha
       exact ⟨b, hb, hd.symm⟩
-    · rintro b hb
+    · intro b hb
       obtain ⟨a, ha, hd⟩ := h₁ b hb
       exact ⟨a, ha, hd.symm⟩
-  trans := by
-    rintro _ _ _ ⟨h₁, h₁'⟩ ⟨h₂, h₂'⟩
+  trans := fun ⟨h₁, h₁'⟩ ⟨h₂, h₂'⟩ => by
     constructor
-    · rintro a ha
+    · intro a ha
       obtain ⟨b, hb, hd₁⟩ := h₁ a ha
       obtain ⟨c, hc, hd₂⟩ := h₂ b hb
       exact ⟨c, hc,  hd₁.trans hd₂⟩
-    · rintro c hc
+    · intro c hc
       obtain ⟨b, hb, hd₁⟩ := h₂' c hc
       obtain ⟨a, ha, hd₂⟩ := h₁' b hb
       exact ⟨a, ha,  hd₂.trans hd₁⟩
@@ -65,22 +64,24 @@ instance : OFE (Agree α) where
   Dist := Agree.dist
   dist_eqv := Agree.dist_equiv
   equiv_dist := by simp
-  dist_lt {n x y m} hn hlt := by
-    rcases hn with ⟨h₁, h₂⟩; constructor
-    · rintro a ha
+  dist_lt {n x y m} := fun ⟨h₁, h₂⟩ hlt => by
+    constructor
+    · intro a ha
       obtain ⟨b, hb, hd⟩ := h₁ a ha
       exact ⟨b, hb, OFE.Dist.lt hd hlt⟩
-    · rintro b hb
+    · intro b hb
       obtain ⟨a, ha, hd⟩ := h₂ b hb
       exact ⟨a, ha, OFE.Dist.lt hd hlt⟩
 
+theorem Agree.equiv_def {x y : Agree α} : x ≡ y ↔ ∀ n, Agree.dist n x y := .rfl
+theorem Agree.dist_def {x y : Agree α} : x ≡{n}≡ y ↔ Agree.dist n x y := .rfl
 
 def Agree.validN (n : Nat) (x : Agree α) : Prop :=
   match x.car with
   | [_] => True
   | _ => ∀ a ∈ x.car, ∀ b ∈ x.car, a ≡{n}≡ b
 
-theorem Agree.validN_def {x : Agree α} :
+theorem Agree.validN_iff {x : Agree α} :
     x.validN n ↔ ∀ a ∈ x.car, ∀ b ∈ x.car, a ≡{n}≡ b := by
   rcases x with ⟨⟨⟩ | ⟨a, ⟨⟩| _⟩, _⟩ <;> simp_all [validN, OFE.Dist.rfl]
 
@@ -90,20 +91,20 @@ def Agree.op (x y : Agree α) : Agree α :=
   ⟨x.car ++ y.car, by apply List.append_ne_nil_of_left_ne_nil; exact x.not_nil⟩
 
 theorem Agree.op_comm {x y : Agree α} :  x.op y ≡ y.op x := by
-  rintro n; simp_all only [dist, op, List.mem_append]
+  intro n; simp_all only [dist, op, List.mem_append]
   constructor <;> exact fun _ ha => ⟨_, ha.symm, .rfl⟩
 
 theorem Agree.op_commN {x y : Agree α} :  x.op y ≡{n}≡ y.op x := op_comm n
 
 theorem Agree.op_assoc {x y z : Agree α} :  x.op (y.op z) ≡ (x.op y).op z := by
-  rintro n; simp_all only [dist, op, List.mem_append, List.append_assoc]
+  intro n; simp_all only [dist, op, List.mem_append, List.append_assoc]
   constructor <;> (intro a ha; exists a)
 
 theorem Agree.idemp {x : Agree α} : x.op x ≡ x := by
-  rintro n; constructor <;> (intro a ha; exists a; simp_all [op])
+  intro n; constructor <;> (intro a ha; exists a; simp_all [op])
 
 theorem Agree.validN_ne {x y : Agree α} : x ≡{n}≡ y → x.validN n → y.validN n := by
-  simp only [OFE.Dist, dist, validN_def, and_imp]
+  simp only [OFE.Dist, dist, validN_iff, and_imp]
   intro h₁ h₂ hn a ha b hb
   have ⟨a', ha', ha'a⟩ := h₂ _ ha
   have ⟨b', hb', hb'b⟩ := h₂ _ hb
@@ -129,7 +130,7 @@ theorem Agree.op_ne₂ : OFE.NonExpansive₂ (Agree.op (α := α)) := by
   exact op_ne.ne hy |>.trans (op_comm n) |>.trans (op_ne.ne hx) |>.trans (op_comm n)
 
 theorem Agree.op_invN {x y : Agree α} : (x.op y).validN n → x ≡{n}≡ y := by
-  simp only [op, validN_def, List.mem_append, OFE.Dist, dist]
+  simp only [op, validN_iff, List.mem_append, OFE.Dist, dist]
   intro h; constructor
   · intro a ha
     obtain ⟨b, hb⟩ := mem_of_agree y
@@ -138,6 +139,11 @@ theorem Agree.op_invN {x y : Agree α} : (x.op y).validN n → x ≡{n}≡ y :=
     obtain ⟨b, hb⟩ := mem_of_agree x
     exists b; simp_all
 
+theorem Agree.op_inv {x y : Agree α} : (x.op y).valid → x ≡ y := by
+  simp [valid, equiv_def]
+  intro h n
+  exact op_invN (h n)
+
 instance : CMRA (Agree α) where
   pcore := some
   op := Agree.op
@@ -150,7 +156,7 @@ instance : CMRA (Agree α) where
 
   valid_iff_validN := by rfl
   validN_succ := by
-    simp [Agree.validN_def]; intro x n hsuc a ha b hb
+    simp [Agree.validN_iff]; intro x n hsuc a ha b hb
     exact (OFE.dist_lt (hsuc a ha b hb) (by omega))
 
   assoc := Agree.op_assoc
@@ -160,26 +166,192 @@ instance : CMRA (Agree α) where
   pcore_op_mono := by simp only [Option.some.injEq]; rintro x _ rfl y; exists y
   validN_op_left := by
     intro n x y
-    simp only [Agree.op, Agree.validN_def, List.mem_append]
-    intro h a ha b hb
-    exact h _ (.inl ha) _ (.inl hb)
-
+    simp only [Agree.op, Agree.validN_iff, List.mem_append]
+    exact fun h a ha b hb => h _ (.inl ha) _ (.inl hb)
   extend := by
     intro n x y₁ y₂ hval heq₁
-    exists x, x
     have heq₂ := Agree.op_invN (Agree.validN_ne heq₁ hval)
     have heq₃ : y₁.op y₂ ≡{n}≡ y₁ := Agree.op_ne.ne heq₂.symm |>.trans (Agree.idemp n)
-    exact ⟨Agree.idemp.symm, heq₁.trans heq₃, heq₁.trans heq₃ |>.trans heq₂⟩
+    exact ⟨x, x, Agree.idemp.symm, heq₁.trans heq₃, heq₁.trans heq₃ |>.trans heq₂⟩
+
+theorem Agree.op_def {x y : Agree α} : x • y = x.op y := rfl
+theorem Agree.validN_def {x : Agree α} : ✓{n} x ↔ x.validN n := .rfl
+theorem Agree.valid_def {x : Agree α} : ✓ x ↔ x.valid := .rfl
+
+instance : CMRA.IsTotal (Agree α) where
+  total x := ⟨x, rfl⟩
+
+instance [OFE.Discrete α] : CMRA.Discrete (Agree α) where
+  discrete_0 := by
+    intro x y ⟨h₁, h₂⟩ n
+    constructor <;> intro a ha
+    · obtain ⟨b, hb, heq⟩ := h₁ a ha
+      exists b; simp_all [OFE.Discrete.discrete_n]
+    · obtain ⟨b, hb, heq⟩ := h₂ a ha
+      exists b; simp_all [OFE.Discrete.discrete_n]
+  discrete_valid {x} hval n := by
+    rw [Agree.validN_def] at hval
+    rw [Agree.validN_iff] at hval ⊢
+    exact fun a ha b hb => OFE.discrete_n (hval a ha b hb)
+
+instance : OFE.NonExpansive (@toAgree α) where
+  ne n x₁ x₂ heq := by constructor <;> simp_all [toAgree]
+
+theorem Agree.toAgree_injN {a b : α} : toAgree a ≡{n}≡ toAgree b → a ≡{n}≡ b := by
+  intro ⟨h₁, h₂⟩; simp_all [toAgree]
+
+theorem Agree.toAgree_inj {a b : α} : toAgree a ≡ toAgree b → a ≡ b := by
+  simp only [OFE.equiv_dist]
+  exact fun heq n => toAgree_injN (heq n)
+
+theorem Agree.toAgree_uninjN {x : Agree α} : ✓{n} x → ∃ a, toAgree a ≡{n}≡ x := by
+  rw [validN_def, validN_iff]
+  obtain ⟨a, ha⟩ := mem_of_agree x
+  intro h; exists a
+  constructor <;> intros
+  · exists a; simp_all [toAgree]
+  · simp_all [toAgree]
+
+theorem Agree.toAgree_uninj {x : Agree α} : ✓ x → ∃ a, toAgree a ≡ x := by
+  simp only [valid_def, valid, validN_iff, equiv_def]
+  obtain ⟨a, ha⟩ := mem_of_agree x
+  intro h; exists a; intro n
+  constructor <;> intros
+  · exists a; simp_all [toAgree]
+  · simp_all [toAgree]
 
 theorem Agree.includedN {x y : Agree α} : x ≼{n} y ↔ y ≡{n}≡ y • x := by
   refine ⟨fun ⟨z, h⟩ => ?_, fun h => ⟨y, h.trans op_commN⟩⟩
   have hid := idemp (x := x) |>.symm
-  exact h.trans <| op_commN.trans <|
-    (op_ne.ne (hid n)).trans <|
-    .trans (op_assoc n) <|
-    op_commN.trans <|
-    (op_ne.ne (h.trans op_commN).symm).trans <|
-    op_commN
+  calc
+    y ≡{n}≡ x • z := h
+    _ ≡{n}≡ (x • x) • z := .op_l (hid n)
+    _ ≡{n}≡ x • (x • z) := CMRA.op_assocN.symm
+    _ ≡{n}≡ x • y := h.symm.op_r
+    _ ≡{n}≡ y • x := op_commN
 
 theorem Agree.included {x y : Agree α} : x ≼ y ↔ y ≡ y • x :=
   ⟨fun ⟨z, h⟩ n => includedN.mp ⟨z, h n⟩, fun h => ⟨y, h.trans op_comm⟩⟩
+
+theorem Agree.valid_includedN {x y : Agree α} : ✓{n} y → x ≼{n} y → x ≡{n}≡ y := by
+  intro hval ⟨z, heq⟩
+  have : ✓{n} (x • z) := heq.validN.mp hval
+  calc
+    x ≡{n}≡ x • x := .symm (idemp _)
+    _ ≡{n}≡ x • z := (op_invN this).op_r
+    _ ≡{n}≡ y := heq.symm
+
+theorem Agree.valid_included {x y : Agree α} : ✓ y → x ≼ y → x ≡ y := by
+  intro hval ⟨z, heq⟩
+  have heq' : x ≡ z := op_inv <| (CMRA.valid_iff heq).mp hval
+  calc
+    x ≡ x • x := idemp.symm
+    _ ≡ x • z := .op_r heq'
+    _ ≡ y := heq.symm
+
+@[simp]
+theorem Agree.toAgree_includedN {a b : α} : toAgree a ≼{n} toAgree b ↔ a ≡{n}≡ b := by
+  constructor <;> intro h
+  · exact toAgree_injN (valid_includedN trivial h)
+  · exists toAgree a
+    calc
+      toAgree b ≡{n}≡ toAgree a := OFE.NonExpansive.ne h.symm
+      _         ≡{n}≡ toAgree a • toAgree a := .symm (idemp n)
+
+@[simp]
+theorem Agree.toAgree_included {a b : α} : toAgree a ≼ toAgree b ↔ a ≡ b := by
+  constructor <;> intro h
+  · exact toAgree_inj (valid_included (fun _ => trivial) h)
+  · exists toAgree a
+    calc
+      toAgree b ≡ toAgree a := OFE.NonExpansive.eqv (OFE.Equiv.symm h)
+      _         ≡ toAgree a • toAgree a := .symm (CMRA.pcore_op_left rfl)
+
+@[simp]
+theorem Agree.toAgree_included_L [OFE.Leibniz α] {a b : α} :
+    toAgree a ≼ toAgree b ↔ a = b := by simp
+
+instance {x : Agree α} : CMRA.Cancelable x where
+  cancelableN {n y z} hval heq := by
+    obtain ⟨a, ha⟩ := Agree.toAgree_uninjN (CMRA.validN_op_left hval)
+    obtain ⟨b, hb⟩ := Agree.toAgree_uninjN (CMRA.validN_op_right hval)
+    have hval' : ✓{n} x • z := (OFE.Dist.validN heq).mp hval
+    have : ✓{n} z := CMRA.validN_op_right hval'
+    obtain ⟨c, hc⟩ := Agree.toAgree_uninjN this
+    have heq₁ : a ≡{n}≡ b := Agree.toAgree_injN <| calc
+      toAgree a ≡{n}≡ x         := ha
+      _         ≡{n}≡ y         := Agree.op_invN hval
+      _         ≡{n}≡ toAgree b := hb.symm
+    have heq₂ : a ≡{n}≡ c := Agree.toAgree_injN <| calc
+      toAgree a ≡{n}≡ x         := ha
+      _         ≡{n}≡ z         := Agree.op_invN hval'
+      _         ≡{n}≡ toAgree c := hc.symm
+    have heq₃ : b ≡{n}≡ c := heq₁.symm.trans heq₂
+    calc
+      y ≡{n}≡ toAgree b := hb.symm
+      _ ≡{n}≡ toAgree c := OFE.NonExpansive.ne heq₃
+      _ ≡{n}≡ z := hc
+
+theorem Agree.toAgree_op_validN_iff_dist {a b : α} :
+    ✓{n} (toAgree a • toAgree b) ↔ a ≡{n}≡ b := by
+  constructor <;> intro h
+  · exact toAgree_injN (op_invN h)
+  · have : toAgree a ≡{n}≡ toAgree b := OFE.NonExpansive.ne h
+    have : toAgree a • toAgree b ≡{n}≡ toAgree a := calc
+      toAgree a • toAgree b ≡{n}≡ toAgree a • toAgree a := this.symm.op_r
+      _ ≡{n}≡ toAgree a := idemp n
+    exact this.symm.validN.mp trivial
+
+theorem Agree.toAgree_op_valid_iff_equiv {a : α} : ✓ (toAgree a • toAgree b) ↔ a ≡ b := by
+  simp [OFE.equiv_dist, CMRA.valid_iff_validN, toAgree_op_validN_iff_dist]
+
+theorem toAgree_op_valid_iff_eq [OFE.Leibniz α] {a : α} :
+    ✓ (toAgree a • toAgree b) ↔ a = b := by simp_all [Agree.toAgree_op_valid_iff_equiv]
+
+end agree
+
+def Agree.map' {α β} (f : α → β) (a : Agree α) : Agree β := ⟨a.car.map f, by simp⟩
+
+section agree_map
+
+variable {α β} [OFE α] [OFE β] {f : α → β} [hne : OFE.NonExpansive f]
+
+local instance : OFE.NonExpansive (Agree.map' f) where
+  ne := by
+    intro n x₁ x₂ h
+    simp only [Agree.map', Agree.dist_def, Agree.dist, List.mem_map, forall_exists_index, and_imp,
+      forall_apply_eq_imp_iff₂]  at h ⊢
+    constructor
+    · intro a ha
+      obtain ⟨b, hb, heq⟩ := h.1 a ha
+      exact ⟨f b, ⟨b, hb, rfl⟩, OFE.NonExpansive.ne heq⟩
+    · intro a ha
+      obtain ⟨b, hb, heq⟩ := h.2 a ha
+      exact ⟨f b, ⟨b, hb, rfl⟩, OFE.NonExpansive.ne heq⟩
+
+variable (f) in
+def Agree.map : CMRA.Hom (Agree α) (Agree β) where
+  f := map' f
+  ne := inferInstance
+  validN {n x} hval := by
+    simp [validN_def, map', validN_iff] at hval ⊢
+    intro a ha b hb
+    exact OFE.NonExpansive.ne (hval a ha b hb)
+  pcore x := .rfl
+  op x y n := by
+    simp only [dist, map', op_def, op, List.map_append, List.mem_append, List.mem_map]
+    constructor <;>
+    · intro a ha
+      obtain ⟨b, hb, rfl⟩ | ⟨b, hb, rfl⟩ := ha
+      · exact ⟨f b, .inl ⟨_, hb, rfl⟩, .rfl⟩
+      · exact ⟨f b, .inr ⟨_, hb, rfl⟩, .rfl⟩
+
+theorem Agree.agree_map_ext {g : α → β} [OFE.NonExpansive g] (heq : ∀ a, f a ≡ g a) :
+    map f x ≡ map g x := by
+  intro n
+  simp only [dist, map, map', List.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
+  constructor <;> intro a ha
+  · exact ⟨g a, ⟨a, ha, rfl⟩, (heq a).dist⟩
+  · exact ⟨f a, ⟨a, ha, rfl⟩, (heq a).dist⟩
+
+end agree_map
diff --git a/src/Iris/Algebra/CMRA.lean b/src/Iris/Algebra/CMRA.lean
index 6d7070b7..bea9335e 100644
--- a/src/Iris/Algebra/CMRA.lean
+++ b/src/Iris/Algebra/CMRA.lean
@@ -552,10 +552,10 @@ theorem valid_0_iff_validN [Discrete α] (n) {x : α} : ✓{0} x ↔ ✓{n} x :=
   ⟨Valid.validN ∘ discrete_valid, validN_of_le (Nat.zero_le n)⟩
 
 theorem inc_iff_incN [OFE.Discrete α] (n) {x y : α} : x ≼ y ↔ x ≼{n} y :=
-  ⟨incN_of_inc _, fun ⟨z, hz⟩ => ⟨z, discrete_n hz⟩⟩
+  ⟨incN_of_inc _, fun ⟨z, hz⟩ => ⟨z, discrete hz⟩⟩
 
 theorem inc_0_iff_incN [OFE.Discrete α] (n) {x y : α} : x ≼{0} y ↔ x ≼{n} y :=
-  ⟨fun ⟨z, hz⟩ => ⟨z, (discrete_n hz).dist⟩,
+  ⟨fun ⟨z, hz⟩ => ⟨z, (discrete hz).dist⟩,
    fun a => incN_of_incN_le (Nat.zero_le n) a⟩
 
 end discreteCMRA
@@ -570,7 +570,7 @@ theorem cancelable {x y z : α} [Cancelable x] (v : ✓(x • y)) (e : x • y 
 
 theorem discrete_cancelable {x : α} [Discrete α]
     (H : ∀ {y z : α}, ✓(x • y) → x • y ≡ x • z → y ≡ z) : Cancelable x where
-  cancelableN {n} {_ _} v e := (H ((valid_iff_validN' n).mpr v) (Discrete.discrete_n e)).dist
+  cancelableN {n} {_ _} v e := (H ((valid_iff_validN' n).mpr v) (Discrete.discrete e)).dist
 
 instance cancelable_op {x y : α} [Cancelable x] [Cancelable y] : Cancelable (x • y) where
   cancelableN {n w _} v e :=
diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index 41230250..9bd6b029 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -140,8 +140,13 @@ class Discrete (α : Type _) [OFE α] where
 export OFE.Discrete (discrete_0)
 
 /-- For discrete OFEs, `n`-equivalence implies equivalence for any `n`. -/
-theorem Discrete.discrete_n [OFE α] [Discrete α] {n} {x y : α} (h : x ≡{n}≡ y) : x ≡ y :=
-  discrete_0 (OFE.Dist.le h (Nat.zero_le _))
+theorem Discrete.discrete [OFE α] [Discrete α] {n} {x y : α} (h : x ≡{n}≡ y) : x ≡ y :=
+  discrete_0 (h.le (Nat.zero_le _))
+export OFE.Discrete (discrete)
+
+/-- For discrete OFEs, `n`-equivalence implies equivalence for any `n`. -/
+theorem Discrete.discrete_n [OFE α] [Discrete α] {n} {x y : α} (h : x ≡{0}≡ y) : x ≡{n}≡ y :=
+  (discrete h).dist
 export OFE.Discrete (discrete_n)
 
 class Leibniz (α : Type _) [OFE α] where