diff --git a/src/Iris/Algebra/CMRA.lean b/src/Iris/Algebra/CMRA.lean
index 4b7fe392..6d7070b7 100644
--- a/src/Iris/Algebra/CMRA.lean
+++ b/src/Iris/Algebra/CMRA.lean
@@ -680,8 +680,8 @@ instance empty_cancelable : Cancelable (unit : α) where
     _ ≡{n}≡ unit • t := e
     _ ≡{n}≡ t := unit_left_id.dist
 
-theorem dst_incN {n} {x y : α} (H : y ≡{n}≡ x) : x ≼{n} y :=
-  ⟨unit, H.trans (equiv_dist.mp unit_right_id n).symm⟩
+theorem _root_.Iris.OFE.Dist.to_incN {n} {x y : α} (H : x ≡{n}≡ y) : x ≼{n} y :=
+  ⟨unit, ((equiv_dist.mp unit_right_id n).trans H).symm⟩
 
 end ucmra
 
diff --git a/src/Iris/Algebra/IProp.lean b/src/Iris/Algebra/IProp.lean
new file mode 100644
index 00000000..dd5b718b
--- /dev/null
+++ b/src/Iris/Algebra/IProp.lean
@@ -0,0 +1,49 @@
+/-
+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.UPred
+import Iris.Algebra.COFESolver
+import Init.Data.Vector
+
+namespace Iris
+
+def GFunctors := Array COFE.OFunctorPre
+
+def GId (FF : GFunctors) : Type _ := Fin FF.size
+
+instance (FF : GFunctors) : GetElem GFunctors (GId FF) COFE.OFunctorPre (fun _ _ => True) where
+  getElem _ x _ := (show Array _ from FF)[x.1]
+
+abbrev IsGFunctors (G : GFunctors) := ∀ (i : GId G), RFunctorContractive G[i]
+
+def SubG (FF₁ FF₂ : GFunctors) : Prop :=
+  ∀ i : GId FF₁, ∃ j : GId FF₂, FF₁[i] = FF₂[j]
+
+def GName := LeibnizO Nat
+
+abbrev IResF (FF : GFunctors) : COFE.OFunctorPre :=
+  DiscreteFunOF (fun i : GId FF => GenMapOF GName FF[i])
+
+section IProp
+open COFE
+
+variable (FF : GFunctors) [IG : IsGFunctors FF]
+
+def iPrePropO : Type _ := OFunctor.Fix (UPredOF (IResF FF))
+
+instance : COFE (iPrePropO FF) := inferInstanceAs (COFE (OFunctor.Fix _))
+
+def IResUR : Type := (i : GId FF) → GName → Option (FF[i] (iPrePropO FF) (iPrePropO FF))
+
+instance : UCMRA (IResUR FF) :=
+  ucmraDiscreteFunO (β := fun (i : GId FF) => GName → Option (FF[i] (iPrePropO FF) (iPrePropO FF)))
+
+abbrev IProp := UPred (IResUR FF)
+
+end IProp
+end Iris
diff --git a/src/Iris/Algebra/UPred.lean b/src/Iris/Algebra/UPred.lean
new file mode 100644
index 00000000..9bb3fdf0
--- /dev/null
+++ b/src/Iris/Algebra/UPred.lean
@@ -0,0 +1,90 @@
+/-
+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
+
+namespace Iris
+open CMRA
+
+/-- The data of a UPred object is an indexed proposition over M (Bundled version) -/
+@[ext]
+structure UPred (M : Type _) [UCMRA M] where
+  holds : Nat → M → Prop
+  mono {n1 n2 x1 x2} : holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → holds n2 x2
+
+instance [UCMRA M] : Inhabited (UPred M) :=
+  ⟨fun _ _ => True, fun _ _ _ => ⟨⟩⟩
+
+instance [UCMRA M] : CoeFun (UPred M) (fun _ => Nat → M → Prop) where
+  coe x := x.holds
+
+section UPred
+
+variable {M : Type} [UCMRA M]
+
+open UPred
+
+instance : OFE (UPred M) where
+  Equiv P Q := ∀ n x, ✓{n} x → (P n x ↔ Q n x)
+  Dist n P Q := ∀ n' x, n' ≤ n → ✓{n'} x → (P n' x ↔ Q n' x)
+  dist_eqv := {
+    refl _ _ _ _ _ := .rfl
+    symm H _ _ A B := (H _ _ A B).symm
+    trans H1 H2 _ _ A B := (H1 _ _ A B).trans (H2 _ _ A B) }
+  equiv_dist := ⟨
+    fun Heqv _ _ _ _ Hvalid => Heqv _ _ Hvalid,
+    fun Hdist _ _ Hvalid => Hdist _ _ _ (Nat.le_refl _) Hvalid⟩
+  dist_lt Hdist Hlt _ _ Hle Hvalid :=
+    Hdist _ _ (Nat.le_trans Hle (Nat.le_of_succ_le Hlt)) Hvalid
+
+theorem uPred_ne {P : UPred M} {n} {m₁ m₂} (H : m₁ ≡{n}≡ m₂) : P n m₁ ↔ P n m₂ :=
+  ⟨fun H' => P.mono H' H.to_incN (Nat.le_refl _),
+   fun H' => P.mono H' H.symm.to_incN (Nat.le_refl _)⟩
+
+theorem uPred_proper {P : UPred M} {n} {m₁ m₂} (H : m₁ ≡ m₂) : P n m₁ ↔ P n m₂ :=
+  uPred_ne H.dist
+
+theorem uPred_holds_ne {P Q : UPred M} {n₁ n₂ x}
+    (HPQ : P ≡{n₂}≡ Q) (Hn : n₂ ≤ n₁) (Hx : ✓{n₂} x) (HQ : Q n₁ x) : P n₂ x :=
+  (HPQ _ _ (Nat.le_refl _) Hx).mpr (Q.mono HQ .rfl Hn)
+
+instance : IsCOFE (UPred M) where
+  compl c := {
+    holds n x := ∀ n', n' ≤ n → ✓{n'} x → (c n') n' x
+    mono {n1 n2 x1 x2 HP Hx12 Hn12 n3 Hn23 Hv} := by
+      refine mono _ ?_ (Hx12.le Hn23) (Nat.le_refl _)
+      exact HP _ (Nat.le_trans Hn23 Hn12) ((Hx12.le Hn23).validN Hv) }
+  conv_compl {n c i x} Hin Hv := by
+    refine .trans ?_ (c.cauchy Hin _ _ (Nat.le_refl _) Hv).symm
+    refine ⟨fun H => H _ (Nat.le_refl _) Hv, fun H n' Hn' Hv' => ?_⟩
+    exact (c.cauchy Hn' _ _ (Nat.le_refl _) Hv').mp (mono _ H .rfl Hn')
+
+abbrev UPredOF (F : COFE.OFunctorPre) [URFunctor F] : COFE.OFunctorPre :=
+  fun A B _ _ => UPred (F B A)
+
+def uPred_map [UCMRA α] [UCMRA β] (f : β -C> α) : UPred α -n> UPred β := by
+  refine ⟨fun P => ⟨fun n x => P n (f x), ?_⟩, ⟨?_⟩⟩
+  · intro n1 n2 x1 x2 HP Hm Hn
+    exact P.mono HP (f.monoN _ Hm) Hn
+  · intro n x1 x2 Hx1x2 n' y Hn' Hv
+    exact Hx1x2 _ _ Hn' (f.validN Hv)
+
+instance [URFunctor F] : COFE.OFunctor (UPredOF F) where
+  cofe := inferInstance
+  map f g := uPred_map (URFunctor.map (F := F) g f)
+  map_ne.ne _ _ _ Hx _ _ Hy _ _ z2 Hn _ :=
+    uPred_ne <| URFunctor.map_ne.ne (Hy.le Hn) (Hx.le Hn) z2
+  map_id _ _ z _ := uPred_proper <| URFunctor.map_id z
+  map_comp f g f' g' _ _ H _ := uPred_proper <| URFunctor.map_comp g' f' g f H
+
+instance [URFunctorContractive F] : COFE.OFunctorContractive (UPredOF F) where
+  map_contractive.1 {_ x y} HKL _ _ _ Hn _ := by
+    refine uPred_ne <| (URFunctorContractive.map_contractive.1
+      (x := (x.snd, x.fst)) (y := (y.snd, y.fst)) ?_ _).le Hn
+    exact fun m Hm => ⟨(HKL m Hm).2, (HKL m Hm).1⟩
+
+end UPred
diff --git a/src/Iris/Examples/Resources.lean b/src/Iris/Examples/Resources.lean
new file mode 100644
index 00000000..434358ef
--- /dev/null
+++ b/src/Iris/Examples/Resources.lean
@@ -0,0 +1,66 @@
+/-
+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.BI
+import Iris.ProofMode
+import Iris.Algebra.IProp
+import Iris.Instances.UPred.Instance
+import Iris.Algebra.Agree
+
+namespace Iris.Examples
+open Iris.BI
+
+section no_resources
+
+abbrev FF0 : GFunctors := #[]
+
+local instance : IsGFunctors FF0 := nofun
+
+-- A proof with no resources
+example (P Q : IProp FF0) : P ∗ Q ⊢ ⌜True⌝ := by
+  iintro ⟨HP, HQ⟩
+  ipure_intro
+  trivial
+
+example (P Q : IProp FF0) : P ∗ Q ⊢ P := by
+  iintro ⟨HP, HQ⟩
+  iexact HP
+
+end no_resources
+
+section const_agree
+
+abbrev FF1 : GFunctors := #[COFE.constOF (Agree (LeibnizO String))]
+abbrev γ : GId FF1 := ⟨0, Nat.zero_lt_succ _⟩
+theorem HγE  (i : GId FF1) : i = γ := by unfold γ; cases i; congr; apply Nat.lt_one_iff.mp; trivial
+theorem HγLookup : FF1[γ] = COFE.constOF (Agree (LeibnizO String)) := rfl
+local instance : IsGFunctors FF1 := fun i => by rw [HγE i, HγLookup]; infer_instance
+
+@[simp]
+def MyAg (S : String) : Agree (LeibnizO String) := ⟨[⟨S⟩], by simp⟩
+
+@[simp]
+def MyR (S : String) : IResUR FF1 := fun i _ => some (HγE i ▸ MyAg S)
+
+theorem MyR_always_invalid (S₁ S₂ : String) (Hne : S₁ ≠ S₂) (n : Nat) : ¬✓{n} MyR S₁ • MyR S₂ := by
+  simp [CMRA.op, CMRA.ValidN]
+  exists γ, ⟨0⟩
+  rw [← HγE ⟨Nat.zero, Nat.le.refl⟩]
+  simp [instIsGFunctorsFF1, CMRA.ValidN, CMRA.op, Agree.op, Agree.validN,
+        instCOFELeibnizO, COFE.ofDiscrete, OFE.ofDiscrete, optionOp, optionValidN]
+  exact fun a => id (Ne.symm Hne)
+
+def AgreeString (S : String) : IProp FF1 := UPred.ownM (MyR S)
+
+example : AgreeString "I <3 iris-lean!" ⊢ (AgreeString "I don't :<" -∗ False) := by
+  iintro H H2
+  istop
+  apply (UPred.ownM_op _ _).2.trans    -- Combine ghost state
+  apply (UPred.ownM_valid _).trans     -- Reduce to invalidity
+  apply UPred.ownM_always_invalid_elim -- The resource is invalid
+  apply MyR_always_invalid; simp       -- Simplify
+
+end const_agree
+end Iris.Examples
diff --git a/src/Iris/Instances/UPred.lean b/src/Iris/Instances/UPred.lean
new file mode 100644
index 00000000..8930d2dc
--- /dev/null
+++ b/src/Iris/Instances/UPred.lean
@@ -0,0 +1 @@
+import Iris.Instances.UPred.Instance
diff --git a/src/Iris/Instances/UPred/Instance.lean b/src/Iris/Instances/UPred/Instance.lean
new file mode 100644
index 00000000..ce72df7a
--- /dev/null
+++ b/src/Iris/Instances/UPred/Instance.lean
@@ -0,0 +1,329 @@
+/-
+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, Mario Carneiro
+-/
+
+import Iris.BI
+import Iris.Algebra.OFE
+import Iris.Algebra.CMRA
+import Iris.Algebra.UPred
+
+section UPredInstance
+
+open Iris BI
+
+namespace UPred
+
+variable {M : Type} [UCMRA M]
+
+section bidefs
+
+variable (P Q : UPred M)
+variable {A : Type}
+variable {O : Type} [OFE O] (o1 o2 : O)
+variable (m : M)
+
+protected def Entails : Prop := ∀ n x, ✓{n} x → P n x → Q n x
+
+protected def pure (p : Prop) : UPred M where
+  holds _ _ := p
+  mono h _ _ := h
+
+protected def and : UPred M where
+  holds n x := P n x ∧ Q n x
+  mono HPQ Hle Hn := ⟨P.mono HPQ.1 Hle Hn, Q.mono HPQ.2 Hle Hn⟩
+
+protected def or : UPred M where
+  holds n x := P n x ∨ Q n x
+  mono
+  | .inl H, Hle, Hn => .inl (P.mono H Hle Hn)
+  | .inr H, Hle, Hn => .inr (Q.mono H Hle Hn)
+
+protected def imp : UPred M where
+  holds n x := ∀ n' x', x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x'
+  mono {n₁ n₂ x₁ x₂} H := fun ⟨m₁, Hle⟩ Hn n x ⟨m₂, Hxle⟩ Hnle Hv HP => by
+    have Hx :=
+      calc x ≡{n}≡ x₂ • m₂        := Hxle.dist
+           _ ≡{n}≡ (x₁ • m₁) • m₂ := (Hle.le Hnle).op_l
+    refine (uPred_ne Hx).mpr (H _ _ ?_ ?_ ?_ ?_)
+    · calc x₁ ≡ x₁ • UCMRA.unit  := CMRA.unit_right_id.symm
+           _  ≼ x₁ • (m₁ • m₂)   := CMRA.op_mono_right _ CMRA.inc_unit
+           _  ≡ (x₁ • m₁) • m₂   := CMRA.assoc
+    · exact Nat.le_trans Hnle Hn
+    · exact Hx.validN.mp Hv
+    · exact (uPred_ne Hx).mp HP
+
+protected def sForall (Ψ : UPred M → Prop) : UPred M where
+  holds n x := ∀ p, Ψ p → p n x
+  mono a a_1 a_2 p a_3 := p.mono (a p a_3) a_1 a_2
+
+protected def sExists (Ψ : UPred M → Prop) : UPred M where
+  holds n x := ∃ p, Ψ p ∧ p n x
+  mono := fun ⟨p, HΨ, Hp⟩ Hv Hn => ⟨p, HΨ, p.mono Hp Hv Hn⟩
+
+protected def eq : UPred M where
+  holds n _ := o1 ≡{n}≡ o2
+  mono H1 _ H2 := H1.le H2
+
+protected def sep : UPred M where
+  holds n x := ∃ x1 x2, x ≡{n}≡ x1 • x2 ∧ P n x1 ∧ Q n x2
+  mono {n₁ n₂ m₁ m₂} := fun ⟨x₁, x₂, Hx, HP, HQ⟩ ⟨m, Hm⟩ Hn => by
+    refine ⟨x₁, x₂ • m, ?_, ?_, ?_⟩
+    · calc m₂ ≡{n₂}≡ m₁ • m := Hm
+           _  ≡{n₂}≡ (x₁ • x₂) • m := (Hx.le Hn).op_l
+           _  ≡{n₂}≡ x₁ • (x₂ • m) := CMRA.assoc.symm.dist
+    · exact P.mono HP (CMRA.incN_refl x₁) Hn
+    · exact Q.mono HQ (CMRA.incN_op_left n₂ x₂ m) Hn
+
+protected def wand : UPred M where
+  holds n x := ∀ n' x', n' ≤ n → ✓{n'} (x • x') → P n' x' → Q n' (x • x')
+  mono {n₁ n₂ m₁ m₂} H Hm Hn n' x Hn' Hv HP := by
+    refine Q.mono ?_ (CMRA.op_monoN_left _ (CMRA.incN_of_incN_le Hn' Hm)) (Nat.le_refl _)
+    let ⟨y, Hx⟩ := Hm
+    refine H _ _ (Nat.le_trans Hn' Hn) ?_ HP
+    refine CMRA.validN_of_incN ⟨y, OFE.Dist.le ?_ Hn'⟩ Hv
+    calc m₂ • x ≡{n₂}≡ (m₁ • y) • x := Hx.op_l
+         _      ≡{n₂}≡ m₁ • (y • x) := CMRA.assoc.symm.dist
+         _      ≡{n₂}≡ m₁ • (x • y) := CMRA.comm.dist.op_r
+         _      ≡{n₂}≡ (m₁ • x) • y := CMRA.assoc.dist
+
+protected def plainly : UPred M where
+  holds n _ := P n UCMRA.unit
+  mono H _ Hn := P.mono H (CMRA.incN_refl UCMRA.unit) Hn
+
+protected def persistently : UPred M where
+  holds n x := P n (CMRA.core x)
+  mono H Hx Hn := P.mono H (CMRA.core_incN_core Hx) Hn
+
+protected def later : UPred M where
+  holds n x := match n with | 0 => True | Nat.succ n' => P n' x
+  mono {n₁ n₂} := by
+    cases n₁ <;> cases n₂ <;> simp
+    exact fun H Hx Hn => P.mono H (CMRA.incN_of_incN_succ Hx) Hn
+
+def ownM : UPred M where
+  holds n x := m ≼{n} x
+  mono {n₁ n₂ x₁ x₂} := fun ⟨m₁, Hm₁⟩ ⟨m₂, Hm₂⟩ Hn => by
+    exists m₁ • m₂
+    calc x₂ ≡{n₂}≡ x₁ • m₂ := Hm₂
+         _  ≡{n₂}≡ (m • m₁) • m₂ := (Hm₁.le Hn).op_l
+         _  ≡{n₂}≡ m • (m₁ • m₂) := CMRA.assoc.symm.dist
+
+def cmraValid : UPred M where
+  holds n _ := ✓{n} m
+  mono hv _ le := CMRA.validN_of_le le hv
+
+/-
+def bupd : UPred M where
+  holds n x := ∀ k yf, k ≤ n → ✓{k} (x • yf) → ∃ x', ✓{k} (x' • yf) ∧ Q k x'
+  mono := sorry
+-/
+
+protected def emp : UPred M where
+  holds _ _ := True
+  mono _ _ _ := trivial
+
+end bidefs
+
+instance : BIBase (UPred M) where
+  Entails      := UPred.Entails
+  emp          := UPred.emp
+  pure         := UPred.pure
+  and          := UPred.and
+  or           := UPred.or
+  imp          := UPred.imp
+  sForall      := UPred.sForall
+  sExists      := UPred.sExists
+  sep          := UPred.sep
+  wand         := UPred.wand
+  persistently := UPred.persistently
+  later        := UPred.later
+
+instance uPred_entails_preorder : Std.Preorder (Entails (PROP := UPred M)) where
+  refl _ _ _ H := H
+  trans H1 H2 _ _ Hv H := H2 _ _ Hv <| H1 _ _ Hv H
+
+instance later_contractive : OFE.Contractive UPred.later (α := UPred M) where
+  distLater_dist {n x y} Hl :=
+    match n with
+    | 0 => by intro; simp_all [UPred.later]
+    | n + 1 => fun
+      | 0 => by simp [UPred.later]
+      | n' + 1 => fun x' Hn' Hx' => Hl _ Hn' _ _ (Nat.le_refl _) (CMRA.validN_succ Hx')
+
+instance : BI (UPred M) where
+  entails_preorder := inferInstance
+  equiv_iff {P Q} := by
+    constructor <;> intro HE
+    · constructor <;> intro n x Hv H <;> apply uPred_holds_ne _ (Nat.le_refl n) Hv H
+      · exact fun n' x a => HE.symm n' x
+      · exact fun n' x a => HE n' x
+    · intro n m Hv
+      exact ⟨fun H => HE.1 _ _ Hv H, fun H => HE.2 _ _ Hv H⟩
+  and_ne.ne _ _ _ H _ _ H' _ _ Hn' Hv' := by
+    constructor <;> intro H <;> rcases H with ⟨H1, H2⟩
+    · constructor
+      · exact (H _ _ Hn' Hv').mp H1
+      · exact (H' _ _ Hn' Hv').mp H2
+    · constructor
+      · exact (H.symm _ _ Hn' Hv').mp H1
+      · exact (H'.symm _ _ Hn' Hv').mp H2
+  or_ne.ne _ _ _ H _ _ H' _ _ Hn' Hv := by
+    constructor <;> intro H'' <;>  rcases H'' with H'' | H''
+    · left; exact (H _ _ Hn' Hv).mp H''
+    · right; exact (H' _ _ Hn' Hv).mp H''
+    · left; exact (H.symm _ _ Hn' Hv).mp H''
+    · right; exact (H'.symm _ _ Hn' Hv).mp H''
+  imp_ne.ne _ _ _ H _ _ H' _ _ Hn' Hv := by
+    constructor <;> intro Hi n' x' Hle Hn'' Hx' H''
+    · refine (H' _ _ (Nat.le_trans Hn'' Hn') Hx').mp ?_
+      refine Hi _ _ Hle Hn'' Hx' ?_
+      exact (H _ _ (Nat.le_trans Hn'' Hn') Hx').mpr H''
+    · refine (H' _ _ (Nat.le_trans Hn'' Hn') Hx').mpr ?_
+      refine Hi _ _ Hle Hn'' Hx' ?_
+      exact (H _ _ (Nat.le_trans Hn'' Hn') Hx').mp H''
+  sep_ne.ne _ _ _ H _ _ H' x n' Hn' Hv := by
+    constructor <;> intro Hi <;> rcases Hi with ⟨z1, z2, H1, H2, H3⟩
+    · refine ⟨z1, z2, H1, (H _ _ Hn' ?_).mp H2, (H' _ _ Hn' ?_).mp H3⟩
+      · exact CMRA.validN_op_right ((H1.trans CMRA.op_commN).validN.1 Hv)
+      · exact CMRA.validN_op_right (H1.validN.1 Hv)
+    · refine ⟨z1, z2, H1, (H _ _ Hn' ?_).mpr H2, (H' _ _ Hn' ?_).mpr H3⟩
+      · exact CMRA.validN_op_right ((H1.trans CMRA.op_commN).validN.1 Hv)
+      · exact CMRA.validN_op_right (H1.validN.1 Hv)
+  wand_ne.ne _ _ _ H _ _ H' _ _ Hn' Hv := by
+    constructor <;> intro HE n x Hn Hv H''
+    · refine (H' _ _ (Nat.le_trans Hn Hn') Hv).mp ?_
+      refine HE _ _ Hn Hv ?_
+      exact (H _ _ (Nat.le_trans Hn Hn') (CMRA.validN_op_right Hv)).mpr H''
+    · refine (H' _ _ (Nat.le_trans Hn Hn') Hv).mpr ?_
+      refine HE _ _ Hn Hv ?_
+      exact (H _ _ (Nat.le_trans Hn Hn') (CMRA.validN_op_right Hv)).mp H''
+  persistently_ne.ne _ _ _ H _ _ Hn Hx := H _ _ Hn (CMRA.validN_core Hx)
+  later_ne := inferInstanceAs (OFE.NonExpansive UPred.later)
+  sForall_ne := fun ⟨HR1, HR2⟩ n' x' Hn' Hx' => by
+    constructor
+    · intro H p Hp
+      let ⟨p', Hp', Hp'eq⟩ := HR2 p Hp
+      exact (Hp'eq n' _ Hn' Hx').mp (H _ Hp')
+    · intro H p Hp
+      let ⟨p', Hp', Hp'eq⟩ := HR1 p Hp
+      exact (Hp'eq n' _ Hn' Hx').mpr (H _ Hp')
+  sExists_ne := fun ⟨HR1, HR2⟩ n' x' Hn' Hx' => by
+    constructor <;> rintro ⟨p, Hp, H⟩
+    · let ⟨p', Hp', Hp'eq⟩ := HR1 p Hp
+      exact ⟨p', Hp', (Hp'eq n' _ Hn' Hx').mp H⟩
+    · let ⟨p', Hp', Hp'eq⟩ := HR2 p Hp
+      exact ⟨p', Hp', (Hp'eq n' _ Hn' Hx').mpr H⟩
+  pure_intro P _ _ _ _ := P
+  pure_elim' I n x a P := I P n x a trivial
+  and_elim_l _ _ _ I := I.1
+  and_elim_r _ _ _ I := I.2
+  and_intro H1 H2 _ _ Hv H := ⟨H1 _ _ Hv H, H2 _ _ Hv H⟩
+  or_intro_l _ _ Hv H := .inl H
+  or_intro_r _ _ Hv H := .inr H
+  or_elim H1 H2 _ _ Hv := fun
+    | .inl H => H1 _ _ Hv H
+    | .inr H => H2 _ _ Hv H
+  imp_intro I _ _ Hv H _ _ Hin Hle Hv' HQ :=
+    I _ _ Hv' ⟨UPred.mono _ H Hin.incN Hle, HQ⟩
+  imp_elim H' _ _ Hv := fun ⟨HP, HQ⟩ =>
+    H' _ _ Hv HP _ _ (CMRA.inc_refl _) (Nat.le_refl _) Hv HQ
+  sForall_intro H n x Hv Hp p' HΨ := H _ HΨ _ _ Hv Hp
+  sForall_elim HΨ _ _ _ H := H _ HΨ
+  sExists_intro H _ _ _ Hp := ⟨_, H, Hp⟩
+  sExists_elim H _ _ Hv := fun ⟨_, HΨ, H'⟩ => H _ HΨ _ _ Hv H'
+  sep_mono H1 H2 n x Hv := fun ⟨x1, x2, HE, Hx1, Hx2⟩ => by
+    refine ⟨x1, x2, HE, H1 _ _ ?_ Hx1, H2 _ _ ?_ Hx2⟩
+    · exact CMRA.validN_op_left (HE.validN.1 Hv)
+    · exact CMRA.validN_op_right (HE.validN.1 Hv)
+  emp_sep {P} := by
+    constructor
+    · intro _ _ _ ⟨x1, x2, HE1, _, HE2⟩
+      exact P.mono HE2 ⟨x1, HE1.trans CMRA.op_commN⟩ (Nat.le_refl _)
+    · intro _ x _ H
+      exact ⟨_, _, UCMRA.unit_left_id.symm.dist, ⟨⟩, H⟩
+  sep_symm _ _ Hv := fun ⟨x1, x2, HE, HP, HQ⟩ => by
+    refine ⟨x2, x1, ?_, HQ, HP⟩
+    exact HE.trans CMRA.comm.dist
+  sep_assoc_l n x Hv := fun ⟨x1, x2, Hx, ⟨y1, y2, Hy, h1, h2⟩, h3⟩ => by
+    refine ⟨y1, y2 • x2, ?_, h1, y2, x2, .rfl, h2, h3⟩
+    calc x ≡{n}≡ x1 • x2 := Hx
+         _ ≡{n}≡ (y1 • y2) • x2 := Hy.op_l
+         _ ≡{n}≡ y1 • (y2 • x2) := CMRA.assoc.symm.dist
+  wand_intro H n x Hv HP n' x' Hn Hv' HQ :=
+    H _ _ Hv' ⟨x, x', .rfl, UPred.mono _ HP .rfl Hn, HQ⟩
+  wand_elim H n x Hv := fun ⟨y1, y2, Hy, HP, HQ⟩ => by
+    refine UPred.mono _ ?_ Hy.symm.to_incN (Nat.le_refl _)
+    have Hv := Hy.validN.1 Hv
+    exact H n y1 (CMRA.validN_op_left Hv) HP _ y2 (Nat.le_refl _) Hv HQ
+  persistently_mono H n x Hv H' := H _ _ (CMRA.validN_core Hv) H'
+  persistently_idem_2 {P} _ x n H := by
+    refine P.mono H ?_ (Nat.le_refl _)
+    refine (CMRA.incN_iff_right ?_).mpr (CMRA.incN_refl _)
+    exact (CMRA.core_idem x).dist
+  persistently_emp_2 := Std.refl
+  persistently_and_2 := Std.refl
+  persistently_sExists_1 n x v := fun ⟨p, HΨ, H⟩ => by
+    refine ⟨iprop(<pers> p), ⟨p, ?_⟩, H⟩
+    ext; exact and_iff_right HΨ
+  persistently_absorb_l {P Q} _ x _ := fun ⟨x1, x2, H1, H2, H3⟩ =>
+    P.mono H2 (CMRA.core_incN_core ⟨x2, H1⟩) (Nat.le_refl _)
+  persistently_and_l _ x _ H := ⟨CMRA.core x, x, (CMRA.core_op _).symm.dist, H⟩
+  later_mono H := fun
+    | 0, _, _ => id
+    | n+1, _, Hv => H _ _ (CMRA.validN_succ Hv)
+  later_intro {P} := fun
+    | 0, _, _, _ => trivial
+    | n+1, _, _, Hp => P.mono Hp (CMRA.incN_refl _) (Nat.le_add_right ..)
+  later_sForall_2 {Ψ} := fun
+    | 0, _, _, _ => trivial
+    | n+1, _, Hx, H => fun _ => H _ ⟨_, rfl⟩ _ _ (CMRA.inc_refl _) (Nat.le_refl _) Hx
+  later_sExists_false := fun
+    | 0, _, _, _ => .inl trivial
+    | n+1, x, Hx, ⟨p', Hp', H⟩ => by
+      refine .inr ⟨later p', ⟨p', ?_⟩, H⟩
+      ext n x; exact and_iff_right Hp'
+  later_sep {P Q} := by
+    constructor <;> rintro (_ | n) x Hv H
+    · exact ⟨UCMRA.unit, x, UCMRA.unit_left_id.dist.symm, trivial, trivial⟩
+    · let ⟨x1, x2, H1, H2, H3⟩ := H
+      let ⟨y1, y2, H1', H2', H3'⟩ := CMRA.extend (CMRA.validN_succ Hv) H1
+      exact ⟨y1, y2, H1'.dist, (uPred_ne H2').mpr H2, (uPred_ne H3').mpr H3⟩
+    · trivial
+    · let ⟨x1, x2, H1, H2, H3⟩ := H
+      exact ⟨x1, x2, H1.lt (Nat.lt_add_one _), H2, H3⟩
+  later_persistently := ⟨Std.refl, Std.refl⟩
+  later_false_em {P} := fun
+    | 0, _, _, _ => .inl trivial
+    | n+1, x, Hv, H => .inr fun
+      | 0, x', Hx'le, Hn', Hv', _ => P.mono H Hx'le.incN (Nat.zero_le _)
+
+instance : BILaterContractive (UPred M) where
+  toContractive := later_contractive
+
+instance (P : UPred M) : Affine P where
+  affine _ := by simp [emp, UPred.emp]
+
+theorem ownM_valid (m : M) : ownM m ⊢ cmraValid m := fun _ _ h hp => hp.validN h
+
+theorem ownM_op (m1 m2 : M) : ownM (m1 • m2) ⊣⊢ ownM m1 ∗ ownM m2 := by
+  constructor
+  · intro n x Hv ⟨z, Hz⟩
+    refine ⟨m1, m2 • z, ?_, .rfl, CMRA.incN_op_left n m2 z⟩
+    exact Hz.trans CMRA.assoc.symm.dist
+  · intro n x Hv ⟨y1, y2, H, ⟨w1, Hw1⟩, ⟨w2, Hw2⟩⟩
+    exists w1 • w2
+    calc
+      x ≡{n}≡ y1 • y2 := H
+      _ ≡{n}≡ (m1 • w1) • (m2 • w2) := Hw1.op Hw2
+      _ ≡{n}≡ m1 • (w1 • (m2 • w2)) := CMRA.assoc.symm.dist
+      _ ≡{n}≡ m1 • ((m2 • w2) • w1) := CMRA.comm.op_r.dist
+      _ ≡{n}≡ m1 • (m2 • (w2 • w1)) := CMRA.assoc.symm.op_r.dist
+      _ ≡{n}≡ (m1 • m2) • (w2 • w1) := CMRA.assoc.dist
+      _ ≡{n}≡ (m1 • m2) • (w1 • w2) := CMRA.comm.op_r.dist
+
+theorem ownM_always_invalid_elim (m : M) (H : ∀ n, ¬✓{n} m) : cmraValid m ⊢ False :=
+  fun n _ _ => H n
+
+end UPred