diff --git a/src/Iris/Algebra.lean b/src/Iris/Algebra.lean
index 2fc931d7..d47a5f5b 100644
--- a/src/Iris/Algebra.lean
+++ b/src/Iris/Algebra.lean
@@ -3,3 +3,4 @@ import Iris.Algebra.CMRA
 import Iris.Algebra.COFESolver
 import Iris.Algebra.OFE
 import Iris.Algebra.Frac
+import Iris.Algebra.View
diff --git a/src/Iris/Algebra/Agree.lean b/src/Iris/Algebra/Agree.lean
index 21c3f51b..dc53683a 100644
--- a/src/Iris/Algebra/Agree.lean
+++ b/src/Iris/Algebra/Agree.lean
@@ -233,6 +233,41 @@ theorem Agree.includedN {x y : Agree α} : x ≼{n} y ↔ y ≡{n}≡ y • x :=
 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.toAgree.is_discrete {a : α} (Ha : OFE.DiscreteE a) : OFE.DiscreteE (toAgree a) := by
+  refine ⟨fun ⟨Hal, Har⟩ _ => ?_⟩
+  constructor <;> simp_all [toAgree]
+  · rcases Hal with ⟨b, Hb1, Hb2⟩
+    exact ⟨b, ⟨Hb1, Ha.discrete (Har b Hb1) |>.dist⟩⟩
+  · intro H Hb
+    exact Ha.discrete (Har H Hb) |>.dist
+
+open OFE OFE.Discrete in
+instance [OFE α] [Discrete α] : Discrete (Agree α) where
+  discrete_0 {x y} H := by
+    refine fun n => ⟨fun a Ha => ?_, fun b Hb => ?_⟩
+    · rcases H.1 a Ha with ⟨c, Hc⟩
+      refine ⟨c, ⟨Hc.1, ?_⟩⟩
+      apply equiv_dist.mp <| discrete_0 (Hc.2.le <| Nat.zero_le 0)
+    · rcases H.2 b Hb with ⟨c, Hc⟩
+      refine ⟨c, ⟨Hc.1, ?_⟩⟩
+      apply equiv_dist.mp <| discrete_0 (Hc.2.le <| Nat.zero_le 0)
+
+instance toAgree.ne [OFE α] : OFE.NonExpansive (toAgree : α → Agree α) where
+  ne n x y H := by
+    refine ⟨?_, ?_⟩
+    · intro a Ha; exists y; revert Ha
+      simp [toAgree]; exact (·▸H)
+    · intro b Hb; exists x; revert Hb
+      simp [toAgree]; exact (·▸H)
+
+theorem toAgree.inj {a1 a2 : α} {n} (H : toAgree a1 ≡{n}≡ toAgree a2) : a1 ≡{n}≡ a2 := by
+  have Hinc : a1 ∈ (toAgree a1).car := by simp [toAgree]
+  rcases H.1 a1 Hinc with ⟨_, ⟨_, _⟩⟩
+  simp_all [toAgree]
+
+instance : CMRA.IsTotal (Agree α) where
+  total := by simp [CMRA.pcore]
+
 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
@@ -354,4 +389,9 @@ theorem Agree.agree_map_ext {g : α → β} [OFE.NonExpansive g] (heq : ∀ a, f
   · exact ⟨g a, ⟨a, ha, rfl⟩, (heq a).dist⟩
   · exact ⟨f a, ⟨a, ha, rfl⟩, (heq a).dist⟩
 
+theorem toAgree.incN {a b : α} {n} : toAgree a ≼{n} toAgree b ↔ a ≡{n}≡ b := by
+  refine ⟨?_, fun H => (CMRA.incN_iff_right <| toAgree.ne.ne H).mp <| CMRA.incN_refl _⟩
+  intro H
+  apply toAgree.inj
+  exact Agree.valid_includedN trivial H
 end agree_map
diff --git a/src/Iris/Algebra/CMRA.lean b/src/Iris/Algebra/CMRA.lean
index c7620a80..dd726f91 100644
--- a/src/Iris/Algebra/CMRA.lean
+++ b/src/Iris/Algebra/CMRA.lean
@@ -224,7 +224,7 @@ theorem valid_opM {x : α} {my : Option α} : ✓ (x •? my) → ✓ x :=
   match my with
   | none => id  | some _ => valid_op_left
 
-theorem validN_op_opM_left {mz : Option α} : ✓{n} (x • y) •? mz → ✓{n} x •? mz :=
+theorem validN_op_opM_left {mz : Option α} : ✓{n} (x • y : α) •? mz → ✓{n} x •? mz :=
   match mz with
   | .none => validN_op_left
   | .some z => fun h =>
@@ -234,7 +234,7 @@ theorem validN_op_opM_left {mz : Option α} : ✓{n} (x • y) •? mz → ✓{n
       _           ≡{n}≡ (x • z) • y := op_assocN
     validN_op_left ((Dist.validN this).mp h)
 
-theorem validN_op_opM_right {mz : Option α} (h : ✓{n} (x • y) •? mz) : ✓{n} y •? mz :=
+theorem validN_op_opM_right {mz : Option α} (h : ✓{n} (x • y : α) •? mz) : ✓{n} y •? mz :=
   validN_op_opM_left (validN_ne (opM_left_dist mz op_commN) h)
 
 /-! ## Core -/
diff --git a/src/Iris/Algebra/DFrac.lean b/src/Iris/Algebra/DFrac.lean
index e578e167..47db59f4 100644
--- a/src/Iris/Algebra/DFrac.lean
+++ b/src/Iris/Algebra/DFrac.lean
@@ -7,6 +7,8 @@ Authors: Markus de Medeiros, Mario Carneiro
 import Iris.Algebra.CMRA
 import Iris.Algebra.OFE
 import Iris.Algebra.Frac
+import Iris.Algebra.Updates
+import Iris.Algebra.LocalUpdates
 
 namespace Iris
 
@@ -138,4 +140,61 @@ theorem valid_discard : ✓ (discard : DFrac F) := by simp [CMRA.Valid, valid]
 theorem valid_own_op_discard {q : F} : ✓ own q • discard ↔ Fractional q := by
   simp [CMRA.op, op, CMRA.Valid, valid]
 
+instance : CMRA.Discrete (DFrac F) where
+  discrete_valid {x} := by simp [CMRA.Valid, CMRA.ValidN]
+
+theorem dfrac.is_discrete {q : DFrac F} : OFE.DiscreteE q := ⟨congrArg id⟩
+
+instance : CMRA.Discrete (DFrac F) where
+  discrete_valid {x} := by simp [CMRA.Valid, CMRA.ValidN]
+
+theorem dfrac_discard_update {dq : DFrac F} : dq ~~> .discard := by
+  rintro n (_|⟨q|_|q⟩) H <;>
+    have H' := (CMRA.valid_iff_validN' n).mpr H <;>
+    apply (CMRA.valid_iff_validN' n).mp <;>
+    simp [CMRA.op?] at H' ⊢
+  · simp [CMRA.Valid, valid]
+  · cases dq
+    · exact valid_op_own H
+    · exact H
+    · exact valid_op_own H
+  · simp [CMRA.Valid, valid, CMRA.op, op]
+  · cases dq
+    · exact CMRA.valid_op_right _ _ H
+    · exact H
+    · exact CMRA.valid_op_right _ _ H
+
+theorem dfrac_undiscard_update [IsSplitFraction F] :
+    (.discard : DFrac F) ~~>: fun k => ∃ q, k = .own q := by
+  apply UpdateP.discrete.mpr
+  rintro (_|⟨q|_|q⟩)
+  · rintro _
+    exists (.own One.one)
+    refine ⟨⟨One.one, rfl⟩, ?_⟩
+    simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid, add_comm]
+    apply UFraction.one_whole.1
+  · rintro ⟨q', HP⟩
+    exists (.own q')
+    refine ⟨⟨q', rfl⟩, ?_⟩
+    simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid, add_comm]
+    exact HP
+  · intro _
+    let q' : F := (IsSplitFraction.split One.one).1
+    exists (.own q')
+    refine ⟨⟨q', rfl⟩, ?_⟩
+    simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid]
+    exists (IsSplitFraction.split One.one).2
+    rw [IsSplitFraction.split_add]
+    apply UFraction.one_whole.1
+  · rintro ⟨q', HP⟩
+    let q'' : F := (IsSplitFraction.split q').1
+    exists (.own q'')
+    refine ⟨⟨q'', rfl⟩, ?_⟩
+    simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid]
+    rw [add_comm]
+    exists (IsSplitFraction.split q').2
+    rw [← add_assoc]
+    rw [IsSplitFraction.split_add]
+    exact HP
+
 end dfrac
diff --git a/src/Iris/Algebra/Frac.lean b/src/Iris/Algebra/Frac.lean
index 59be0f53..3f94d905 100644
--- a/src/Iris/Algebra/Frac.lean
+++ b/src/Iris/Algebra/Frac.lean
@@ -27,6 +27,10 @@ class Fraction (α : Type _) extends Add α where
   add_ne : ∀ {a b : α}, a ≠ b + a
   proper_add_mono_left : ∀ {a b : α}, Proper (a + b) → Proper a
 
+class IsSplitFraction (α : Type _) [Fraction α] where
+  split : α → α × α
+  split_add {a : α} : (split a).1 + (split a).2 = a
+
 namespace Fraction
 
 /-- A fraction does not represent the entire resource.
diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index 1d6404f2..7354cbbb 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -284,6 +284,24 @@ instance [OFE α] [Leibniz α] : Leibniz (Option α) where
     | none, none, _ => rfl
     | some _, some _, h => congrArg some (Leibniz.eq_of_eqv h)
 
+instance [OFE α] [Discrete α] : Discrete (Option α) where
+  discrete_0 {x y} H :=
+    match x, y with
+    | none, none => H
+    | some _, some _ => some_eqv_some.mpr (discrete_0 H)
+
+instance OFE.Option.some.ne [OFE α] : OFE.NonExpansive (some : α → Option α) := ⟨fun _ _ _ => id⟩
+
+theorem Option.some_is_discrete [OFE α] {a : α} (Ha : DiscreteE a) : DiscreteE (some a) := by
+  constructor
+  intro y H; cases y
+  · exact H
+  · exact Ha.discrete H
+
+theorem Option.none_is_discrete [OFE α] : DiscreteE (none : Option α) := by
+  constructor
+  intro y; cases y <;> simp
+
 abbrev OFEFun {α : Type _} (β : α → Type _) := ∀ a, OFE (β a)
 
 instance [OFEFun (β : α → _)] : OFE ((x : α) → β x) where
@@ -349,6 +367,19 @@ theorem dist_snd {n} [OFE α] [OFE β] {x y : α × β} (h : x ≡{n}≡ y) : x.
 theorem dist_prod_ext {n} [OFE α] [OFE β] {x₁ x₂ : α} {y₁ y₂ : β}
     (ex : x₁ ≡{n}≡ x₂) (ey : y₁ ≡{n}≡ y₂) : (x₁, y₁) ≡{n}≡ (x₂, y₂) := ⟨ex, ey⟩
 
+theorem prod.is_discrete [OFE α] [OFE β] {a : α} {b : β} (Ha : DiscreteE a) (Hb : DiscreteE b) :
+    DiscreteE (a, b) := by
+  constructor
+  intro y H; refine ⟨Ha.discrete H.1, Hb.discrete H.2⟩
+
+instance [OFE α] [OFE β] [Discrete α] [Discrete β] : Discrete (α × β) where
+  discrete_0 H := by
+    constructor
+    · apply Discrete.discrete_0
+      apply H.1
+    · apply Discrete.discrete_0
+      apply H.2
+
 /-- An isomorphism between two OFEs is a pair of morphisms whose composition is equivalent to the
 identity morphism. -/
 @[ext] structure Iso (α β : Type _) [OFE α] [OFE β] where
diff --git a/src/Iris/Algebra/Updates.lean b/src/Iris/Algebra/Updates.lean
index 07dd8c1f..b506f62e 100644
--- a/src/Iris/Algebra/Updates.lean
+++ b/src/Iris/Algebra/Updates.lean
@@ -110,7 +110,7 @@ theorem UpdateP.op {P Q R : α → Prop} {x y}
   exact ⟨z • w, pqr z w pz pw, CMRA.validN_ne (CMRA.op_opM_assoc_dist z w mz).symm vz⟩
 
 theorem UpdateP.op' {P Q : α → Prop} {x y : α} (uxp : x ~~>: P) (uyq : y ~~>: Q) :
-    x • y ~~>: λ t ↦ ∃ z w, t = z • w ∧ P z ∧ Q w :=
+    (x • y : α) ~~>: λ t ↦ ∃ z w, t = (z • w : α) ∧ P z ∧ Q w :=
   .op uxp uyq fun z w pz qw => ⟨z, w, rfl, pz, qw⟩
 
 theorem Update.op {x₁ x₂ y₁ y₂ : α} (xy₁ : x₁ ~~> y₁) (xy₂ : x₂ ~~> y₂) : x₁ • x₂ ~~> y₁ • y₂ :=
diff --git a/src/Iris/Algebra/View.lean b/src/Iris/Algebra/View.lean
new file mode 100644
index 00000000..5fef8d85
--- /dev/null
+++ b/src/Iris/Algebra/View.lean
@@ -0,0 +1,762 @@
+/-
+Copyright (c) 2025 Markus de Medeiros. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+
+import Iris.Algebra.CMRA
+import Iris.Algebra.OFE
+import Iris.Algebra.Frac
+import Iris.Algebra.DFrac
+import Iris.Algebra.Agree
+import Iris.Algebra.Updates
+import Iris.Algebra.LocalUpdates
+
+open Iris
+
+abbrev view_rel (A B : Type _) := Nat → A → B → Prop
+
+class ViewRel [OFE A] [UCMRA B] (R : view_rel A B) where
+  mono {n1 n2 : Nat} {a1 a2 : A} {b1 b2 : B} :
+    R n1 a1 b1 → a1 ≡{n2}≡ a2 → b2 ≼{n2} b1 → n2 ≤ n1 → R n2 a2 b2
+  rel_validN n a b : R n a b → ✓{n} b
+  rel_unit n : ∃ a, R n a UCMRA.unit
+
+class ViewRelDiscrete [OFE A] [UCMRA B] (R : view_rel A B) extends ViewRel R where
+  discrete n a b : R 0 a b → R n a b
+
+namespace viewrel
+
+variable [OFE A] [UCMRA B] {R : view_rel A B} [ViewRel R]
+
+theorem ne {a1 a2 : A} {b1 b2 : B} {n : Nat} (Ha : a1 ≡{n}≡ a2) (Hb : b1 ≡{n}≡ b2) : R n a1 b1 ↔ R n a2 b2 :=
+  ⟨(ViewRel.mono · Ha Hb.symm.to_incN n.le_refl), (ViewRel.mono · Ha.symm Hb.to_incN n.le_refl)⟩
+
+theorem eqv_ne {a1 a2 : A} {b1 b2 : B} (Ha : a1 ≡ a2) (Hb : b1 ≡ b2) : R n a1 b1 ↔ R n a2 b2 :=
+  ne Ha.dist Hb.dist
+
+end viewrel
+
+structure View (F : Type _) {A B : Type _} (R : view_rel A B) where
+  π_auth : Option ((DFrac F) × Agree A)
+  π_frag : B
+
+abbrev View.auth [UCMRA B] {R : view_rel A B} (dq : DFrac F) (a : A) : View F R :=
+  ⟨some (dq, toAgree a), UCMRA.unit⟩
+
+abbrev View.frag {R : view_rel A B} (b : B) : View F R := ⟨none, b⟩
+
+notation "●V{" dq "} " a => View.auth dq a
+notation "●V " a => View.auth (DFrac.own One.one) a
+notation "◯V " b => View.frag b
+
+namespace View
+section ofe
+
+variable [OFE A] [OFE B] {R : view_rel A B}
+
+abbrev equiv (x y : View F R) : Prop := x.π_auth ≡ y.π_auth ∧ x.π_frag ≡ y.π_frag
+abbrev dist (n : Nat) (x y : View F R) : Prop := x.π_auth ≡{n}≡ y.π_auth ∧ x.π_frag ≡{n}≡ y.π_frag
+
+instance : OFE (View F R) where
+  Equiv := equiv
+  Dist := dist
+  dist_eqv := {
+    refl _ := ⟨OFE.Dist.of_eq rfl, OFE.Dist.of_eq rfl⟩
+    symm H := ⟨H.1.symm, H.2.symm⟩
+    trans H1 H2 := ⟨H1.1.trans H2.1, H1.2.trans H2.2⟩
+  }
+  equiv_dist :=
+    ⟨fun H _ => ⟨H.1.dist, H.2.dist⟩,
+     fun H => ⟨OFE.equiv_dist.mpr (H · |>.1), OFE.equiv_dist.mpr (H · |>.2)⟩⟩
+  dist_lt H Hn := ⟨OFE.dist_lt H.1 Hn, OFE.dist_lt H.2 Hn⟩
+
+instance View.mk.ne : OFE.NonExpansive₂ (View.mk : _ → _ → View F R) := ⟨fun _ _ _ Ha _ _ Hb => ⟨Ha, Hb⟩⟩
+instance View.π_auth.ne : OFE.NonExpansive (View.π_auth : View F R → _) := ⟨fun _ _ _ H => H.1⟩
+instance View.π_frag.ne : OFE.NonExpansive (View.π_frag : View F R → _) := ⟨fun _ _ _ H => H.2⟩
+
+theorem is_discrete {ag : Option ((DFrac F) × Agree A)} (Ha : OFE.DiscreteE ag) (Hb : OFE.DiscreteE b) :
+  OFE.DiscreteE (α := View F R) (View.mk ag b) := ⟨fun H => ⟨Ha.discrete H.1, Hb.discrete H.2⟩⟩
+
+open OFE in
+instance [Discrete A] [Discrete B] : Discrete (View F R) where
+  discrete_0 H := ⟨Discrete.discrete_0 H.1, Discrete.discrete_0 H.2⟩
+
+theorem view_auth.frac_inj [UCMRA B] {q1 q2 : DFrac F} {a1 a2 : A} {n} (H : (●V{q1} a1 : View F R) ≡{n}≡ ●V{q2} a2) :
+    q1 = q2 := H.1.1
+
+theorem view_auth.ag_inj [UCMRA B] {q1 q2 : DFrac F} {a1 a2 : A} {n} (H : (●V{q1} a1 : View F R) ≡{n}≡ ●V{q2} a2) :
+    a1 ≡{n}≡ a2 := toAgree.inj H.1.2
+
+theorem view_frag.inj [UCMRA B] {b1 b2 : B} {n} (H : (◯V b1 : View F R) ≡{n}≡ ◯V b2) :
+    b1 ≡{n}≡ b2 := H.2
+
+theorem view_auth_discrete [UFraction F] [UCMRA B] {dq a} (Ha : OFE.DiscreteE a) (He : OFE.DiscreteE (UCMRA.unit : B)) :
+    OFE.DiscreteE (●V{dq} a : View F R) := by
+  refine is_discrete ?_ He
+  apply OFE.Option.some_is_discrete
+  apply OFE.prod.is_discrete dfrac.is_discrete
+  apply Agree.toAgree.is_discrete
+  exact Ha
+
+theorem view_frag_discrete [UCMRA B] {b : B} (Hb : OFE.DiscreteE b) : (OFE.DiscreteE (◯V b : View F R)) :=
+  is_discrete OFE.Option.none_is_discrete Hb
+
+end ofe
+
+section cmra
+variable [UFraction F] [OFE A] [IB : UCMRA B] {R : view_rel A B} [ViewRel R]
+
+theorem rel_iff_agree (Hb : b' ≡{n}≡ b) :
+    (∃ a', toAgree a ≡{n}≡ toAgree a' ∧ R n a' b') ↔ R n a b := by
+  refine ⟨fun H => ?_, fun H => ?_⟩
+  · rcases H with ⟨_, HA, HR⟩
+    exact ViewRel.mono HR (toAgree.inj HA.symm) Hb.symm.to_incN n.le_refl
+  · exact ⟨a, .rfl, ViewRel.mono H .rfl Hb.to_incN n.le_refl⟩
+
+instance auth_ne {dq : DFrac F} : OFE.NonExpansive (View.auth dq : A → View F R) where
+  ne _ _ _ H := by
+    refine View.mk.ne.ne ?_ .rfl
+    refine OFE.some_dist_some.mpr ⟨.rfl, ?_⟩
+    simp only
+    exact OFE.NonExpansive.ne H
+
+instance auth_ne₂ : OFE.NonExpansive₂ (View.auth : DFrac F → A → View F R) where
+  ne _ _ _ Hq _ _ Hf := by
+    unfold auth
+    refine (OFE.NonExpansive₂.ne ?_ .rfl)
+    refine OFE.NonExpansive.ne ?_
+    exact OFE.dist_prod_ext Hq (OFE.NonExpansive.ne Hf)
+
+instance frag_ne : OFE.NonExpansive (View.frag : B → View F R) where
+  ne _ _ _ H := View.mk.ne.ne .rfl H
+
+@[simp] def valid (v : View F R) : Prop :=
+  match v.π_auth with
+  | some (dq, ag) => ✓ dq ∧ (∀ n, ∃ a, ag ≡{n}≡ toAgree a ∧ R n a (π_frag v))
+  | none => ∀ n, ∃ a, R n a (π_frag v)
+
+@[simp] def validN (n : Nat) (v : View F R) : Prop :=
+  match v.π_auth with
+  | some (dq, ag) => ✓{n} dq ∧ (∃ a, ag ≡{n}≡ toAgree a ∧ R n a (π_frag v))
+  | none => ∃ a, R n a (π_frag v)
+
+@[simp] def pcore (v : View F R) : Option (View F R) :=
+  some <| View.mk (CMRA.core v.1) (CMRA.core v.2)
+
+@[simp] def op (v1 v2 : View F R) : View F R :=
+  View.mk (v1.1 • v2.1) (v1.2 • v2.2)
+
+instance : CMRA (View F R) where
+  pcore := pcore
+  op := op
+  ValidN := validN
+  Valid := valid
+  op_ne.ne n x1 x2 H := by
+    refine View.mk.ne.ne ?_ ?_
+    · refine cmraOption.op_ne.ne (OFE.NonExpansive.ne H)
+    · refine IB.op_ne.ne (OFE.NonExpansive.ne H)
+  pcore_ne {n x y} cx H := by
+    simp only [pcore, Option.some.injEq]
+    intro Hc; subst Hc
+    exists { π_auth := CMRA.core y.π_auth, π_frag := CMRA.core y.π_frag }
+    exact ⟨rfl, ⟨OFE.Dist.core H.1, OFE.Dist.core H.2⟩⟩
+  validN_ne {n x1 x2} H := by
+    simp [validN]
+    rcases H with ⟨Hl, Hr⟩
+    rcases x1 with ⟨_|⟨q1, ag1⟩, b1⟩ <;>
+    rcases x2 with ⟨_|⟨q2, ag2⟩, b2⟩ <;>
+    simp_all
+    · intro x H
+      exists x
+      exact ViewRel.mono H .rfl Hr.symm.to_incN n.le_refl
+    intro Hq a Hag HR
+    refine ⟨CMRA.discrete_valid <| DFrac_CMRA.validN_ne Hl.1 Hq, ?_⟩
+    refine ⟨a, ?_⟩
+    refine ⟨Hl.2.symm.trans Hag, ?_⟩
+    refine ViewRel.mono HR .rfl ?_ n.le_refl
+    exact OFE.Dist.to_incN Hr.symm
+  valid_iff_validN {x} := by
+    simp only [valid, validN]; split
+    · exact ⟨fun H n => ⟨H.1, H.2 n⟩, fun H => ⟨(H 0).1, fun n => (H n).2⟩⟩
+    · exact Eq.to_iff rfl
+  validN_succ {x n} := by
+    simp only [validN]
+    split
+    · refine fun H => ⟨H.1, ?_⟩
+      rcases H.2 with ⟨ag, Ha⟩; exists ag
+      refine ⟨OFE.Dist.le Ha.1 n.le_succ, ?_⟩
+      exact ViewRel.mono Ha.2 .rfl (CMRA.incN_refl x.π_frag) n.le_succ
+    · rintro ⟨z, HR⟩
+      exists z
+      exact ViewRel.mono HR .rfl (CMRA.incN_refl _) n.le_succ
+  validN_op_left {n x y} := by
+    simp [op, validN]
+    rcases x with ⟨_|⟨q1, ag1⟩, b1⟩ <;>
+    rcases y with ⟨_|⟨q2, ag2⟩, b2⟩ <;>
+    simp [CMRA.op, optionOp]
+    · refine fun a Hr => ⟨a, ?_⟩
+      exact ViewRel.mono Hr .rfl (CMRA.incN_op_left n b1 b2) n.le_refl
+    · refine fun _ a _ Hr => ⟨a, ?_⟩
+      apply ViewRel.mono Hr .rfl (CMRA.incN_op_left n b1 b2) n.le_refl
+    · refine fun Hq a H Hr => ⟨Hq, ⟨a, ⟨H, ?_⟩⟩⟩
+      apply ViewRel.mono Hr .rfl (CMRA.incN_op_left n b1 b2) n.le_refl
+    · refine fun Hq a H Hr => ⟨CMRA.validN_op_left Hq, ⟨a, ?_⟩⟩
+      refine ⟨?_, ?_⟩
+      · refine .trans ?_ H
+        refine .trans Agree.idemp.symm.dist ?_
+        exact CMRA.op_ne.ne <| Agree.op_invN (Agree.validN_ne H.symm trivial)
+      · exact ViewRel.mono Hr .rfl (CMRA.incN_op_left n b1 b2) n.le_refl
+  assoc := OFE.NonExpansive₂.eqv CMRA.assoc CMRA.assoc
+  comm := OFE.NonExpansive₂.eqv CMRA.comm CMRA.comm
+  pcore_op_left {x _} := by
+    simp only [pcore, Option.some.injEq]
+    exact fun H => H ▸ OFE.NonExpansive₂.eqv (CMRA.core_op x.π_auth) (CMRA.core_op x.π_frag)
+  pcore_idem {_ cx} := by
+    simp only [pcore, Option.some.injEq, OFE.some_eqv_some]
+    rcases cx
+    simp only [mk.injEq, and_imp]
+    intro H1 H2
+    constructor
+    · simp only; exact H1 ▸ CMRA.core_idem _
+    · exact H2 ▸ CMRA.core_idem _
+  pcore_op_mono := by
+    apply pcore_op_mono_of_core_op_mono
+    let f : (Option ((DFrac F) × Agree A) × B) → View F R := fun x => ⟨x.1, x.2⟩
+    let g : View F R → (Option ((DFrac F) × Agree A) × B) := fun x => (x.1, x.2)
+    let opM' (x : View F R) (y : Option (View F R)) : View F R :=
+      match y with | some y => op x y | none => x
+
+    have g_pcore_0 {y : View F R} : CMRA.pcore (g y) ≡ g <$> pcore y := by
+      rcases y with ⟨x, b⟩
+      simp only [pcore, Option.map_eq_map, Option.map, g]
+      simp [CMRA.pcore, Prod.pcore, optionCore]
+      simp [CMRA.pcore_eq_core]
+      rfl
+
+    have g_pcore {y cy : View F R} : pcore y ≡ some cy ↔ CMRA.pcore (g y) ≡ some (g cy) := by
+      suffices y.pcore ≡ some cy ↔ g <$> y.pcore ≡ some (g cy) by
+        exact ⟨g_pcore_0.trans ∘ this.mp, this.mpr ∘ g_pcore_0.symm.trans⟩
+      refine Iff.trans OFE.equiv_dist (Iff.trans ?_ OFE.equiv_dist.symm)
+      exact ⟨fun H n => H n, fun H n => H n⟩
+
+    have g_opM_f {x y} : g (opM' y (f x)) ≡ CMRA.op (g y) x := by
+      simp [opM', g, f, CMRA.op, Prod.op]
+
+    rintro y1 cy y2 ⟨z, Hy2⟩ Hy1
+    let Lcore := (@CMRA.pcore_mono' _ _ (g y1) (g y2) (g cy) ?G1 ?G2)
+    case G1 => exists (g z)
+    case G2 => exact g_pcore.mp <| OFE.Equiv.of_eq Hy1
+    rcases Lcore with ⟨cx, Hcgy2, ⟨x, Hcx⟩⟩
+    have Hcx' : cx ≡ g (opM' cy (f x)) := Hcx
+    have Hcgy2' : CMRA.pcore (g y2) ≡ some (g (opM' cy (f x))) := by rw [Hcgy2]; exact Hcx
+    have Hcgy2'' : pcore y2 ≡ some (opM' cy (f x)) := g_pcore.mpr Hcgy2'
+    generalize HC : y2.pcore = C
+    rw [HC] at Hcgy2''
+    cases C; exact Hcgy2''.elim
+    rename_i cy'
+    refine ⟨cy', ⟨rfl, ?_⟩⟩
+    exists (f x)
+  extend {n x y1 y2} Hv He := by
+    let g : View F R → (Option ((DFrac F) × Agree A) × B) := fun x => (x.1, x.2)
+    have H2 := @CMRA.extend _ _ n (g x) (g y1) (g y2) ?G1 He
+    case G1 =>
+      simp_all [validN, CMRA.ValidN, Prod.ValidN, g, optionValidN]
+      rcases x with ⟨_|⟨q1, ag1⟩, b1⟩ <;> simp_all only
+      · refine ⟨trivial, ?_⟩
+        rcases Hv with ⟨_, Ha⟩
+        apply ViewRel.rel_validN _ _ _ Ha
+      · rcases Hv with ⟨Hq, ⟨a, ⟨Ha1, Ha2⟩⟩⟩
+        refine ⟨⟨trivial, ?_⟩, ?_⟩
+        · exact Agree.validN_ne Ha1.symm trivial
+        · exact ViewRel.rel_validN _ _ _ Ha2
+    rcases H2 with ⟨z1, z2, Hze, Hz1, Hz2⟩
+    exists ⟨z1.1, z1.2⟩
+    exists ⟨z2.1, z2.2⟩
+
+instance [OFE.Discrete A] [CMRA.Discrete B] [ViewRelDiscrete R] : CMRA.Discrete (View F R) where
+  discrete_valid := by
+    simp [CMRA.ValidN, validN, CMRA.Valid, valid]
+    intro x
+    split
+    · rintro ⟨H1, ⟨a, H2, H3⟩⟩
+      refine ⟨H1, fun n => ⟨a, ⟨?_, ?_⟩⟩⟩
+      · exact OFE.equiv_dist.mp (OFE.Discrete.discrete_0 H2) _
+      · exact ViewRelDiscrete.discrete _ _ _ H3
+    · rintro ⟨a, H⟩ _
+      exact ⟨a, ViewRelDiscrete.discrete _ _ _ H⟩
+
+instance : UCMRA (View F R) where
+  unit := ⟨UCMRA.unit, UCMRA.unit⟩
+  unit_valid := ViewRel.rel_unit
+  unit_left_id := ⟨UCMRA.unit_left_id, UCMRA.unit_left_id⟩
+  pcore_unit := ⟨by rfl, CMRA.core_eqv_self UCMRA.unit⟩
+
+theorem view_core_eq : (CMRA.core : View F R → _) = fun v => ⟨CMRA.core v.1, CMRA.core v.2⟩ := rfl
+
+theorem view_auth_dfrac_op : (●V{dq1 • dq2} a : View F R) ≡ (●V{dq1} a) • ●V{dq2} a :=
+  ⟨⟨rfl, Agree.idemp.symm⟩, UCMRA.unit_left_id.symm⟩
+
+theorem view_frag_op : (◯V (b1 • b2) : View F R) = ((◯V b1) • ◯V b2 : View F R):= rfl
+
+theorem view_frag_mono (H : b1 ≼ b2) : (◯V b1 : View F R) ≼ ◯V b2 := by
+  rcases H with ⟨c, H⟩
+  refine CMRA.inc_of_inc_of_eqv ?_ (frag_ne.eqv H.symm)
+  rw [view_frag_op]
+  exact CMRA.inc_op_left _ _
+
+theorem view_frag_core : CMRA.core (◯V b : View F R) = ◯V (CMRA.core b) := rfl
+
+theorem view_both_core_discarded : CMRA.core ((●V{.discard} a) • ◯V b : View F R) ≡ (●V{.discard} a) • ◯V (CMRA.core b) :=
+  ⟨.rfl, (CMRA.core_ne.eqv UCMRA.unit_left_id).trans UCMRA.unit_left_id.symm⟩
+
+theorem view_both_core_frac : CMRA.core ((●V{.own q} a) • ◯V b : View F R) ≡ ◯V (CMRA.core b) :=
+  ⟨trivial, CMRA.core_ne.eqv UCMRA.unit_left_id⟩
+
+instance view_auth_core_id : CMRA.CoreId (●V{.discard} a : View F R) where
+  core_id := ⟨.rfl, CMRA.core_eqv_self UCMRA.unit⟩
+
+instance view_frag_core_id [CMRA.CoreId b] : CMRA.CoreId (◯V b : View F R) where
+  core_id := ⟨.rfl, CMRA.coreId_iff_core_eqv_self.mp (by trivial)⟩
+
+instance view_both_core_id [CMRA.CoreId b] : CMRA.CoreId ((●V{.discard} a : View F R) • ◯V b) where
+  core_id := by
+    refine ⟨.rfl, ?_⟩
+    refine (CMRA.core_ne.eqv UCMRA.unit_left_id).trans ?_
+    refine (CMRA.coreId_iff_core_eqv_self.mp (by trivial)).trans ?_
+    refine UCMRA.unit_left_id.symm
+
+theorem view_auth_dfrac_op_invN (H : ✓{n} ((●V{dq1} a1 : View F R) • ●V{dq2} a2)) : a1 ≡{n}≡ a2 := by
+  rcases H with ⟨_, _, H, _⟩
+  refine toAgree.inj (Agree.op_invN ?_)
+  exact Agree.validN_ne H.symm trivial
+
+theorem view_auth_dfrac_op_inv (H : ✓ ((●V{dq1} a1 : View F R) • ●V{dq2} a2)) : a1 ≡ a2 :=
+  OFE.equiv_dist.mpr fun _ => view_auth_dfrac_op_invN H.validN
+
+theorem view_auth_dfrac_validN : ✓{n} (●V{dq} a : View F R) ↔ ✓{n}dq ∧ R n a UCMRA.unit :=
+  and_congr_right fun _ => rel_iff_agree .rfl
+
+theorem view_auth_validN n a : ✓{n} (●V a : View F R) ↔ R n a UCMRA.unit :=
+  ⟨(view_auth_dfrac_validN.mp · |>.2), (view_auth_dfrac_validN.mpr ⟨UFraction.one_whole.1, ·⟩)⟩
+
+theorem view_auth_dfrac_op_validN :
+    ✓{n} ((●V{dq1} a1 : View F R) • ●V{dq2} a2) ↔ ✓(dq1 • dq2) ∧ a1 ≡{n}≡ a2 ∧ R n a1 UCMRA.unit := by
+  refine ⟨fun H => ?_, fun H => ?_⟩
+  · let Ha' : a1 ≡{n}≡ a2 := view_auth_dfrac_op_invN H
+    rcases H with ⟨Hq, _, Ha, HR⟩
+    refine ⟨Hq, Ha', ViewRel.mono HR ?_ CMRA.incN_unit n.le_refl⟩
+    refine .trans ?_ Ha'.symm
+    refine toAgree.inj ?_
+    apply Ha.symm.trans
+    apply CMRA.op_commN.trans
+    apply (CMRA.op_ne.ne (toAgree.ne.ne Ha')).trans
+    apply Agree.idemp
+  · simp [CMRA.op, CMRA.ValidN, validN, optionOp, Prod.op]
+    refine ⟨H.1, a1, ?_, ?_⟩
+    · exact (CMRA.op_ne.ne <| toAgree.ne.ne H.2.1.symm).trans Agree.idemp.dist
+    · refine ViewRel.mono H.2.2 .rfl ?_ n.le_refl
+      exact OFE.Dist.to_incN <| CMRA.unit_left_id_dist UCMRA.unit
+
+theorem view_auth_op_validN : ✓{n} ((●V a1 : View F R) • ●V a2) ↔ False := by
+  refine view_auth_dfrac_op_validN.trans ?_
+  simp only [iff_false, not_and]
+  intro _
+  refine (UFraction.one_whole (α := F)).2 ?_ |>.elim
+  exists 1
+
+theorem view_frag_validN : ✓{n} (◯V b : View F R) ↔ ∃ a, R n a b := by rfl
+
+theorem view_both_dfrac_validN : ✓{n} ((●V{dq} a : View F R) • ◯V b) ↔ ✓dq ∧ R n a b :=
+  and_congr_right (fun _ => rel_iff_agree <| CMRA.unit_left_id_dist b)
+
+theorem view_both_validN : ✓{n} ((●V a : View F R) • ◯V b) ↔ R n a b :=
+  view_both_dfrac_validN.trans <| and_iff_right_iff_imp.mpr (fun _ => valid_own_one)
+
+theorem view_auth_dfrac_valid : ✓ (●V{dq} a : View F R) ↔ ✓dq ∧ ∀ n, R n a UCMRA.unit :=
+  and_congr_right (fun _=> forall_congr' fun _ => rel_iff_agree .rfl)
+
+theorem view_auth_valid : ✓ (●V a : View F R) ↔ ∀ n, R n a UCMRA.unit :=
+  view_auth_dfrac_valid.trans <| and_iff_right_iff_imp.mpr (fun _ => valid_own_one)
+
+theorem view_auth_dfrac_op_valid : ✓ ((●V{dq1} a1 : View F R) • ●V{dq2} a2) ↔ ✓(dq1 • dq2) ∧ a1 ≡ a2 ∧ ∀ n, R n a1 UCMRA.unit := by
+  refine CMRA.valid_iff_validN.trans ?_
+  refine ⟨fun H => ?_, fun H n => ?_⟩
+  · simp [CMRA.Valid, valid, auth, CMRA.op, op, optionOp, CMRA.ValidN, validN] at H
+    let Hn (n) := view_auth_dfrac_op_invN (H n)
+    refine ⟨(H 0).1, OFE.equiv_dist.mpr Hn, fun n => ?_⟩
+    · rcases (H n) with ⟨_, _, Hl, H⟩
+      apply ViewRel.mono H ?_ CMRA.incN_unit n.le_refl
+      apply toAgree.inj
+      apply Hl.symm.trans
+      exact (CMRA.op_ne.ne <| toAgree.ne.ne (Hn _).symm).trans Agree.idemp.dist
+  · exact view_auth_dfrac_op_validN.mpr ⟨H.1, H.2.1.dist, H.2.2 n⟩
+
+theorem view_auth_op_valid : ✓ ((●V a1 : View F R) • ●V a2) ↔ False := by
+  refine view_auth_dfrac_op_valid.trans ?_
+  simp [CMRA.op, op, CMRA.Valid, op, valid]
+  intro _
+  refine (UFraction.one_whole (α := F)).2 ?_ |>.elim
+  exists 1
+
+theorem view_frag_valid : ✓ (◯V b : View F R) ↔ ∀ n, ∃ a, R n a b := by rfl
+
+theorem view_both_dfrac_valid : ✓ ((●V{dq} a : View F R) • ◯V b) ↔ ✓dq ∧ ∀ n, R n a b :=
+  and_congr_right (fun _ => forall_congr' fun _ => rel_iff_agree <| CMRA.unit_left_id_dist b)
+
+theorem view_both_valid : ✓ ((●V a : View F R) • ◯V b) ↔ ∀ n, R n a b :=
+  view_both_dfrac_valid.trans <| and_iff_right_iff_imp.mpr (fun _ => valid_own_one)
+
+theorem view_auth_dfrac_includedN : (●V{dq1} a1 : View F R) ≼{n} ((●V{dq2} a2) • ◯V b) ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2 := by
+  refine ⟨?_, ?_⟩
+  · simp only [auth, frag, CMRA.IncludedN, CMRA.op, op, optionOp, Prod.op]
+    rintro ⟨(_|⟨dqf, af⟩),⟨⟨x1, x2⟩, y⟩⟩
+    · exact ⟨Or.inr x1.symm, toAgree.inj x2.symm⟩
+    · simp_all only []
+      apply And.intro
+      · left; exists dqf
+      · apply toAgree.incN.mp; exists af
+  · intro H
+    -- simp only [auth, frag, CMRA.IncludedN, CMRA.op, op, optionOp, Prod.op]
+    rcases H with ⟨(⟨z, HRz⟩| HRa2), HRb⟩
+    · -- have _ := @view_auth_dfrac_op
+      apply (CMRA.incN_iff_right <| ?G).mp
+      case G =>
+        apply OFE.equiv_dist.mp
+        apply CMRA.comm
+      apply (CMRA.incN_iff_right <| ?G).mp
+      case G =>
+        apply CMRA.op_ne.ne
+        apply OFE.NonExpansive₂.ne HRz.symm HRb
+      apply (CMRA.incN_iff_right <| ?G).mp
+      case G =>
+        apply CMRA.op_ne.ne
+        apply OFE.equiv_dist.mp
+        apply view_auth_dfrac_op.symm
+      apply (CMRA.incN_iff_right <| ?G).mp
+      case G =>
+        apply CMRA.op_ne.ne
+        apply OFE.equiv_dist.mp
+        apply CMRA.comm
+      apply (CMRA.incN_iff_right <| ?G).mp
+      case G =>
+        apply OFE.equiv_dist.mp
+        apply CMRA.assoc.symm
+      apply (CMRA.incN_iff_right <| ?G).mp
+      case G =>
+        apply OFE.equiv_dist.mp
+        apply CMRA.comm
+      exists ((◯V b) • ●V{z} a1)
+    · exists (◯V b)
+      refine .trans (OFE.equiv_dist.mp CMRA.comm _) (.trans ?_ (OFE.equiv_dist.mp CMRA.comm _))
+      apply CMRA.op_ne.ne
+      rw [HRa2]
+      exact OFE.NonExpansive₂.ne rfl HRb.symm
+
+theorem view_auth_dfrac_included : ((●V{dq1} a1 : View F R) ≼ (●V{dq2} a2 : View F R) • ◯V b) ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2 := by
+  refine ⟨fun H => ⟨?_, ?_⟩, fun H => ?_⟩
+  · exact view_auth_dfrac_includedN (n := 0) |>.mp (CMRA.incN_of_inc _ H) |>.1
+  · refine OFE.equiv_dist.mpr (fun n => ?_)
+    exact view_auth_dfrac_includedN |>.mp (CMRA.incN_of_inc _ H) |>.2
+  · rcases H with ⟨(⟨q, Hq⟩|Hq), Ha⟩
+    · apply (CMRA.inc_iff_right <| ?G).mp
+      case G =>
+        apply OFE.Equiv.symm
+        apply CMRA.comm.trans
+        apply CMRA.op_ne.eqv
+        apply auth_ne₂.eqv Hq Ha.symm
+      apply (CMRA.inc_iff_right <| ?G1).mp
+      case G1 =>
+        apply CMRA.op_ne.eqv
+        apply view_auth_dfrac_op.symm
+      apply (CMRA.inc_iff_right <| CMRA.comm).mp
+      apply (CMRA.inc_iff_right <| CMRA.assoc).mp
+      exists ((●V{q} a1) • ◯V b)
+    · exists (◯V b)
+      refine .trans CMRA.comm (.trans ?_ CMRA.comm )
+      apply CMRA.op_ne.eqv
+      rw [Hq]
+      exact OFE.NonExpansive₂.eqv rfl Ha.symm
+
+theorem view_auth_includedN : (●V a1 : View F R) ≼{n} ((●V a2) • ◯V b) ↔ a1 ≡{n}≡ a2 :=
+  view_auth_dfrac_includedN.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl
+
+theorem view_auth_included : (●V a1 : View F R) ≼ ((●V a2) • ◯V b) ↔ a1 ≡ a2 :=
+  view_auth_dfrac_included.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl
+
+theorem view_frag_includedN : (◯V b1 : View F R) ≼{n} ((●V{p} a) • ◯V b2) ↔ b1 ≼{n} b2 := by
+  constructor
+  · rintro ⟨xf, ⟨_, Hb⟩⟩
+    simp [auth, frag, CMRA.op, op] at Hb
+    have Hb' : b2 ≡{n}≡ b1 • xf.π_frag := by
+      apply OFE.Dist.trans
+      apply OFE.Dist.symm
+      apply OFE.equiv_dist.mp
+      apply UCMRA.unit_left_id
+      apply Hb
+    apply (CMRA.incN_iff_right <| Hb'.symm).mp
+    exists xf.π_frag
+  · rintro ⟨bf, Hbf⟩
+    apply (CMRA.incN_iff_right <| ?G).mp
+    case G =>
+      apply CMRA.op_ne.ne
+      apply frag_ne.ne Hbf.symm
+    rw [view_frag_op]
+    apply (CMRA.incN_iff_right <| ?G).mp
+    case G =>
+      apply OFE.equiv_dist.mp
+      apply CMRA.comm
+    apply (CMRA.incN_iff_right <| ?G).mp
+    case G =>
+      apply OFE.equiv_dist.mp
+      apply CMRA.assoc
+    exists ((◯V bf) • ●V{p} a)
+
+theorem view_frag_included : (◯V b1 : View F R) ≼ ((●V{p} a) • ◯V b2) ↔ b1 ≼ b2 := by
+  constructor
+  · rintro ⟨xf, ⟨_, Hb⟩⟩
+    simp [auth, frag, CMRA.op, op] at Hb
+    have Hb' : b2 ≡ b1 • xf.π_frag := by
+      apply OFE.Equiv.trans
+      apply OFE.Equiv.symm
+      apply UCMRA.unit_left_id
+      apply Hb
+    apply (CMRA.inc_iff_right <| Hb'.symm).mp
+    exists xf.π_frag
+  · rintro ⟨bf, Hbf⟩
+    apply (CMRA.inc_iff_right <| ?G).mp
+    case G =>
+      apply CMRA.op_ne.eqv
+      apply frag_ne.eqv Hbf.symm
+    rw [view_frag_op]
+    apply (CMRA.inc_iff_right <| ?G).mp
+    case G => apply CMRA.comm
+    apply (CMRA.inc_iff_right <| ?G).mp
+    case G =>
+      apply CMRA.assoc
+    exists ((◯V bf) • ●V{p} a)
+
+theorem view_both_dfrac_includedN :
+    ((●V{dq1} a1 : View F R) • ◯V b1) ≼{n} ((●V{dq2} a2) • ◯V b2) ↔
+      (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2 := by
+  constructor
+  · intro H
+    rw [← and_assoc]
+    constructor
+    · apply (view_auth_dfrac_includedN (R := R)).mp
+      apply CMRA.incN_trans ?_ H
+      exact CMRA.incN_op_left n (●V{dq1} a1) (◯V b1)
+    · apply (view_frag_includedN (R := R) (F := F)).mp
+      apply CMRA.incN_trans (CMRA.incN_op_right _ _ _)
+      apply H
+  · rintro ⟨H0, H1, ⟨bf, H2⟩⟩
+    apply (CMRA.incN_iff_right <| ?G).mp
+    case G =>
+      apply CMRA.op_ne.ne
+      apply frag_ne.ne
+      apply OFE.Dist.symm
+      apply H2.trans
+      apply OFE.equiv_dist.mp
+      apply CMRA.comm
+    rewrite [view_frag_op]
+    apply (CMRA.incN_iff_right <| ?G).mp
+    case G =>
+      apply OFE.equiv_dist.mp
+      apply CMRA.assoc.symm
+    refine CMRA.op_monoN_left (◯V b1) ?_
+    apply view_auth_dfrac_includedN.mpr
+    exact ⟨H0, H1⟩
+
+theorem view_both_dfrac_included : ((●V{dq1} a1 : View F R) • ◯V b1) ≼ ((●V{dq2} a2) • ◯V b2) ↔
+      (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2 ∧ b1 ≼ b2 := by
+  constructor
+  · intro H
+    rw [← and_assoc]
+    constructor
+    · apply (view_auth_dfrac_included (R := R)).mp
+      apply CMRA.inc_trans ?_ H
+      exact CMRA.inc_op_left (●V{dq1} a1) (◯V b1)
+    · apply (view_frag_included (R := R) (F := F)).mp
+      apply CMRA.inc_trans (CMRA.inc_op_right _ _)
+      apply H
+  · rintro ⟨H0, H1, ⟨bf, H2⟩⟩
+    apply (CMRA.inc_iff_right <| ?G).mp
+    case G =>
+      apply CMRA.op_ne.eqv
+      apply frag_ne.eqv
+      apply OFE.Equiv.symm
+      apply H2.trans
+      apply CMRA.comm
+    rewrite [view_frag_op]
+    apply (CMRA.inc_iff_right <| ?G).mp
+    case G =>
+      apply CMRA.assoc.symm
+    refine CMRA.op_mono_left (◯V b1) ?_
+    apply view_auth_dfrac_included.mpr
+    exact ⟨H0, H1⟩
+
+theorem view_both_includedN : ((●V a1 : View F R) • ◯V b1) ≼{n} ((●V a2) • ◯V b2) ↔ (a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2) :=
+  view_both_dfrac_includedN.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl
+
+theorem view_both_included : ((●V a1 : View F R) • ◯V b1) ≼ ((●V a2) • ◯V b2) ↔ a1 ≡ a2 ∧ b1 ≼ b2 :=
+  view_both_dfrac_included.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl
+
+end cmra
+
+section updates
+
+variable [UFraction F] [OFE A] [IB : UCMRA B] {R : view_rel A B} [ViewRel R]
+
+theorem view_updateP {Pab : A → B → Prop}
+    (Hup : ∀ n bf, R n a (b • bf) → ∃ a' b', Pab a' b' ∧ R n a' (b' • bf)) :
+    ((●V a) • ◯V b : View F R) ~~>: fun k => ∃ a' b', k = ((●V a') • ◯V b' : View F R) ∧ Pab a' b' := by
+  refine UpdateP.total.mpr (fun n ⟨ag, bf⟩ => ?_)
+  rcases ag with (_|⟨dq, ag⟩)
+  · intro H
+    simp [CMRA.op, op, CMRA.ValidN, optionOp, validN] at H
+    obtain ⟨_, a0, He', Hrel'⟩ := H
+    have He := toAgree.inj He'; clear He'
+    have Hrel : R n a (b • bf) := by
+      apply ViewRel.mono Hrel' He.symm _ n.le_refl
+      apply Iris.OFE.Dist.to_incN
+      refine CMRA.comm.dist.trans (.trans ?_ CMRA.comm.dist)
+      refine CMRA.op_ne.ne ?_
+      exact (CMRA.unit_left_id_dist b).symm
+    obtain ⟨a', b', Hab', Hrel''⟩ := Hup _ _ Hrel
+    refine ⟨((●V a') • ◯V b'), ?_, ⟨by trivial, ?_⟩⟩
+    · exists a'; exists b'
+    · refine ⟨a', .rfl, ?_⟩
+      apply ViewRel.mono Hrel'' .rfl _ n.le_refl
+      simp [CMRA.op, op]
+      apply Iris.OFE.Dist.to_incN
+      refine CMRA.comm.dist.trans (.trans ?_ CMRA.comm.dist)
+      refine CMRA.op_ne.ne ?_
+      exact (CMRA.unit_left_id_dist b')
+  · -- FIXME: Why doesn't this synthesize?
+    have _ : CMRA.Exclusive (DFrac.own One.one : DFrac F) := by
+      apply own_whole_exclusive <| UFraction.one_whole
+    exact (CMRA.not_valid_exclN_op_left ·.1 |>.elim)
+
+theorem view_update (Hup : ∀ n bf, R n a (b • bf) → R n a' (b' • bf)) :
+    ((●V a) • ◯V b : View F R) ~~> (●V a') • ◯V b' := by
+  apply Update.of_updateP
+  apply UpdateP.weaken
+  · apply view_updateP (Pab := fun a b => a = a' ∧ b = b')
+    intro _ _ H
+    exact ⟨a', b', ⟨rfl, rfl⟩, Hup _ _ H⟩
+  · rintro y ⟨a', b', H, rfl, rfl⟩; exact H.symm
+
+theorem view_update_alloc (Hup : ∀ n bf, R n a bf → R n a' (b' • bf)) :
+    ((●V a) ~~> ((●V a' : View F R) • ◯V b')) := by
+  refine Update.equiv_left CMRA.unit_right_id ?_
+  refine view_update (fun n bf H => Hup n bf <| ViewRel.mono H .rfl ?_ n.le_refl)
+  exact CMRA.incN_op_right n UCMRA.unit bf
+
+theorem view_update_dealloc (Hup : (∀ n bf, R n a (b • bf) → R n a' bf)) :
+    ((●V a : View F R) • ◯V b) ~~> ●V a' := by
+  refine Update.equiv_right CMRA.unit_right_id ?_
+  refine view_update (fun n bf H => ?_)
+  refine ViewRel.mono (Hup n bf H) .rfl ?_ n.le_refl
+  exact Iris.OFE.Dist.to_incN (CMRA.unit_left_id_dist bf)
+
+theorem view_update_auth (Hup : ∀ n bf, R n a bf → R n a' bf) :
+    (●V a : View F R) ~~> ●V a' := by
+  refine Update.equiv_right CMRA.unit_right_id ?_
+  refine Update.equiv_left  CMRA.unit_right_id ?_
+  refine view_update (fun n bf H => ?_)
+  exact ViewRel.mono (Hup n _ H) .rfl .rfl n.le_refl
+
+theorem view_updateP_auth_dfrac (Hupd : dq ~~>: P) :
+    (●V{dq} a : View F R ) ~~>: (fun k => ∃ dq', (k = ●V{dq'} a) ∧ P dq') := by
+  refine UpdateP.total.mpr (fun n ⟨ag, bf⟩ => ?_)
+  rcases ag with (_|⟨dq', ag⟩) <;> rintro ⟨Hv, a', _, _⟩
+  · obtain ⟨dr, Hdr, Heq⟩ := Hupd n none Hv
+    refine ⟨●V{dr} a, (by exists dr), ⟨Heq, (by exists a')⟩⟩
+  · obtain ⟨dr, Hdr, Heq⟩ := Hupd n (some dq') Hv
+    refine ⟨●V{dr} a, (by exists dr), ⟨Heq, (by exists a')⟩⟩
+
+theorem view_update_auth_persist : (●V{dq} a : View F R) ~~> ●V{.discard} a := by
+  apply Update.lift_updateP (g := fun dq => ●V{dq} a)
+  · intro P
+    apply view_updateP_auth_dfrac
+  · exact dfrac_discard_update
+
+theorem view_updateP_auth_unpersist [IsSplitFraction F] :
+    (●V{.discard} a : View F R) ~~>: fun k => ∃ q, k = ●V{.own q} a := by
+  apply UpdateP.weaken
+  · apply view_updateP_auth_dfrac
+    exact dfrac_undiscard_update
+  · rintro y ⟨dq, rfl, q', rfl⟩
+    exists q'
+
+theorem view_updateP_both_unpersist [IsSplitFraction F] :
+    ((●V{.discard} a : View F R) • ◯V b) ~~>: fun k => ∃ q, k = ((●V{.own q} a : View F R) • ◯V b ):= by
+  apply UpdateP.op
+  apply view_updateP_auth_unpersist
+  apply UpdateP.id rfl
+  rintro z1 z2 ⟨q, rfl⟩ rfl; exists q
+
+theorem view_updateP_frag {P : B → Prop} (Hupd : ∀ a n bf, R n a (b • bf) → ∃ b', P b' ∧ R n a (b' • bf)) :
+    (◯V b : View F R) ~~>: (fun k => ∃ b', (k = (◯V b' : View F R)) ∧ P b') := by
+  refine UpdateP.total.mpr (fun n ⟨ag, bf⟩ => ?_)
+  rcases ag with (_|⟨dq,af⟩)
+  simp only [CMRA.ValidN, validN]
+  · rintro ⟨a, Ha⟩
+    obtain ⟨b', HP, Hb'⟩ := Hupd a n bf Ha
+    exists (◯V b')
+    simp only [mk.injEq, true_and, exists_eq_left']
+    refine ⟨HP, ⟨a, Hb'⟩⟩
+  · rintro ⟨Hq, a, Hae, Hr⟩
+    obtain ⟨b', Hb', Hp⟩ := Hupd a n bf Hr
+    exists (◯V b')
+    simp only [mk.injEq, true_and, exists_eq_left']
+    refine ⟨Hb', ?_⟩
+    simp [CMRA.ValidN, validN, CMRA.op, op, optionOp]
+    refine ⟨Hq, ⟨a, Hae, Hp⟩⟩
+
+theorem view_update_frag (Hupd : ∀ a n bf, R n a (b • bf) → R n a (b' • bf)) :
+    (◯V b : View F R) ~~> (◯V b' : View F R) := by
+  refine Update.total.mpr (fun n ⟨ag, bf⟩ => ?_)
+  rcases ag with (_|⟨dq,af⟩)
+  simp only [CMRA.ValidN, validN]
+  · simp_all [CMRA.op, optionOp]
+    intro a HR
+    exists a
+    apply Hupd _ _ _ HR
+  · simp_all [CMRA.op, op, optionOp, CMRA.ValidN, validN]
+    intro Hq a He Hr
+    exists a
+    exact ⟨He, Hupd _ _ _ Hr⟩
+
+theorem view_update_dfrac_alloc (Hup : ∀ n bf, R n a bf → R n a (b • bf)) :
+    (●V{dq} a : View F R) ~~> ((●V{dq} a) • ◯V b) := by
+  refine Update.total.mpr (fun n ⟨ag', bf⟩ => ?_)
+  obtain (_|⟨p, ag⟩) := ag'
+  · simp [CMRA.op, op, optionOp, CMRA.ValidN, validN]
+    intro Hq a' Hag HR
+    refine ⟨Hq, a', Hag, ?_⟩
+    have He := toAgree.inj Hag
+    have HR' := ViewRel.mono HR He.symm (CMRA.incN_op_right n UCMRA.unit bf) n.le_refl
+    apply ViewRel.mono (Hup n bf HR') He ?_ n.le_refl
+    apply Iris.OFE.Dist.to_incN
+    refine CMRA.comm.dist.trans (.trans ?_ CMRA.comm.dist)
+    refine CMRA.op_ne.ne ?_
+    exact (CMRA.unit_left_id_dist _)
+  · rintro ⟨Hv, a0, Hag, Hrel⟩
+    refine ⟨Hv, ?_⟩
+    simp
+    exists a0
+    refine ⟨Hag, ?_⟩
+    simp_all [CMRA.op, op]
+    have Heq  := toAgree.incN.mp ⟨ag, Hag.symm⟩
+    have HR' := ViewRel.mono Hrel Heq.symm (CMRA.incN_op_right n UCMRA.unit bf) n.le_refl
+    apply ViewRel.mono (Hup _ _ HR') Heq ?_ n.le_refl
+    apply Iris.OFE.Dist.to_incN
+    refine CMRA.comm.dist.trans (.trans ?_ CMRA.comm.dist)
+    refine CMRA.op_ne.ne ?_
+    exact (CMRA.unit_left_id_dist _)
+
+-- TODO: Local update lemma
+
+end updates
+end View