From fc3ac14835cba3cc39e751b14e08268b2099fd60 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 21 Oct 2016 21:56:06 +0200
Subject: [PATCH] Move base_logic stuff to its own folder: base_logic.

---
 _CoqProject                                   |   14 +-
 algebra/agree.v                               |    2 +-
 algebra/auth.v                                |    2 +-
 algebra/csum.v                                |    3 +-
 algebra/excl.v                                |    2 +-
 algebra/gmap.v                                |    3 +-
 algebra/iprod.v                               |    4 +-
 algebra/list.v                                |    3 +-
 algebra/upred.v                               | 1599 -----------------
 base_logic/base_logic.v                       |   17 +
 algebra/upred_big_op.v => base_logic/big_op.v |   84 +-
 base_logic/derived.v                          |  751 ++++++++
 {algebra => base_logic}/double_negation.v     |    2 +-
 algebra/upred_hlist.v => base_logic/hlist.v   |    2 +-
 base_logic/primitive.v                        |  592 ++++++
 base_logic/soundness.v                        |   24 +
 .../upred_tactics.v => base_logic/tactics.v   |    3 +-
 base_logic/upred.v                            |  172 ++
 heap_lang/lib/barrier/proof.v                 |    2 +-
 program_logic/adequacy.v                      |    9 +-
 program_logic/auth.v                          |    1 +
 program_logic/boxes.v                         |    3 +-
 program_logic/counter_examples.v              |    4 +-
 program_logic/fancy_updates.v                 |    3 +-
 program_logic/ghost_ownership.v               |    1 +
 program_logic/iris.v                          |    2 +-
 program_logic/lifting.v                       |    2 +-
 program_logic/model.v                         |    2 +-
 program_logic/weakestpre.v                    |    2 +-
 program_logic/wsat.v                          |    3 +-
 proofmode/class_instances.v                   |    3 +-
 proofmode/classes.v                           |    2 +-
 proofmode/coq_tactics.v                       |    4 +-
 proofmode/tactics.v                           |    2 +-
 tests/atomic.v                                |    2 +-
 35 files changed, 1689 insertions(+), 1637 deletions(-)
 delete mode 100644 algebra/upred.v
 create mode 100644 base_logic/base_logic.v
 rename algebra/upred_big_op.v => base_logic/big_op.v (85%)
 create mode 100644 base_logic/derived.v
 rename {algebra => base_logic}/double_negation.v (99%)
 rename algebra/upred_hlist.v => base_logic/hlist.v (96%)
 create mode 100644 base_logic/primitive.v
 create mode 100644 base_logic/soundness.v
 rename algebra/upred_tactics.v => base_logic/tactics.v (98%)
 create mode 100644 base_logic/upred.v

diff --git a/_CoqProject b/_CoqProject
index 5d4efbcb4..54d3925c6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -51,10 +51,6 @@ algebra/agree.v
 algebra/dec_agree.v
 algebra/excl.v
 algebra/iprod.v
-algebra/upred.v
-algebra/upred_tactics.v
-algebra/upred_big_op.v
-algebra/upred_hlist.v
 algebra/frac.v
 algebra/csum.v
 algebra/list.v
@@ -62,7 +58,15 @@ algebra/updates.v
 algebra/local_updates.v
 algebra/gset.v
 algebra/coPset.v
-algebra/double_negation.v
+base_logic/upred.v
+base_logic/primitive.v
+base_logic/derived.v
+base_logic/base_logic.v
+base_logic/tactics.v
+base_logic/big_op.v
+base_logic/hlist.v
+base_logic/soundness.v
+base_logic/double_negation.v
 program_logic/model.v
 program_logic/adequacy.v
 program_logic/lifting.v
diff --git a/algebra/agree.v b/algebra/agree.v
index e138d0368..35283796a 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import upred.
+From iris.base_logic Require Import base_logic.
 Local Hint Extern 10 (_ â‰¤ _) => omega.
 
 Record agree (A : Type) : Type := Agree {
diff --git a/algebra/auth.v b/algebra/auth.v
index 94b0cabf3..c9ba5b776 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export excl local_updates.
-From iris.algebra Require Import upred updates.
+From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import class_instances.
 Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
diff --git a/algebra/csum.v b/algebra/csum.v
index 27066a1d8..954fdabf5 100644
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import upred updates local_updates.
+From iris.base_logic Require Import base_logic.
+From iris.algebra Require Import local_updates.
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.
 Local Arguments validN _ _ _ !_ /.
diff --git a/algebra/excl.v b/algebra/excl.v
index bd1bc8612..4c0200eaa 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import upred.
+From iris.base_logic Require Import base_logic.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 42f430f56..5af9911a0 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.prelude Require Export gmap.
-From iris.algebra Require Import upred updates local_updates.
+From iris.algebra Require Import updates local_updates.
+From iris.base_logic Require Import base_logic.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index d2870d53f..317484fbe 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Export cmra updates.
-From iris.algebra Require Import upred.
+From iris.algebra Require Export cmra.
+From iris.base_logic Require Import base_logic.
 From iris.prelude Require Import finite.
 
 (** * Indexed product *)
diff --git a/algebra/list.v b/algebra/list.v
index c9bd4bfcf..5d67d4f74 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.prelude Require Export list.
-From iris.algebra Require Import upred updates local_updates.
+From iris.base_logic Require Import base_logic.
+From iris.algebra Require Import updates local_updates.
 
 Section cofe.
 Context {A : cofeT}.
diff --git a/algebra/upred.v b/algebra/upred.v
deleted file mode 100644
index c4b6e5da4..000000000
--- a/algebra/upred.v
+++ /dev/null
@@ -1,1599 +0,0 @@
-From iris.algebra Require Export cmra updates.
-Local Hint Extern 1 (_ â‰¼ _) => etrans; [eassumption|].
-Local Hint Extern 1 (_ â‰¼ _) => etrans; [|eassumption].
-Local Hint Extern 10 (_ â‰¤ _) => omega.
-
-Record uPred (M : ucmraT) : Type := IProp {
-  uPred_holds :> nat â†’ M â†’ Prop;
-  uPred_mono n x1 x2 : uPred_holds n x1 â†’ x1 â‰¼{n} x2 â†’ uPred_holds n x2;
-  uPred_closed n1 n2 x : uPred_holds n1 x â†’ n2 â‰¤ n1 â†’ âœ“{n2} x â†’ uPred_holds n2 x
-}.
-Arguments uPred_holds {_} _ _ _ : simpl never.
-Add Printing Constructor uPred.
-Instance: Params (@uPred_holds) 3.
-
-Delimit Scope uPred_scope with I.
-Bind Scope uPred_scope with uPred.
-Arguments uPred_holds {_} _%I _ _.
-
-Section cofe.
-  Context {M : ucmraT}.
-
-  Inductive uPred_equiv' (P Q : uPred M) : Prop :=
-    { uPred_in_equiv : âˆ€ n x, âœ“{n} x â†’ P n x â†” Q n x }.
-  Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
-  Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
-    { uPred_in_dist : âˆ€ n' x, n' â‰¤ n â†’ âœ“{n'} x â†’ P n' x â†” Q n' x }.
-  Instance uPred_dist : Dist (uPred M) := uPred_dist'.
-  Program Instance uPred_compl : Compl (uPred M) := Î» c,
-    {| uPred_holds n x := c n n x |}.
-  Next Obligation. naive_solver eauto using uPred_mono. Qed.
-  Next Obligation.
-    intros c n1 n2 x ???; simpl in *.
-    apply (chain_cauchy c n2 n1); eauto using uPred_closed.
-  Qed.
-  Definition uPred_cofe_mixin : CofeMixin (uPred M).
-  Proof.
-    split.
-    - intros P Q; split.
-      + by intros HPQ n; split=> i x ??; apply HPQ.
-      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
-    - intros n; split.
-      + by intros P; split=> x i.
-      + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
-      + intros P Q Q' HP HQ; split=> i x ??.
-        by trans (Q i x);[apply HP|apply HQ].
-    - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
-    - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
-  Qed.
-  Canonical Structure uPredC : cofeT := CofeT (uPred M) uPred_cofe_mixin.
-End cofe.
-Arguments uPredC : clear implicits.
-
-Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
-Proof.
-  intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx.
-Qed.
-Instance uPred_proper {M} (P : uPred M) n : Proper ((â‰¡) ==> iff) (P n).
-Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.
-
-Lemma uPred_holds_ne {M} (P Q : uPred M) n1 n2 x :
-  P â‰¡{n2}â‰¡ Q â†’ n2 â‰¤ n1 â†’ âœ“{n2} x â†’ Q n1 x â†’ P n2 x.
-Proof.
-  intros [Hne] ???. eapply Hne; try done.
-  eapply uPred_closed; eauto using cmra_validN_le.
-Qed.
-
-(** functor *)
-Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
-  `{!CMRAMonotone f} (P : uPred M1) :
-  uPred M2 := {| uPred_holds n x := P n (f x) |}.
-Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
-Next Obligation. naive_solver eauto using uPred_closed, cmra_monotone_validN. Qed.
-
-Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
-  `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
-Proof.
-  intros x1 x2 Hx; split=> n' y ??.
-  split; apply Hx; auto using cmra_monotone_validN.
-Qed.
-Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P â‰¡ P.
-Proof. by split=> n x ?. Qed.
-Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3)
-    `{!CMRAMonotone f, !CMRAMonotone g} (P : uPred M3):
-  uPred_map (g â—Ž f) P â‰¡ uPred_map f (uPred_map g P).
-Proof. by split=> n x Hx. Qed.
-Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2)
-      `{!CMRAMonotone f} `{!CMRAMonotone g}:
-  (âˆ€ x, f x â‰¡ g x) â†’ âˆ€ x, uPred_map f x â‰¡ uPred_map g x.
-Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
-Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
-  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 â†’ uPredC M2).
-Lemma uPredC_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
-    `{!CMRAMonotone f, !CMRAMonotone g} n :
-  f â‰¡{n}â‰¡ g â†’ uPredC_map f â‰¡{n}â‰¡ uPredC_map g.
-Proof.
-  by intros Hfg P; split=> n' y ??;
-    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
-Qed.
-
-Program Definition uPredCF (F : urFunctor) : cFunctor := {|
-  cFunctor_car A B := uPredC (urFunctor_car F B A);
-  cFunctor_map A1 A2 B1 B2 fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
-|}.
-Next Obligation.
-  intros F A1 A2 B1 B2 n P Q HPQ.
-  apply uPredC_map_ne, urFunctor_ne; split; by apply HPQ.
-Qed.
-Next Obligation.
-  intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
-  apply uPred_map_ext=>y. by rewrite urFunctor_id.
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' P; simpl. rewrite -uPred_map_compose.
-  apply uPred_map_ext=>y; apply urFunctor_compose.
-Qed.
-
-Instance uPredCF_contractive F :
-  urFunctorContractive F â†’ cFunctorContractive (uPredCF F).
-Proof.
-  intros ? A1 A2 B1 B2 n P Q HPQ.
-  apply uPredC_map_ne, urFunctor_contractive=> i ?; split; by apply HPQ.
-Qed.
-
-(** logical entailement *)
-Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
-  { uPred_in_entails : âˆ€ n x, âœ“{n} x â†’ P n x â†’ Q n x }.
-Hint Extern 0 (uPred_entails _ _) => reflexivity.
-Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
-
-Hint Resolve uPred_mono uPred_closed : uPred_def.
-
-(** logical connectives *)
-Program Definition uPred_pure_def {M} (Ï† : Prop) : uPred M :=
-  {| uPred_holds n x := Ï† |}.
-Solve Obligations with done.
-Definition uPred_pure_aux : { x | x = @uPred_pure_def }. by eexists. Qed.
-Definition uPred_pure {M} := proj1_sig uPred_pure_aux M.
-Definition uPred_pure_eq :
-  @uPred_pure = @uPred_pure_def := proj2_sig uPred_pure_aux.
-
-Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_pure True).
-
-Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := P n x âˆ§ Q n x |}.
-Solve Obligations with naive_solver eauto 2 with uPred_def.
-Definition uPred_and_aux : { x | x = @uPred_and_def }. by eexists. Qed.
-Definition uPred_and {M} := proj1_sig uPred_and_aux M.
-Definition uPred_and_eq: @uPred_and = @uPred_and_def := proj2_sig uPred_and_aux.
-
-Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := P n x âˆ¨ Q n x |}.
-Solve Obligations with naive_solver eauto 2 with uPred_def.
-Definition uPred_or_aux : { x | x = @uPred_or_def }. by eexists. Qed.
-Definition uPred_or {M} := proj1_sig uPred_or_aux M.
-Definition uPred_or_eq: @uPred_or = @uPred_or_def := proj2_sig uPred_or_aux.
-
-Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := âˆ€ n' x',
-       x â‰¼ x' â†’ n' â‰¤ n â†’ âœ“{n'} x' â†’ P n' x' â†’ Q n' x' |}.
-Next Obligation.
-  intros M P Q n1 x1 x1' HPQ [x2 Hx1'] n2 x3 [x4 Hx3] ?; simpl in *.
-  rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
-  eapply HPQ; auto. exists (x2 â‹… x4); by rewrite assoc.
-Qed.
-Next Obligation. intros M P Q [|n1] [|n2] x; auto with lia. Qed.
-Definition uPred_impl_aux : { x | x = @uPred_impl_def }. by eexists. Qed.
-Definition uPred_impl {M} := proj1_sig uPred_impl_aux M.
-Definition uPred_impl_eq :
-  @uPred_impl = @uPred_impl_def := proj2_sig uPred_impl_aux.
-
-Program Definition uPred_forall_def {M A} (Î¨ : A â†’ uPred M) : uPred M :=
-  {| uPred_holds n x := âˆ€ a, Î¨ a n x |}.
-Solve Obligations with naive_solver eauto 2 with uPred_def.
-Definition uPred_forall_aux : { x | x = @uPred_forall_def }. by eexists. Qed.
-Definition uPred_forall {M A} := proj1_sig uPred_forall_aux M A.
-Definition uPred_forall_eq :
-  @uPred_forall = @uPred_forall_def := proj2_sig uPred_forall_aux.
-
-Program Definition uPred_exist_def {M A} (Î¨ : A â†’ uPred M) : uPred M :=
-  {| uPred_holds n x := âˆƒ a, Î¨ a n x |}.
-Solve Obligations with naive_solver eauto 2 with uPred_def.
-Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed.
-Definition uPred_exist {M A} := proj1_sig uPred_exist_aux M A.
-Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := proj2_sig uPred_exist_aux.
-
-Program Definition uPred_eq_def {M} {A : cofeT} (a1 a2 : A) : uPred M :=
-  {| uPred_holds n x := a1 â‰¡{n}â‰¡ a2 |}.
-Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
-Definition uPred_eq_aux : { x | x = @uPred_eq_def }. by eexists. Qed.
-Definition uPred_eq {M A} := proj1_sig uPred_eq_aux M A.
-Definition uPred_eq_eq: @uPred_eq = @uPred_eq_def := proj2_sig uPred_eq_aux.
-
-Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := âˆƒ x1 x2, x â‰¡{n}â‰¡ x1 â‹… x2 âˆ§ P n x1 âˆ§ Q n x2 |}.
-Next Obligation.
-  intros M P Q n x y (x1&x2&Hx&?&?) [z Hy].
-  exists x1, (x2 â‹… z); split_and?; eauto using uPred_mono, cmra_includedN_l.
-  by rewrite Hy Hx assoc.
-Qed.
-Next Obligation.
-  intros M P Q n1 n2 x (x1&x2&Hx&?&?) ?; rewrite {1}(dist_le _ _ _ _ Hx) // =>?.
-  exists x1, x2; cofe_subst; split_and!;
-    eauto using dist_le, uPred_closed, cmra_validN_op_l, cmra_validN_op_r.
-Qed.
-Definition uPred_sep_aux : { x | x = @uPred_sep_def }. by eexists. Qed.
-Definition uPred_sep {M} := proj1_sig uPred_sep_aux M.
-Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := proj2_sig uPred_sep_aux.
-
-Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := âˆ€ n' x',
-       n' â‰¤ n â†’ âœ“{n'} (x â‹… x') â†’ P n' x' â†’ Q n' (x â‹… x') |}.
-Next Obligation.
-  intros M P Q n x1 x1' HPQ ? n3 x3 ???; simpl in *.
-  apply uPred_mono with (x1 â‹… x3);
-    eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
-Qed.
-Next Obligation. naive_solver. Qed.
-Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
-Definition uPred_wand {M} := proj1_sig uPred_wand_aux M.
-Definition uPred_wand_eq :
-  @uPred_wand = @uPred_wand_def := proj2_sig uPred_wand_aux.
-
-Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
-  {| uPred_holds n x := P n (core x) |}.
-Next Obligation.
-  intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
-Qed.
-Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
-Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
-Definition uPred_always {M} := proj1_sig uPred_always_aux M.
-Definition uPred_always_eq :
-  @uPred_always = @uPred_always_def := proj2_sig uPred_always_aux.
-
-Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
-  {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
-Next Obligation.
-  intros M P [|n] x1 x2; eauto using uPred_mono, cmra_includedN_S.
-Qed.
-Next Obligation.
-  intros M P [|n1] [|n2] x; eauto using uPred_closed, cmra_validN_S with lia.
-Qed.
-Definition uPred_later_aux : { x | x = @uPred_later_def }. by eexists. Qed.
-Definition uPred_later {M} := proj1_sig uPred_later_aux M.
-Definition uPred_later_eq :
-  @uPred_later = @uPred_later_def := proj2_sig uPred_later_aux.
-
-Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
-  {| uPred_holds n x := a â‰¼{n} x |}.
-Next Obligation.
-  intros M a n x1 x [a' Hx1] [x2 ->].
-  exists (a' â‹… x2). by rewrite (assoc op) Hx1.
-Qed.
-Next Obligation. naive_solver eauto using cmra_includedN_le. Qed.
-Definition uPred_ownM_aux : { x | x = @uPred_ownM_def }. by eexists. Qed.
-Definition uPred_ownM {M} := proj1_sig uPred_ownM_aux M.
-Definition uPred_ownM_eq :
-  @uPred_ownM = @uPred_ownM_def := proj2_sig uPred_ownM_aux.
-
-Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M :=
-  {| uPred_holds n x := âœ“{n} a |}.
-Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
-Definition uPred_cmra_valid_aux : { x | x = @uPred_cmra_valid_def }. by eexists. Qed.
-Definition uPred_cmra_valid {M A} := proj1_sig uPred_cmra_valid_aux M A.
-Definition uPred_cmra_valid_eq :
-  @uPred_cmra_valid = @uPred_cmra_valid_def := proj2_sig uPred_cmra_valid_aux.
-
-Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
-  {| uPred_holds n x := âˆ€ k yf,
-      k â‰¤ n â†’ âœ“{k} (x â‹… yf) â†’ âˆƒ x', âœ“{k} (x' â‹… yf) âˆ§ Q k x' |}.
-Next Obligation.
-  intros M Q n x1 x2 HQ [x3 Hx] k yf Hk.
-  rewrite (dist_le _ _ _ _ Hx); last lia. intros Hxy.
-  destruct (HQ k (x3 â‹… yf)) as (x'&?&?); [auto|by rewrite assoc|].
-  exists (x' â‹… x3); split; first by rewrite -assoc.
-  apply uPred_mono with x'; eauto using cmra_includedN_l.
-Qed.
-Next Obligation. naive_solver. Qed.
-Definition uPred_bupd_aux : { x | x = @uPred_bupd_def }. by eexists. Qed.
-Definition uPred_bupd {M} := proj1_sig uPred_bupd_aux M.
-Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := proj2_sig uPred_bupd_aux.
-
-Notation "P âŠ¢ Q" := (uPred_entails P%I Q%I)
-  (at level 99, Q at level 200, right associativity) : C_scope.
-Notation "(âŠ¢)" := uPred_entails (only parsing) : C_scope.
-Notation "P âŠ£âŠ¢ Q" := (equiv (A:=uPred _) P%I Q%I)
-  (at level 95, no associativity) : C_scope.
-Notation "(âŠ£âŠ¢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
-Notation "â–  Ï†" := (uPred_pure Ï†%C%type)
-  (at level 20, right associativity) : uPred_scope.
-Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) : uPred_scope.
-Notation "x âŠ¥ y" := (uPred_pure (x%C%type âŠ¥ y%C%type)) : uPred_scope.
-Notation "'False'" := (uPred_pure False) : uPred_scope.
-Notation "'True'" := (uPred_pure True) : uPred_scope.
-Infix "âˆ§" := uPred_and : uPred_scope.
-Notation "(âˆ§)" := uPred_and (only parsing) : uPred_scope.
-Infix "âˆ¨" := uPred_or : uPred_scope.
-Notation "(âˆ¨)" := uPred_or (only parsing) : uPred_scope.
-Infix "â†’" := uPred_impl : uPred_scope.
-Infix "â˜…" := uPred_sep (at level 80, right associativity) : uPred_scope.
-Notation "(â˜…)" := uPred_sep (only parsing) : uPred_scope.
-Notation "P -â˜… Q" := (uPred_wand P Q)
-  (at level 99, Q at level 200, right associativity) : uPred_scope.
-Notation "âˆ€ x .. y , P" :=
-  (uPred_forall (Î» x, .. (uPred_forall (Î» y, P)) ..)%I) : uPred_scope.
-Notation "âˆƒ x .. y , P" :=
-  (uPred_exist (Î» x, .. (uPred_exist (Î» y, P)) ..)%I) : uPred_scope.
-Notation "â–¡ P" := (uPred_always P)
-  (at level 20, right associativity) : uPred_scope.
-Notation "â–· P" := (uPred_later P)
-  (at level 20, right associativity) : uPred_scope.
-Infix "â‰¡" := uPred_eq : uPred_scope.
-Notation "âœ“ x" := (uPred_cmra_valid x) (at level 20) : uPred_scope.
-Notation "|==> Q" := (uPred_bupd Q)
-  (at level 99, Q at level 200, format "|==>  Q") : uPred_scope.
-Notation "P ==â˜… Q" := (P âŠ¢ |==> Q)
-  (at level 99, Q at level 200, only parsing) : C_scope.
-Notation "P ==â˜… Q" := (P -â˜… |==> Q)%I
-  (at level 99, Q at level 200, format "P  ==â˜…  Q") : uPred_scope.
-
-Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P â†’ Q) âˆ§ (Q â†’ P))%I.
-Instance: Params (@uPred_iff) 1.
-Infix "â†”" := uPred_iff : uPred_scope.
-
-Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
-  (if p then â–¡ P else P)%I.
-Instance: Params (@uPred_always_if) 2.
-Arguments uPred_always_if _ !_ _/.
-Notation "â–¡? p P" := (uPred_always_if p P)
-  (at level 20, p at level 0, P at level 20, format "â–¡? p  P").
-
-Definition uPred_except_last {M} (P : uPred M) : uPred M := â–· False âˆ¨ P.
-Notation "â—‡ P" := (uPred_except_last P)
-  (at level 20, right associativity) : uPred_scope.
-Instance: Params (@uPred_except_last) 1.
-Typeclasses Opaque uPred_except_last.
-
-Class TimelessP {M} (P : uPred M) := timelessP : â–· P âŠ¢ â—‡ P.
-Arguments timelessP {_} _ {_}.
-
-Class PersistentP {M} (P : uPred M) := persistentP : P âŠ¢ â–¡ P.
-Arguments persistentP {_} _ {_}.
-
-Module uPred.
-Definition unseal :=
-  (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
-  uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
-  uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, uPred_bupd_eq).
-Ltac unseal := rewrite !unseal /=.
-
-Section uPred_logic.
-Context {M : ucmraT}.
-Implicit Types Ï† : Prop.
-Implicit Types P Q : uPred M.
-Implicit Types A : Type.
-Notation "P âŠ¢ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
-Notation "P âŠ£âŠ¢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *)
-Arguments uPred_holds {_} !_ _ _ /.
-Hint Immediate uPred_in_entails.
-
-Global Instance: PreOrder (@uPred_entails M).
-Proof.
-  split.
-  - by intros P; split=> x i.
-  - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
-Qed.
-Global Instance: AntiSymm (âŠ£âŠ¢) (@uPred_entails M).
-Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
-
-Lemma equiv_spec P Q : (P âŠ£âŠ¢ Q) â†” (P âŠ¢ Q) âˆ§ (Q âŠ¢ P).
-Proof.
-  split; [|by intros [??]; apply (anti_symm (âŠ¢))].
-  intros HPQ; split; split=> x i; apply HPQ.
-Qed.
-Lemma equiv_entails P Q : (P âŠ£âŠ¢ Q) â†’ (P âŠ¢ Q).
-Proof. apply equiv_spec. Qed.
-Lemma equiv_entails_sym P Q : (Q âŠ£âŠ¢ P) â†’ (P âŠ¢ Q).
-Proof. apply equiv_spec. Qed.
-Global Instance entails_proper :
-  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> iff) ((âŠ¢) : relation (uPred M)).
-Proof.
-  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
-  - by trans P1; [|trans Q1].
-  - by trans P2; [|trans Q2].
-Qed.
-Lemma entails_equiv_l (P Q R : uPred M) : (P âŠ£âŠ¢ Q) â†’ (Q âŠ¢ R) â†’ (P âŠ¢ R).
-Proof. by intros ->. Qed.
-Lemma entails_equiv_r (P Q R : uPred M) : (P âŠ¢ Q) â†’ (Q âŠ£âŠ¢ R) â†’ (P âŠ¢ R).
-Proof. by intros ? <-. Qed.
-
-(** Non-expansiveness and setoid morphisms *)
-Global Instance pure_proper : Proper (iff ==> (âŠ£âŠ¢)) (@uPred_pure M).
-Proof. intros Ï†1 Ï†2 HÏ†. by unseal; split=> -[|n] ?; try apply HÏ†. Qed.
-Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
-Proof.
-  intros P P' HP Q Q' HQ; unseal; split=> x n' ??.
-  split; (intros [??]; split; [by apply HP|by apply HQ]).
-Qed.
-Global Instance and_proper :
-  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_and M) := ne_proper_2 _.
-Global Instance or_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
-Proof.
-  intros P P' HP Q Q' HQ; split=> x n' ??.
-  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
-Qed.
-Global Instance or_proper :
-  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_or M) := ne_proper_2 _.
-Global Instance impl_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
-Proof.
-  intros P P' HP Q Q' HQ; split=> x n' ??.
-  unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
-Qed.
-Global Instance impl_proper :
-  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_impl M) := ne_proper_2 _.
-Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
-Proof.
-  intros P P' HP Q Q' HQ; split=> n' x ??.
-  unseal; split; intros (x1&x2&?&?&?); cofe_subst x;
-    exists x1, x2; split_and!; try (apply HP || apply HQ);
-    eauto using cmra_validN_op_l, cmra_validN_op_r.
-Qed.
-Global Instance sep_proper :
-  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_sep M) := ne_proper_2 _.
-Global Instance wand_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
-Proof.
-  intros P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
-    apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
-Qed.
-Global Instance wand_proper :
-  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_wand M) := ne_proper_2 _.
-Global Instance eq_ne (A : cofeT) n :
-  Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
-Proof.
-  intros x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
-  - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
-  - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
-Qed.
-Global Instance eq_proper (A : cofeT) :
-  Proper ((â‰¡) ==> (â‰¡) ==> (âŠ£âŠ¢)) (@uPred_eq M A) := ne_proper_2 _.
-Global Instance forall_ne A n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
-Proof.
-  by intros Î¨1 Î¨2 HÎ¨; unseal; split=> n' x; split; intros HP a; apply HÎ¨.
-Qed.
-Global Instance forall_proper A :
-  Proper (pointwise_relation _ (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_forall M A).
-Proof.
-  by intros Î¨1 Î¨2 HÎ¨; unseal; split=> n' x; split; intros HP a; apply HÎ¨.
-Qed.
-Global Instance exist_ne A n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
-Proof.
-  intros Î¨1 Î¨2 HÎ¨.
-  unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HÎ¨.
-Qed.
-Global Instance exist_proper A :
-  Proper (pointwise_relation _ (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_exist M A).
-Proof.
-  intros Î¨1 Î¨2 HÎ¨.
-  unseal; split=> n' x ?; split; intros [a ?]; exists a; by apply HÎ¨.
-Qed.
-Global Instance later_contractive : Contractive (@uPred_later M).
-Proof.
-  intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|].
-  apply (HPQ n'); eauto using cmra_validN_S.
-Qed.
-Global Instance later_proper' :
-  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_later M) := ne_proper _.
-Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
-Proof.
-  intros P1 P2 HP.
-  unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
-Qed.
-Global Instance always_proper :
-  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_always M) := ne_proper _.
-Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
-Proof.
-  intros a b Ha.
-  unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
-Qed.
-Global Instance ownM_proper: Proper ((â‰¡) ==> (âŠ£âŠ¢)) (@uPred_ownM M) := ne_proper _.
-Global Instance cmra_valid_ne {A : cmraT} n :
-Proper (dist n ==> dist n) (@uPred_cmra_valid M A).
-Proof.
-  intros a b Ha; unseal; split=> n' x ? /=.
-  by rewrite (dist_le _ _ _ _ Ha); last lia.
-Qed.
-Global Instance cmra_valid_proper {A : cmraT} :
-  Proper ((â‰¡) ==> (âŠ£âŠ¢)) (@uPred_cmra_valid M A) := ne_proper _.
-Global Instance bupd_ne n : Proper (dist n ==> dist n) (@uPred_bupd M).
-Proof.
-  intros P Q HPQ.
-  unseal; split=> n' x; split; intros HP k yf ??;
-    destruct (HP k yf) as (x'&?&?); auto;
-    exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
-Qed.
-Global Instance bupd_proper : Proper ((â‰¡) ==> (â‰¡)) (@uPred_bupd M) := ne_proper _.
-
-(** Introduction and elimination rules *)
-Lemma pure_intro Ï† P : Ï† â†’ P âŠ¢ â–  Ï†.
-Proof. by intros ?; unseal; split. Qed.
-Lemma pure_elim Ï† Q R : (Q âŠ¢ â–  Ï†) â†’ (Ï† â†’ Q âŠ¢ R) â†’ Q âŠ¢ R.
-Proof.
-  unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
-Qed.
-Lemma pure_forall_2 {A} (Ï† : A â†’ Prop) : (âˆ€ x : A, â–  Ï† x) âŠ¢ â–  (âˆ€ x : A, Ï† x).
-Proof. by unseal. Qed.
-
-Lemma and_elim_l P Q : P âˆ§ Q âŠ¢ P.
-Proof. by unseal; split=> n x ? [??]. Qed.
-Lemma and_elim_r P Q : P âˆ§ Q âŠ¢ Q.
-Proof. by unseal; split=> n x ? [??]. Qed.
-Lemma and_intro P Q R : (P âŠ¢ Q) â†’ (P âŠ¢ R) â†’ P âŠ¢ Q âˆ§ R.
-Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
-
-Lemma or_intro_l P Q : P âŠ¢ P âˆ¨ Q.
-Proof. unseal; split=> n x ??; left; auto. Qed.
-Lemma or_intro_r P Q : Q âŠ¢ P âˆ¨ Q.
-Proof. unseal; split=> n x ??; right; auto. Qed.
-Lemma or_elim P Q R : (P âŠ¢ R) â†’ (Q âŠ¢ R) â†’ P âˆ¨ Q âŠ¢ R.
-Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
-
-Lemma impl_intro_r P Q R : (P âˆ§ Q âŠ¢ R) â†’ P âŠ¢ Q â†’ R.
-Proof.
-  unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ;
-    naive_solver eauto using uPred_mono, uPred_closed, cmra_included_includedN.
-Qed.
-Lemma impl_elim P Q R : (P âŠ¢ Q â†’ R) â†’ (P âŠ¢ Q) â†’ P âŠ¢ R.
-Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
-
-Lemma forall_intro {A} P (Î¨ : A â†’ uPred M): (âˆ€ a, P âŠ¢ Î¨ a) â†’ P âŠ¢ âˆ€ a, Î¨ a.
-Proof. unseal; intros HPÎ¨; split=> n x ?? a; by apply HPÎ¨. Qed.
-Lemma forall_elim {A} {Î¨ : A â†’ uPred M} a : (âˆ€ a, Î¨ a) âŠ¢ Î¨ a.
-Proof. unseal; split=> n x ? HP; apply HP. Qed.
-
-Lemma exist_intro {A} {Î¨ : A â†’ uPred M} a : Î¨ a âŠ¢ âˆƒ a, Î¨ a.
-Proof. unseal; split=> n x ??; by exists a. Qed.
-Lemma exist_elim {A} (Î¦ : A â†’ uPred M) Q : (âˆ€ a, Î¦ a âŠ¢ Q) â†’ (âˆƒ a, Î¦ a) âŠ¢ Q.
-Proof. unseal; intros HÎ¦Î¨; split=> n x ? [a ?]; by apply HÎ¦Î¨ with a. Qed.
-
-Lemma eq_refl {A : cofeT} (a : A) : True âŠ¢ a â‰¡ a.
-Proof. unseal; by split=> n x ??; simpl. Qed.
-Lemma eq_rewrite {A : cofeT} a b (Î¨ : A â†’ uPred M) P
-  {HÎ¨ : âˆ€ n, Proper (dist n ==> dist n) Î¨} : (P âŠ¢ a â‰¡ b) â†’ (P âŠ¢ Î¨ a) â†’ P âŠ¢ Î¨ b.
-Proof.
-  unseal; intros Hab Ha; split=> n x ??. apply HÎ¨ with n a; auto.
-  - by symmetry; apply Hab with x.
-  - by apply Ha.
-Qed.
-Lemma eq_equiv {A : cofeT} (a b : A) : (True âŠ¢ a â‰¡ b) â†’ a â‰¡ b.
-Proof.
-  unseal=> Hab; apply equiv_dist; intros n; apply Hab with âˆ…; last done.
-  apply cmra_valid_validN, ucmra_unit_valid.
-Qed.
-Lemma eq_rewrite_contractive {A : cofeT} a b (Î¨ : A â†’ uPred M) P
-  {HÎ¨ : Contractive Î¨} : (P âŠ¢ â–· (a â‰¡ b)) â†’ (P âŠ¢ Î¨ a) â†’ P âŠ¢ Î¨ b.
-Proof.
-  unseal; intros Hab Ha; split=> n x ??. apply HÎ¨ with n a; auto.
-  - destruct n; intros m ?; first omega. apply (dist_le n); last omega.
-    symmetry. by destruct Hab as [Hab]; eapply (Hab (S n)).
-  - by apply Ha.
-Qed.
-
-(* Derived logical stuff *)
-Lemma False_elim P : False âŠ¢ P.
-Proof. by apply (pure_elim False). Qed.
-Lemma True_intro P : P âŠ¢ True.
-Proof. by apply pure_intro. Qed.
-
-Lemma and_elim_l' P Q R : (P âŠ¢ R) â†’ P âˆ§ Q âŠ¢ R.
-Proof. by rewrite and_elim_l. Qed.
-Lemma and_elim_r' P Q R : (Q âŠ¢ R) â†’ P âˆ§ Q âŠ¢ R.
-Proof. by rewrite and_elim_r. Qed.
-Lemma or_intro_l' P Q R : (P âŠ¢ Q) â†’ P âŠ¢ Q âˆ¨ R.
-Proof. intros ->; apply or_intro_l. Qed.
-Lemma or_intro_r' P Q R : (P âŠ¢ R) â†’ P âŠ¢ Q âˆ¨ R.
-Proof. intros ->; apply or_intro_r. Qed.
-Lemma exist_intro' {A} P (Î¨ : A â†’ uPred M) a : (P âŠ¢ Î¨ a) â†’ P âŠ¢ âˆƒ a, Î¨ a.
-Proof. intros ->; apply exist_intro. Qed.
-Lemma forall_elim' {A} P (Î¨ : A â†’ uPred M) : (P âŠ¢ âˆ€ a, Î¨ a) â†’ âˆ€ a, P âŠ¢ Î¨ a.
-Proof. move=> HP a. by rewrite HP forall_elim. Qed.
-
-Hint Resolve pure_intro.
-Hint Resolve or_elim or_intro_l' or_intro_r'.
-Hint Resolve and_intro and_elim_l' and_elim_r'.
-Hint Immediate True_intro False_elim.
-
-Lemma impl_intro_l P Q R : (Q âˆ§ P âŠ¢ R) â†’ P âŠ¢ Q â†’ R.
-Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
-Lemma impl_elim_l P Q : (P â†’ Q) âˆ§ P âŠ¢ Q.
-Proof. apply impl_elim with P; auto. Qed.
-Lemma impl_elim_r P Q : P âˆ§ (P â†’ Q) âŠ¢ Q.
-Proof. apply impl_elim with P; auto. Qed.
-Lemma impl_elim_l' P Q R : (P âŠ¢ Q â†’ R) â†’ P âˆ§ Q âŠ¢ R.
-Proof. intros; apply impl_elim with Q; auto. Qed.
-Lemma impl_elim_r' P Q R : (Q âŠ¢ P â†’ R) â†’ P âˆ§ Q âŠ¢ R.
-Proof. intros; apply impl_elim with P; auto. Qed.
-Lemma impl_entails P Q : (True âŠ¢ P â†’ Q) â†’ P âŠ¢ Q.
-Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
-Lemma entails_impl P Q : (P âŠ¢ Q) â†’ True âŠ¢ P â†’ Q.
-Proof. auto using impl_intro_l. Qed.
-
-Lemma and_mono P P' Q Q' : (P âŠ¢ Q) â†’ (P' âŠ¢ Q') â†’ P âˆ§ P' âŠ¢ Q âˆ§ Q'.
-Proof. auto. Qed.
-Lemma and_mono_l P P' Q : (P âŠ¢ Q) â†’ P âˆ§ P' âŠ¢ Q âˆ§ P'.
-Proof. by intros; apply and_mono. Qed.
-Lemma and_mono_r P P' Q' : (P' âŠ¢ Q') â†’ P âˆ§ P' âŠ¢ P âˆ§ Q'.
-Proof. by apply and_mono. Qed.
-
-Lemma or_mono P P' Q Q' : (P âŠ¢ Q) â†’ (P' âŠ¢ Q') â†’ P âˆ¨ P' âŠ¢ Q âˆ¨ Q'.
-Proof. auto. Qed.
-Lemma or_mono_l P P' Q : (P âŠ¢ Q) â†’ P âˆ¨ P' âŠ¢ Q âˆ¨ P'.
-Proof. by intros; apply or_mono. Qed.
-Lemma or_mono_r P P' Q' : (P' âŠ¢ Q') â†’ P âˆ¨ P' âŠ¢ P âˆ¨ Q'.
-Proof. by apply or_mono. Qed.
-
-Lemma impl_mono P P' Q Q' : (Q âŠ¢ P) â†’ (P' âŠ¢ Q') â†’ (P â†’ P') âŠ¢ Q â†’ Q'.
-Proof.
-  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
-  apply impl_elim with P; eauto.
-Qed.
-Lemma forall_mono {A} (Î¦ Î¨ : A â†’ uPred M) :
-  (âˆ€ a, Î¦ a âŠ¢ Î¨ a) â†’ (âˆ€ a, Î¦ a) âŠ¢ âˆ€ a, Î¨ a.
-Proof.
-  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
-Qed.
-Lemma exist_mono {A} (Î¦ Î¨ : A â†’ uPred M) :
-  (âˆ€ a, Î¦ a âŠ¢ Î¨ a) â†’ (âˆƒ a, Î¦ a) âŠ¢ âˆƒ a, Î¨ a.
-Proof. intros HÎ¦. apply exist_elim=> a; rewrite (HÎ¦ a); apply exist_intro. Qed.
-
-Global Instance and_mono' : Proper ((âŠ¢) ==> (âŠ¢) ==> (âŠ¢)) (@uPred_and M).
-Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
-Global Instance and_flip_mono' :
-  Proper (flip (âŠ¢) ==> flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_and M).
-Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
-Global Instance or_mono' : Proper ((âŠ¢) ==> (âŠ¢) ==> (âŠ¢)) (@uPred_or M).
-Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
-Global Instance or_flip_mono' :
-  Proper (flip (âŠ¢) ==> flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_or M).
-Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
-Global Instance impl_mono' :
-  Proper (flip (âŠ¢) ==> (âŠ¢) ==> (âŠ¢)) (@uPred_impl M).
-Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
-Global Instance forall_mono' A :
-  Proper (pointwise_relation _ (âŠ¢) ==> (âŠ¢)) (@uPred_forall M A).
-Proof. intros P1 P2; apply forall_mono. Qed.
-Global Instance exist_mono' A :
-  Proper (pointwise_relation _ (âŠ¢) ==> (âŠ¢)) (@uPred_exist M A).
-Proof. intros P1 P2; apply exist_mono. Qed.
-
-Global Instance and_idem : IdemP (âŠ£âŠ¢) (@uPred_and M).
-Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance or_idem : IdemP (âŠ£âŠ¢) (@uPred_or M).
-Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance and_comm : Comm (âŠ£âŠ¢) (@uPred_and M).
-Proof. intros P Q; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance True_and : LeftId (âŠ£âŠ¢) True%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance and_True : RightId (âŠ£âŠ¢) True%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance False_and : LeftAbsorb (âŠ£âŠ¢) False%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance and_False : RightAbsorb (âŠ£âŠ¢) False%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance True_or : LeftAbsorb (âŠ£âŠ¢) True%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance or_True : RightAbsorb (âŠ£âŠ¢) True%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance False_or : LeftId (âŠ£âŠ¢) False%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance or_False : RightId (âŠ£âŠ¢) False%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance and_assoc : Assoc (âŠ£âŠ¢) (@uPred_and M).
-Proof. intros P Q R; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance or_comm : Comm (âŠ£âŠ¢) (@uPred_or M).
-Proof. intros P Q; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance or_assoc : Assoc (âŠ£âŠ¢) (@uPred_or M).
-Proof. intros P Q R; apply (anti_symm (âŠ¢)); auto. Qed.
-Global Instance True_impl : LeftId (âŠ£âŠ¢) True%I (@uPred_impl M).
-Proof.
-  intros P; apply (anti_symm (âŠ¢)).
-  - by rewrite -(left_id True%I uPred_and (_ â†’ _)%I) impl_elim_r.
-  - by apply impl_intro_l; rewrite left_id.
-Qed.
-
-Lemma exists_impl_forall {A} P (Î¨ : A â†’ uPred M) :
-  ((âˆƒ x : A, Î¨ x) â†’ P) âŠ£âŠ¢ âˆ€ x : A, Î¨ x â†’ P.
-Proof.
-  apply equiv_spec; split.
-  - apply forall_intro=>x. by rewrite -exist_intro.
-  - apply impl_intro_r, impl_elim_r', exist_elim=>x.
-    apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r.
-Qed.
-
-Lemma or_and_l P Q R : P âˆ¨ Q âˆ§ R âŠ£âŠ¢ (P âˆ¨ Q) âˆ§ (P âˆ¨ R).
-Proof.
-  apply (anti_symm (âŠ¢)); first auto.
-  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
-Qed.
-Lemma or_and_r P Q R : P âˆ§ Q âˆ¨ R âŠ£âŠ¢ (P âˆ¨ R) âˆ§ (Q âˆ¨ R).
-Proof. by rewrite -!(comm _ R) or_and_l. Qed.
-Lemma and_or_l P Q R : P âˆ§ (Q âˆ¨ R) âŠ£âŠ¢ P âˆ§ Q âˆ¨ P âˆ§ R.
-Proof.
-  apply (anti_symm (âŠ¢)); last auto.
-  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
-Qed.
-Lemma and_or_r P Q R : (P âˆ¨ Q) âˆ§ R âŠ£âŠ¢ P âˆ§ R âˆ¨ Q âˆ§ R.
-Proof. by rewrite -!(comm _ R) and_or_l. Qed.
-Lemma and_exist_l {A} P (Î¨ : A â†’ uPred M) : P âˆ§ (âˆƒ a, Î¨ a) âŠ£âŠ¢ âˆƒ a, P âˆ§ Î¨ a.
-Proof.
-  apply (anti_symm (âŠ¢)).
-  - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
-    by rewrite -(exist_intro a).
-  - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
-    by rewrite -(exist_intro a) and_elim_r.
-Qed.
-Lemma and_exist_r {A} P (Î¦: A â†’ uPred M) : (âˆƒ a, Î¦ a) âˆ§ P âŠ£âŠ¢ âˆƒ a, Î¦ a âˆ§ P.
-Proof.
-  rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
-Qed.
-
-Lemma pure_mono Ï†1 Ï†2 : (Ï†1 â†’ Ï†2) â†’ â–  Ï†1 âŠ¢ â–  Ï†2.
-Proof. intros; apply pure_elim with Ï†1; eauto. Qed.
-Global Instance pure_mono' : Proper (impl ==> (âŠ¢)) (@uPred_pure M).
-Proof. intros Ï†1 Ï†2; apply pure_mono. Qed.
-Lemma pure_iff Ï†1 Ï†2 : (Ï†1 â†” Ï†2) â†’ â–  Ï†1 âŠ£âŠ¢ â–  Ï†2.
-Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
-Lemma pure_intro_l Ï† Q R : Ï† â†’ (â–  Ï† âˆ§ Q âŠ¢ R) â†’ Q âŠ¢ R.
-Proof. intros ? <-; auto using pure_intro. Qed.
-Lemma pure_intro_r Ï† Q R : Ï† â†’ (Q âˆ§ â–  Ï† âŠ¢ R) â†’ Q âŠ¢ R.
-Proof. intros ? <-; auto. Qed.
-Lemma pure_intro_impl Ï† Q R : Ï† â†’ (Q âŠ¢ â–  Ï† â†’ R) â†’ Q âŠ¢ R.
-Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
-Lemma pure_elim_l Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ â–  Ï† âˆ§ Q âŠ¢ R.
-Proof. intros; apply pure_elim with Ï†; eauto. Qed.
-Lemma pure_elim_r Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ Q âˆ§ â–  Ï† âŠ¢ R.
-Proof. intros; apply pure_elim with Ï†; eauto. Qed.
-Lemma pure_equiv (Ï† : Prop) : Ï† â†’ â–  Ï† âŠ£âŠ¢ True.
-Proof. intros; apply (anti_symm _); auto. Qed.
-
-Lemma pure_and Ï†1 Ï†2 : â–  (Ï†1 âˆ§ Ï†2) âŠ£âŠ¢ â–  Ï†1 âˆ§ â–  Ï†2.
-Proof.
-  apply (anti_symm _).
-  - eapply pure_elim=> // -[??]; auto.
-  - eapply (pure_elim Ï†1); [auto|]=> ?. eapply (pure_elim Ï†2); auto.
-Qed.
-Lemma pure_or Ï†1 Ï†2 : â–  (Ï†1 âˆ¨ Ï†2) âŠ£âŠ¢ â–  Ï†1 âˆ¨ â–  Ï†2.
-Proof.
-  apply (anti_symm _).
-  - eapply pure_elim=> // -[?|?]; auto.
-  - apply or_elim; eapply pure_elim; eauto.
-Qed.
-Lemma pure_impl Ï†1 Ï†2 : â–  (Ï†1 â†’ Ï†2) âŠ£âŠ¢ (â–  Ï†1 â†’ â–  Ï†2).
-Proof.
-  apply (anti_symm _).
-  - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
-  - rewrite -pure_forall_2. apply forall_intro=> ?.
-    by rewrite -(left_id True uPred_and (_â†’_))%I (pure_equiv Ï†1) // impl_elim_r.
-Qed.
-Lemma pure_forall {A} (Ï† : A â†’ Prop) : â–  (âˆ€ x, Ï† x) âŠ£âŠ¢ âˆ€ x, â–  Ï† x.
-Proof.
-  apply (anti_symm _); auto using pure_forall_2.
-  apply forall_intro=> x. eauto using pure_mono.
-Qed.
-Lemma pure_exist {A} (Ï† : A â†’ Prop) : â–  (âˆƒ x, Ï† x) âŠ£âŠ¢ âˆƒ x, â–  Ï† x.
-Proof.
-  apply (anti_symm _).
-  - eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto.
-  - apply exist_elim=> x. eauto using pure_mono.
-Qed.
-
-Lemma eq_refl' {A : cofeT} (a : A) P : P âŠ¢ a â‰¡ a.
-Proof. rewrite (True_intro P). apply eq_refl. Qed.
-Hint Resolve eq_refl'.
-Lemma equiv_eq {A : cofeT} P (a b : A) : a â‰¡ b â†’ P âŠ¢ a â‰¡ b.
-Proof. by intros ->. Qed.
-Lemma eq_sym {A : cofeT} (a b : A) : a â‰¡ b âŠ¢ b â‰¡ a.
-Proof. apply (eq_rewrite a b (Î» b, b â‰¡ a)%I); auto. solve_proper. Qed.
-
-Lemma pure_alt Ï† : â–  Ï† âŠ£âŠ¢ âˆƒ _ : Ï†, True.
-Proof.
-  apply (anti_symm _).
-  - eapply pure_elim; eauto=> H. rewrite -(exist_intro H); auto.
-  - by apply exist_elim, pure_intro.
-Qed.
-Lemma and_alt P Q : P âˆ§ Q âŠ£âŠ¢ âˆ€ b : bool, if b then P else Q.
-Proof.
-  apply (anti_symm _); first apply forall_intro=> -[]; auto.
-  apply and_intro. by rewrite (forall_elim true). by rewrite (forall_elim false).
-Qed.
-Lemma or_alt P Q : P âˆ¨ Q âŠ£âŠ¢ âˆƒ b : bool, if b then P else Q.
-Proof.
-  apply (anti_symm _); last apply exist_elim=> -[]; auto.
-  apply or_elim. by rewrite -(exist_intro true). by rewrite -(exist_intro false).
-Qed.
-
-Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
-Proof. unfold uPred_iff; solve_proper. Qed.
-Global Instance iff_proper :
-  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_iff M) := ne_proper_2 _.
-
-Lemma iff_refl Q P : Q âŠ¢ P â†” P.
-Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
-Lemma iff_equiv P Q : (True âŠ¢ P â†” Q) â†’ (P âŠ£âŠ¢ Q).
-Proof.
-  intros HPQ; apply (anti_symm (âŠ¢));
-    apply impl_entails; rewrite HPQ /uPred_iff; auto.
-Qed.
-Lemma equiv_iff P Q : (P âŠ£âŠ¢ Q) â†’ True âŠ¢ P â†” Q.
-Proof. intros ->; apply iff_refl. Qed.
-Lemma eq_iff P Q : P â‰¡ Q âŠ¢ P â†” Q.
-Proof.
-  apply (eq_rewrite P Q (Î» Q, P â†” Q))%I; first solve_proper; auto using iff_refl.
-Qed.
-
-(* BI connectives *)
-Lemma sep_mono P P' Q Q' : (P âŠ¢ Q) â†’ (P' âŠ¢ Q') â†’ P â˜… P' âŠ¢ Q â˜… Q'.
-Proof.
-  intros HQ HQ'; unseal.
-  split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; cofe_subst x;
-    eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
-Qed.
-Lemma True_sep_1 P : P âŠ¢ True â˜… P.
-Proof.
-  unseal; split; intros n x ??. exists (core x), x. by rewrite cmra_core_l.
-Qed.
-Lemma True_sep_2 P : True â˜… P âŠ¢ P.
-Proof.
-  unseal; split; intros n x ? (x1&x2&?&_&?); cofe_subst;
-    eauto using uPred_mono, cmra_includedN_r.
-Qed.
-Lemma sep_comm' P Q : P â˜… Q âŠ¢ Q â˜… P.
-Proof.
-  unseal; split; intros n x ? (x1&x2&?&?&?); exists x2, x1; by rewrite (comm op).
-Qed.
-Lemma sep_assoc' P Q R : (P â˜… Q) â˜… R âŠ¢ P â˜… (Q â˜… R).
-Proof.
-  unseal; split; intros n x ? (x1&x2&Hx&(y1&y2&Hy&?&?)&?).
-  exists y1, (y2 â‹… x2); split_and?; auto.
-  + by rewrite (assoc op) -Hy -Hx.
-  + by exists y2, x2.
-Qed.
-Lemma wand_intro_r P Q R : (P â˜… Q âŠ¢ R) â†’ P âŠ¢ Q -â˜… R.
-Proof.
-  unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
-  exists x, x'; split_and?; auto.
-  eapply uPred_closed with n; eauto using cmra_validN_op_l.
-Qed.
-Lemma wand_elim_l' P Q R : (P âŠ¢ Q -â˜… R) â†’ P â˜… Q âŠ¢ R.
-Proof.
-  unseal =>HPQR. split; intros n x ? (?&?&?&?&?). cofe_subst.
-  eapply HPQR; eauto using cmra_validN_op_l.
-Qed.
-
-(* Derived BI Stuff *)
-Hint Resolve sep_mono.
-Lemma sep_mono_l P P' Q : (P âŠ¢ Q) â†’ P â˜… P' âŠ¢ Q â˜… P'.
-Proof. by intros; apply sep_mono. Qed.
-Lemma sep_mono_r P P' Q' : (P' âŠ¢ Q') â†’ P â˜… P' âŠ¢ P â˜… Q'.
-Proof. by apply sep_mono. Qed.
-Global Instance sep_mono' : Proper ((âŠ¢) ==> (âŠ¢) ==> (âŠ¢)) (@uPred_sep M).
-Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
-Global Instance sep_flip_mono' :
-  Proper (flip (âŠ¢) ==> flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_sep M).
-Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
-Lemma wand_mono P P' Q Q' : (Q âŠ¢ P) â†’ (P' âŠ¢ Q') â†’ (P -â˜… P') âŠ¢ Q -â˜… Q'.
-Proof.
-  intros HP HQ; apply wand_intro_r. rewrite HP -HQ. by apply wand_elim_l'.
-Qed.
-Global Instance wand_mono' : Proper (flip (âŠ¢) ==> (âŠ¢) ==> (âŠ¢)) (@uPred_wand M).
-Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
-
-Global Instance sep_comm : Comm (âŠ£âŠ¢) (@uPred_sep M).
-Proof. intros P Q; apply (anti_symm _); auto using sep_comm'. Qed.
-Global Instance sep_assoc : Assoc (âŠ£âŠ¢) (@uPred_sep M).
-Proof.
-  intros P Q R; apply (anti_symm _); auto using sep_assoc'.
-  by rewrite !(comm _ P) !(comm _ _ R) sep_assoc'.
-Qed.
-Global Instance True_sep : LeftId (âŠ£âŠ¢) True%I (@uPred_sep M).
-Proof. intros P; apply (anti_symm _); auto using True_sep_1, True_sep_2. Qed.
-Global Instance sep_True : RightId (âŠ£âŠ¢) True%I (@uPred_sep M).
-Proof. by intros P; rewrite comm left_id. Qed.
-Lemma sep_elim_l P Q : P â˜… Q âŠ¢ P.
-Proof. by rewrite (True_intro Q) right_id. Qed.
-Lemma sep_elim_r P Q : P â˜… Q âŠ¢ Q.
-Proof. by rewrite (comm (â˜…))%I; apply sep_elim_l. Qed.
-Lemma sep_elim_l' P Q R : (P âŠ¢ R) â†’ P â˜… Q âŠ¢ R.
-Proof. intros ->; apply sep_elim_l. Qed.
-Lemma sep_elim_r' P Q R : (Q âŠ¢ R) â†’ P â˜… Q âŠ¢ R.
-Proof. intros ->; apply sep_elim_r. Qed.
-Hint Resolve sep_elim_l' sep_elim_r'.
-Lemma sep_intro_True_l P Q R : (True âŠ¢ P) â†’ (R âŠ¢ Q) â†’ R âŠ¢ P â˜… Q.
-Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
-Lemma sep_intro_True_r P Q R : (R âŠ¢ P) â†’ (True âŠ¢ Q) â†’ R âŠ¢ P â˜… Q.
-Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
-Lemma sep_elim_True_l P Q R : (True âŠ¢ P) â†’ (P â˜… R âŠ¢ Q) â†’ R âŠ¢ Q.
-Proof. by intros HP; rewrite -HP left_id. Qed.
-Lemma sep_elim_True_r P Q R : (True âŠ¢ P) â†’ (R â˜… P âŠ¢ Q) â†’ R âŠ¢ Q.
-Proof. by intros HP; rewrite -HP right_id. Qed.
-Lemma wand_intro_l P Q R : (Q â˜… P âŠ¢ R) â†’ P âŠ¢ Q -â˜… R.
-Proof. rewrite comm; apply wand_intro_r. Qed.
-Lemma wand_elim_l P Q : (P -â˜… Q) â˜… P âŠ¢ Q.
-Proof. by apply wand_elim_l'. Qed.
-Lemma wand_elim_r P Q : P â˜… (P -â˜… Q) âŠ¢ Q.
-Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
-Lemma wand_elim_r' P Q R : (Q âŠ¢ P -â˜… R) â†’ P â˜… Q âŠ¢ R.
-Proof. intros ->; apply wand_elim_r. Qed.
-Lemma wand_apply_l P Q Q' R R' : (P âŠ¢ Q' -â˜… R') â†’ (R' âŠ¢ R) â†’ (Q âŠ¢ Q') â†’ P â˜… Q âŠ¢ R.
-Proof. intros -> -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r P Q Q' R R' : (P âŠ¢ Q' -â˜… R') â†’ (R' âŠ¢ R) â†’ (Q âŠ¢ Q') â†’ Q â˜… P âŠ¢ R.
-Proof. intros -> -> <-; apply wand_elim_r. Qed.
-Lemma wand_apply_l' P Q Q' R : (P âŠ¢ Q' -â˜… R) â†’ (Q âŠ¢ Q') â†’ P â˜… Q âŠ¢ R.
-Proof. intros -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r' P Q Q' R : (P âŠ¢ Q' -â˜… R) â†’ (Q âŠ¢ Q') â†’ Q â˜… P âŠ¢ R.
-Proof. intros -> <-; apply wand_elim_r. Qed.
-Lemma wand_frame_l P Q R : (Q -â˜… R) âŠ¢ P â˜… Q -â˜… P â˜… R.
-Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
-Lemma wand_frame_r P Q R : (Q -â˜… R) âŠ¢ Q â˜… P -â˜… R â˜… P.
-Proof.
-  apply wand_intro_l. rewrite ![(_ â˜… P)%I]comm -assoc.
-  apply sep_mono_r, wand_elim_r.
-Qed.
-Lemma wand_diag P : (P -â˜… P) âŠ£âŠ¢ True.
-Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
-Lemma wand_True P : (True -â˜… P) âŠ£âŠ¢ P.
-Proof.
-  apply (anti_symm _); last by auto using wand_intro_l.
-  eapply sep_elim_True_l; first reflexivity. by rewrite wand_elim_r.
-Qed.
-Lemma wand_entails P Q : (True âŠ¢ P -â˜… Q) â†’ P âŠ¢ Q.
-Proof.
-  intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
-Qed.
-Lemma entails_wand P Q : (P âŠ¢ Q) â†’ True âŠ¢ P -â˜… Q.
-Proof. auto using wand_intro_l. Qed.
-Lemma wand_curry P Q R : (P -â˜… Q -â˜… R) âŠ£âŠ¢ (P â˜… Q -â˜… R).
-Proof.
-  apply (anti_symm _).
-  - apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r.
-  - do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) wand_elim_r.
-Qed.
-
-Lemma sep_and P Q : (P â˜… Q) âŠ¢ (P âˆ§ Q).
-Proof. auto. Qed.
-Lemma impl_wand P Q : (P â†’ Q) âŠ¢ P -â˜… Q.
-Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
-Lemma pure_elim_sep_l Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ â–  Ï† â˜… Q âŠ¢ R.
-Proof. intros; apply pure_elim with Ï†; eauto. Qed.
-Lemma pure_elim_sep_r Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ Q â˜… â–  Ï† âŠ¢ R.
-Proof. intros; apply pure_elim with Ï†; eauto. Qed.
-
-Global Instance sep_False : LeftAbsorb (âŠ£âŠ¢) False%I (@uPred_sep M).
-Proof. intros P; apply (anti_symm _); auto. Qed.
-Global Instance False_sep : RightAbsorb (âŠ£âŠ¢) False%I (@uPred_sep M).
-Proof. intros P; apply (anti_symm _); auto. Qed.
-
-Lemma sep_and_l P Q R : P â˜… (Q âˆ§ R) âŠ¢ (P â˜… Q) âˆ§ (P â˜… R).
-Proof. auto. Qed.
-Lemma sep_and_r P Q R : (P âˆ§ Q) â˜… R âŠ¢ (P â˜… R) âˆ§ (Q â˜… R).
-Proof. auto. Qed.
-Lemma sep_or_l P Q R : P â˜… (Q âˆ¨ R) âŠ£âŠ¢ (P â˜… Q) âˆ¨ (P â˜… R).
-Proof.
-  apply (anti_symm (âŠ¢)); last by eauto 8.
-  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
-Qed.
-Lemma sep_or_r P Q R : (P âˆ¨ Q) â˜… R âŠ£âŠ¢ (P â˜… R) âˆ¨ (Q â˜… R).
-Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
-Lemma sep_exist_l {A} P (Î¨ : A â†’ uPred M) : P â˜… (âˆƒ a, Î¨ a) âŠ£âŠ¢ âˆƒ a, P â˜… Î¨ a.
-Proof.
-  intros; apply (anti_symm (âŠ¢)).
-  - apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
-    by rewrite -(exist_intro a).
-  - apply exist_elim=> a; apply sep_mono; auto using exist_intro.
-Qed.
-Lemma sep_exist_r {A} (Î¦: A â†’ uPred M) Q: (âˆƒ a, Î¦ a) â˜… Q âŠ£âŠ¢ âˆƒ a, Î¦ a â˜… Q.
-Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
-Lemma sep_forall_l {A} P (Î¨ : A â†’ uPred M) : P â˜… (âˆ€ a, Î¨ a) âŠ¢ âˆ€ a, P â˜… Î¨ a.
-Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
-Lemma sep_forall_r {A} (Î¦ : A â†’ uPred M) Q : (âˆ€ a, Î¦ a) â˜… Q âŠ¢ âˆ€ a, Î¦ a â˜… Q.
-Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
-
-(* Always *)
-Lemma always_mono P Q : (P âŠ¢ Q) â†’ â–¡ P âŠ¢ â–¡ Q.
-Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
-Lemma always_elim P : â–¡ P âŠ¢ P.
-Proof.
-  unseal; split=> n x ? /=.
-  eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
-Qed.
-Lemma always_idemp P : â–¡ P âŠ¢ â–¡ â–¡ P.
-Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
-
-Lemma always_pure_2 Ï† : â–  Ï† âŠ¢ â–¡ â–  Ï†.
-Proof. by unseal. Qed.
-Lemma always_forall_2 {A} (Î¨ : A â†’ uPred M) : (âˆ€ a, â–¡ Î¨ a) âŠ¢ (â–¡ âˆ€ a, Î¨ a).
-Proof. by unseal. Qed.
-Lemma always_exist_1 {A} (Î¨ : A â†’ uPred M) : (â–¡ âˆƒ a, Î¨ a) âŠ¢ (âˆƒ a, â–¡ Î¨ a).
-Proof. by unseal. Qed.
-
-Lemma always_and_sep_1 P Q : â–¡ (P âˆ§ Q) âŠ¢ â–¡ (P â˜… Q).
-Proof.
-  unseal; split=> n x ? [??].
-  exists (core x), (core x); rewrite -cmra_core_dup; auto.
-Qed.
-Lemma always_and_sep_l_1 P Q : â–¡ P âˆ§ Q âŠ¢ â–¡ P â˜… Q.
-Proof.
-  unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
-  by rewrite cmra_core_l cmra_core_idemp.
-Qed.
-
-(* Always derived *)
-Hint Resolve always_mono always_elim.
-Global Instance always_mono' : Proper ((âŠ¢) ==> (âŠ¢)) (@uPred_always M).
-Proof. intros P Q; apply always_mono. Qed.
-Global Instance always_flip_mono' :
-  Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_always M).
-Proof. intros P Q; apply always_mono. Qed.
-
-Lemma always_intro' P Q : (â–¡ P âŠ¢ Q) â†’ â–¡ P âŠ¢ â–¡ Q.
-Proof. intros <-. apply always_idemp. Qed.
-
-Lemma always_pure Ï† : â–¡ â–  Ï† âŠ£âŠ¢ â–  Ï†.
-Proof. apply (anti_symm _); auto using always_pure_2. Qed.
-Lemma always_forall {A} (Î¨ : A â†’ uPred M) : (â–¡ âˆ€ a, Î¨ a) âŠ£âŠ¢ (âˆ€ a, â–¡ Î¨ a).
-Proof.
-  apply (anti_symm _); auto using always_forall_2.
-  apply forall_intro=> x. by rewrite (forall_elim x).
-Qed.
-Lemma always_exist {A} (Î¨ : A â†’ uPred M) : (â–¡ âˆƒ a, Î¨ a) âŠ£âŠ¢ (âˆƒ a, â–¡ Î¨ a).
-Proof.
-  apply (anti_symm _); auto using always_exist_1.
-  apply exist_elim=> x. by rewrite (exist_intro x).
-Qed.
-Lemma always_and P Q : â–¡ (P âˆ§ Q) âŠ£âŠ¢ â–¡ P âˆ§ â–¡ Q.
-Proof. rewrite !and_alt always_forall. by apply forall_proper=> -[]. Qed.
-Lemma always_or P Q : â–¡ (P âˆ¨ Q) âŠ£âŠ¢ â–¡ P âˆ¨ â–¡ Q.
-Proof. rewrite !or_alt always_exist. by apply exist_proper=> -[]. Qed.
-Lemma always_impl P Q : â–¡ (P â†’ Q) âŠ¢ â–¡ P â†’ â–¡ Q.
-Proof.
-  apply impl_intro_l; rewrite -always_and.
-  apply always_mono, impl_elim with P; auto.
-Qed.
-Lemma always_eq {A:cofeT} (a b : A) : â–¡ (a â‰¡ b) âŠ£âŠ¢ a â‰¡ b.
-Proof.
-  apply (anti_symm (âŠ¢)); auto using always_elim.
-  apply (eq_rewrite a b (Î» b, â–¡ (a â‰¡ b))%I); auto.
-  { intros n; solve_proper. }
-  rewrite -(eq_refl a) always_pure; auto.
-Qed.
-
-Lemma always_and_sep P Q : â–¡ (P âˆ§ Q) âŠ£âŠ¢ â–¡ (P â˜… Q).
-Proof. apply (anti_symm (âŠ¢)); auto using always_and_sep_1. Qed.
-Lemma always_and_sep_l' P Q : â–¡ P âˆ§ Q âŠ£âŠ¢ â–¡ P â˜… Q.
-Proof. apply (anti_symm (âŠ¢)); auto using always_and_sep_l_1. Qed.
-Lemma always_and_sep_r' P Q : P âˆ§ â–¡ Q âŠ£âŠ¢ P â˜… â–¡ Q.
-Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
-Lemma always_sep P Q : â–¡ (P â˜… Q) âŠ£âŠ¢ â–¡ P â˜… â–¡ Q.
-Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
-Lemma always_sep_dup' P : â–¡ P âŠ£âŠ¢ â–¡ P â˜… â–¡ P.
-Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.
-
-Lemma always_wand P Q : â–¡ (P -â˜… Q) âŠ¢ â–¡ P -â˜… â–¡ Q.
-Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
-Lemma always_wand_impl P Q : â–¡ (P -â˜… Q) âŠ£âŠ¢ â–¡ (P â†’ Q).
-Proof.
-  apply (anti_symm (âŠ¢)); [|by rewrite -impl_wand].
-  apply always_intro', impl_intro_r.
-  by rewrite always_and_sep_l' always_elim wand_elim_l.
-Qed.
-Lemma always_entails_l' P Q : (P âŠ¢ â–¡ Q) â†’ P âŠ¢ â–¡ Q â˜… P.
-Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
-Lemma always_entails_r' P Q : (P âŠ¢ â–¡ Q) â†’ P âŠ¢ P â˜… â–¡ Q.
-Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
-
-(* Later *)
-Lemma later_mono P Q : (P âŠ¢ Q) â†’ â–· P âŠ¢ â–· Q.
-Proof.
-  unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
-Qed.
-Lemma lÃ¶b P : (â–· P â†’ P) âŠ¢ P.
-Proof.
-  unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|].
-  apply HP, IH, uPred_closed with (S n); eauto using cmra_validN_S.
-Qed.
-Lemma later_forall_2 {A} (Î¦ : A â†’ uPred M) : (âˆ€ a, â–· Î¦ a) âŠ¢ â–· âˆ€ a, Î¦ a.
-Proof. unseal; by split=> -[|n] x. Qed.
-Lemma later_exist_false {A} (Î¦ : A â†’ uPred M) :
-  (â–· âˆƒ a, Î¦ a) âŠ¢ â–· False âˆ¨ (âˆƒ a, â–· Î¦ a).
-Proof. unseal; split=> -[|[|n]] x /=; eauto. Qed.
-Lemma later_sep P Q : â–· (P â˜… Q) âŠ£âŠ¢ â–· P â˜… â–· Q.
-Proof.
-  unseal; split=> n x ?; split.
-  - destruct n as [|n]; simpl.
-    { by exists x, (core x); rewrite cmra_core_r. }
-    intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
-      as (y1&y2&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
-    exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
-  - destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
-    exists x1, x2; eauto using dist_S.
-Qed.
-Lemma later_false_excluded_middle P : â–· P âŠ¢ â–· False âˆ¨ (â–· False â†’ P).
-Proof.
-  unseal; split=> -[|n] x ? /= HP; [by left|right].
-  intros [|n'] x' ????; [|done].
-  eauto using uPred_closed, uPred_mono, cmra_included_includedN.
-Qed.
-
-Lemma always_later P : â–¡ â–· P âŠ£âŠ¢ â–· â–¡ P.
-Proof. by unseal. Qed.
-
-
-(* Later derived *)
-Lemma later_proper P Q : (P âŠ£âŠ¢ Q) â†’ â–· P âŠ£âŠ¢ â–· Q.
-Proof. by intros ->. Qed.
-Hint Resolve later_mono later_proper.
-Global Instance later_mono' : Proper ((âŠ¢) ==> (âŠ¢)) (@uPred_later M).
-Proof. intros P Q; apply later_mono. Qed.
-Global Instance later_flip_mono' :
-  Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_later M).
-Proof. intros P Q; apply later_mono. Qed.
-
-Lemma later_intro P : P âŠ¢ â–· P.
-Proof.
-  rewrite -(and_elim_l (â–· P) P) -(lÃ¶b (â–· P âˆ§ P)).
-  apply impl_intro_l. by rewrite {1}(and_elim_r (â–· P)).
-Qed.
-
-Lemma later_True : â–· True âŠ£âŠ¢ True.
-Proof. apply (anti_symm (âŠ¢)); auto using later_intro. Qed.
-Lemma later_forall {A} (Î¦ : A â†’ uPred M) : (â–· âˆ€ a, Î¦ a) âŠ£âŠ¢ (âˆ€ a, â–· Î¦ a).
-Proof.
-  apply (anti_symm _); auto using later_forall_2.
-  apply forall_intro=> x. by rewrite (forall_elim x).
-Qed.
-Lemma later_exist `{Inhabited A} (Î¦ : A â†’ uPred M) :
-  â–· (âˆƒ a, Î¦ a) âŠ£âŠ¢ (âˆƒ a, â–· Î¦ a).
-Proof.
-  apply: anti_symm; [|apply exist_elim; eauto using exist_intro].
-  rewrite later_exist_false. apply or_elim; last done.
-  rewrite -(exist_intro inhabitant); auto.
-Qed.
-Lemma later_and P Q : â–· (P âˆ§ Q) âŠ£âŠ¢ â–· P âˆ§ â–· Q.
-Proof. rewrite !and_alt later_forall. by apply forall_proper=> -[]. Qed.
-Lemma later_or P Q : â–· (P âˆ¨ Q) âŠ£âŠ¢ â–· P âˆ¨ â–· Q.
-Proof. rewrite !or_alt later_exist. by apply exist_proper=> -[]. Qed.
-Lemma later_impl P Q : â–· (P â†’ Q) âŠ¢ â–· P â†’ â–· Q.
-Proof. apply impl_intro_l; rewrite -later_and; eauto using impl_elim. Qed.
-Lemma later_wand P Q : â–· (P -â˜… Q) âŠ¢ â–· P -â˜… â–· Q.
-Proof. apply wand_intro_r; rewrite -later_sep; eauto using wand_elim_l. Qed.
-Lemma later_iff P Q : â–· (P â†” Q) âŠ¢ â–· P â†” â–· Q.
-Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
-
-
-(* Conditional always *)
-Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
-Proof. solve_proper. Qed.
-Global Instance always_if_proper p : Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_always_if M p).
-Proof. solve_proper. Qed.
-Global Instance always_if_mono p : Proper ((âŠ¢) ==> (âŠ¢)) (@uPred_always_if M p).
-Proof. solve_proper. Qed.
-
-Lemma always_if_elim p P : â–¡?p P âŠ¢ P.
-Proof. destruct p; simpl; auto using always_elim. Qed.
-Lemma always_elim_if p P : â–¡ P âŠ¢ â–¡?p P.
-Proof. destruct p; simpl; auto using always_elim. Qed.
-
-Lemma always_if_pure p Ï† : â–¡?p â–  Ï† âŠ£âŠ¢ â–  Ï†.
-Proof. destruct p; simpl; auto using always_pure. Qed.
-Lemma always_if_and p P Q : â–¡?p (P âˆ§ Q) âŠ£âŠ¢ â–¡?p P âˆ§ â–¡?p Q.
-Proof. destruct p; simpl; auto using always_and. Qed.
-Lemma always_if_or p P Q : â–¡?p (P âˆ¨ Q) âŠ£âŠ¢ â–¡?p P âˆ¨ â–¡?p Q.
-Proof. destruct p; simpl; auto using always_or. Qed.
-Lemma always_if_exist {A} p (Î¨ : A â†’ uPred M) : (â–¡?p âˆƒ a, Î¨ a) âŠ£âŠ¢ âˆƒ a, â–¡?p Î¨ a.
-Proof. destruct p; simpl; auto using always_exist. Qed.
-Lemma always_if_sep p P Q : â–¡?p (P â˜… Q) âŠ£âŠ¢ â–¡?p P â˜… â–¡?p Q.
-Proof. destruct p; simpl; auto using always_sep. Qed.
-Lemma always_if_later p P : â–¡?p â–· P âŠ£âŠ¢ â–· â–¡?p P.
-Proof. destruct p; simpl; auto using always_later. Qed.
-
-
-(* True now *)
-Global Instance except_last_ne n : Proper (dist n ==> dist n) (@uPred_except_last M).
-Proof. solve_proper. Qed.
-Global Instance except_last_proper : Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_except_last M).
-Proof. solve_proper. Qed.
-Global Instance except_last_mono' : Proper ((âŠ¢) ==> (âŠ¢)) (@uPred_except_last M).
-Proof. solve_proper. Qed.
-Global Instance except_last_flip_mono' :
-  Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_except_last M).
-Proof. solve_proper. Qed.
-
-Lemma except_last_intro P : P âŠ¢ â—‡ P.
-Proof. rewrite /uPred_except_last; auto. Qed.
-Lemma except_last_mono P Q : (P âŠ¢ Q) â†’ â—‡ P âŠ¢ â—‡ Q.
-Proof. by intros ->. Qed.
-Lemma except_last_idemp P : â—‡ â—‡ P âŠ¢ â—‡ P.
-Proof. rewrite /uPred_except_last; auto. Qed.
-
-Lemma except_last_True : â—‡ True âŠ£âŠ¢ True.
-Proof. rewrite /uPred_except_last. apply (anti_symm _); auto. Qed.
-Lemma except_last_or P Q : â—‡ (P âˆ¨ Q) âŠ£âŠ¢ â—‡ P âˆ¨ â—‡ Q.
-Proof. rewrite /uPred_except_last. apply (anti_symm _); auto. Qed.
-Lemma except_last_and P Q : â—‡ (P âˆ§ Q) âŠ£âŠ¢ â—‡ P âˆ§ â—‡ Q.
-Proof. by rewrite /uPred_except_last or_and_l. Qed.
-Lemma except_last_sep P Q : â—‡ (P â˜… Q) âŠ£âŠ¢ â—‡ P â˜… â—‡ Q.
-Proof.
-  rewrite /uPred_except_last. apply (anti_symm _).
-  - apply or_elim; last by auto.
-    by rewrite -!or_intro_l -always_pure -always_later -always_sep_dup'.
-  - rewrite sep_or_r sep_elim_l sep_or_l; auto.
-Qed.
-Lemma except_last_forall {A} (Î¦ : A â†’ uPred M) : â—‡ (âˆ€ a, Î¦ a) âŠ¢ âˆ€ a, â—‡ Î¦ a.
-Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
-Lemma except_last_exist {A} (Î¦ : A â†’ uPred M) : (âˆƒ a, â—‡ Î¦ a) âŠ¢ â—‡ âˆƒ a, Î¦ a.
-Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
-Lemma except_last_later P : â—‡ â–· P âŠ¢ â–· P.
-Proof. by rewrite /uPred_except_last -later_or False_or. Qed.
-Lemma except_last_always P : â—‡ â–¡ P âŠ£âŠ¢ â–¡ â—‡ P.
-Proof. by rewrite /uPred_except_last always_or always_later always_pure. Qed.
-Lemma except_last_always_if p P : â—‡ â–¡?p P âŠ£âŠ¢ â–¡?p â—‡ P.
-Proof. destruct p; simpl; auto using except_last_always. Qed.
-Lemma except_last_frame_l P Q : P â˜… â—‡ Q âŠ¢ â—‡ (P â˜… Q).
-Proof. by rewrite {1}(except_last_intro P) except_last_sep. Qed.
-Lemma except_last_frame_r P Q : â—‡ P â˜… Q âŠ¢ â—‡ (P â˜… Q).
-Proof. by rewrite {1}(except_last_intro Q) except_last_sep. Qed.
-
-(* Own *)
-Lemma ownM_op (a1 a2 : M) :
-  uPred_ownM (a1 â‹… a2) âŠ£âŠ¢ uPred_ownM a1 â˜… uPred_ownM a2.
-Proof.
-  unseal; split=> n x ?; split.
-  - intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
-    split. by exists (core a1); rewrite cmra_core_r. by exists z.
-  - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
-    by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-      -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
-Qed.
-Lemma always_ownM_core (a : M) : uPred_ownM a âŠ¢ â–¡ uPred_ownM (core a).
-Proof.
-  split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
-Qed.
-Lemma ownM_empty : True âŠ¢ uPred_ownM âˆ….
-Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
-Lemma later_ownM a : â–· uPred_ownM a âŠ¢ âˆƒ b, uPred_ownM b âˆ§ â–· (a â‰¡ b).
-Proof.
-  unseal; split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
-  destruct Hax as [y ?].
-  destruct (cmra_extend n x a y) as (a'&y'&Hx&?&?); auto using cmra_validN_S.
-  exists a'. rewrite Hx. eauto using cmra_includedN_l.
-Qed.
-
-(* Valid *)
-Lemma ownM_valid (a : M) : uPred_ownM a âŠ¢ âœ“ a.
-Proof.
-  unseal; split=> n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l.
-Qed.
-Lemma cmra_valid_intro {A : cmraT} (a : A) : âœ“ a â†’ True âŠ¢ âœ“ a.
-Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
-Lemma cmra_valid_elim {A : cmraT} (a : A) : Â¬ âœ“{0} a â†’ âœ“ a âŠ¢ False.
-Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma always_cmra_valid_1 {A : cmraT} (a : A) : âœ“ a âŠ¢ â–¡ âœ“ a.
-Proof. by unseal. Qed.
-Lemma cmra_valid_weaken {A : cmraT} (a b : A) : âœ“ (a â‹… b) âŠ¢ âœ“ a.
-Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
-
-(* Own and valid derived *)
-Lemma always_ownM (a : M) : Persistent a â†’ â–¡ uPred_ownM a âŠ£âŠ¢ uPred_ownM a.
-Proof.
-  intros; apply (anti_symm _); first by apply:always_elim.
-  by rewrite {1}always_ownM_core persistent_core.
-Qed.
-Lemma ownM_invalid (a : M) : Â¬ âœ“{0} a â†’ uPred_ownM a âŠ¢ False.
-Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
-Global Instance ownM_mono : Proper (flip (â‰¼) ==> (âŠ¢)) (@uPred_ownM M).
-Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
-Lemma ownM_empty' : uPred_ownM âˆ… âŠ£âŠ¢ True.
-Proof. apply (anti_symm _); auto using ownM_empty. Qed.
-Lemma always_cmra_valid {A : cmraT} (a : A) : â–¡ âœ“ a âŠ£âŠ¢ âœ“ a.
-  intros; apply (anti_symm _); first by apply:always_elim.
-  apply:always_cmra_valid_1.
-Qed.
-
-(* Basic update modality *)
-Lemma bupd_intro P : P ==â˜… P.
-Proof.
-  unseal. split=> n x ? HP k yf ?; exists x; split; first done.
-  apply uPred_closed with n; eauto using cmra_validN_op_l.
-Qed.
-Lemma bupd_mono P Q : (P âŠ¢ Q) â†’ (|==> P) ==â˜… Q.
-Proof.
-  unseal. intros HPQ; split=> n x ? HP k yf ??.
-  destruct (HP k yf) as (x'&?&?); eauto.
-  exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
-Qed.
-Lemma bupd_trans P : (|==> |==> P) ==â˜… P.
-Proof. unseal; split; naive_solver. Qed.
-Lemma bupd_frame_r P R : (|==> P) â˜… R ==â˜… P â˜… R.
-Proof.
-  unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
-  destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto.
-  { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
-  exists (x' â‹… x2); split; first by rewrite -assoc.
-  exists x', x2; split_and?; auto.
-  apply uPred_closed with n; eauto 3 using cmra_validN_op_l, cmra_validN_op_r.
-Qed.
-Lemma bupd_ownM_updateP x (Î¦ : M â†’ Prop) :
-  x ~~>: Î¦ â†’ uPred_ownM x ==â˜… âˆƒ y, â–  Î¦ y âˆ§ uPred_ownM y.
-Proof.
-  unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
-  destruct (Hup k (Some (x3 â‹… yf))) as (y&?&?); simpl in *.
-  { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. }
-  exists (y â‹… x3); split; first by rewrite -assoc.
-  exists y; eauto using cmra_includedN_l.
-Qed.
-
-(** * Derived rules *)
-Global Instance bupd_mono' : Proper ((âŠ¢) ==> (âŠ¢)) (@uPred_bupd M).
-Proof. intros P Q; apply bupd_mono. Qed.
-Global Instance bupd_flip_mono' : Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_bupd M).
-Proof. intros P Q; apply bupd_mono. Qed.
-Lemma bupd_frame_l R Q : (R â˜… |==> Q) ==â˜… R â˜… Q.
-Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
-Lemma bupd_wand_l P Q : (P -â˜… Q) â˜… (|==> P) ==â˜… Q.
-Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
-Lemma bupd_wand_r P Q : (|==> P) â˜… (P -â˜… Q) ==â˜… Q.
-Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
-Lemma bupd_sep P Q : (|==> P) â˜… (|==> Q) ==â˜… P â˜… Q.
-Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
-Lemma bupd_ownM_update x y : x ~~> y â†’ uPred_ownM x âŠ¢ |==> uPred_ownM y.
-Proof.
-  intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
-  by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
-Qed.
-Lemma except_last_bupd P : â—‡ (|==> P) âŠ¢ (|==> â—‡ P).
-Proof.
-  rewrite /uPred_except_last. apply or_elim; auto using bupd_mono.
-  by rewrite -bupd_intro -or_intro_l.
-Qed.
-
-(* Products *)
-Lemma prod_equivI {A B : cofeT} (x y : A * B) : x â‰¡ y âŠ£âŠ¢ x.1 â‰¡ y.1 âˆ§ x.2 â‰¡ y.2.
-Proof. by unseal. Qed.
-Lemma prod_validI {A B : cmraT} (x : A * B) : âœ“ x âŠ£âŠ¢ âœ“ x.1 âˆ§ âœ“ x.2.
-Proof. by unseal. Qed.
-
-(* Later *)
-Lemma later_equivI {A : cofeT} (x y : A) : Next x â‰¡ Next y âŠ£âŠ¢ â–· (x â‰¡ y).
-Proof. by unseal. Qed.
-
-(* Discrete *)
-Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : âœ“ a âŠ£âŠ¢ â–  âœ“ a.
-Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
-Lemma timeless_eq {A : cofeT} (a b : A) : Timeless a â†’ a â‰¡ b âŠ£âŠ¢ â–  (a â‰¡ b).
-Proof.
-  unseal=> ?. apply (anti_symm (âŠ¢)); split=> n x ?; by apply (timeless_iff n).
-Qed.
-
-(* Option *)
-Lemma option_equivI {A : cofeT} (mx my : option A) :
-  mx â‰¡ my âŠ£âŠ¢ match mx, my with
-             | Some x, Some y => x â‰¡ y | None, None => True | _, _ => False
-             end.
-Proof.
-  uPred.unseal. do 2 split. by destruct 1. by destruct mx, my; try constructor.
-Qed.
-Lemma option_validI {A : cmraT} (mx : option A) :
-  âœ“ mx âŠ£âŠ¢ match mx with Some x => âœ“ x | None => True end.
-Proof. uPred.unseal. by destruct mx. Qed.
-
-(* Functions *)
-Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f â‰¡ g âŠ£âŠ¢ âˆ€ x, f x â‰¡ g x.
-Proof. by uPred.unseal. Qed.
-Lemma cofe_moreC_equivI {A B : cofeT} (f g : A -n> B) : f â‰¡ g âŠ£âŠ¢ âˆ€ x, f x â‰¡ g x.
-Proof. by uPred.unseal. Qed.
-
-(* Timeless instances *)
-Global Instance pure_timeless Ï† : TimelessP (â–  Ï† : uPred M)%I.
-Proof.
-  rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True.
-Qed.
-Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
-  TimelessP (âœ“ a : uPred M)%I.
-Proof. rewrite /TimelessP !discrete_valid. apply (timelessP _). Qed.
-Global Instance and_timeless P Q: TimelessP P â†’ TimelessP Q â†’ TimelessP (P âˆ§ Q).
-Proof. intros; rewrite /TimelessP except_last_and later_and; auto. Qed.
-Global Instance or_timeless P Q : TimelessP P â†’ TimelessP Q â†’ TimelessP (P âˆ¨ Q).
-Proof. intros; rewrite /TimelessP except_last_or later_or; auto. Qed.
-Global Instance impl_timeless P Q : TimelessP Q â†’ TimelessP (P â†’ Q).
-Proof.
-  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
-  apply or_mono, impl_intro_l; first done.
-  rewrite -{2}(lÃ¶b Q); apply impl_intro_l.
-  rewrite HQ /uPred_except_last !and_or_r. apply or_elim; last auto.
-  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
-Qed.
-Global Instance sep_timeless P Q: TimelessP P â†’ TimelessP Q â†’ TimelessP (P â˜… Q).
-Proof. intros; rewrite /TimelessP except_last_sep later_sep; auto. Qed.
-Global Instance wand_timeless P Q : TimelessP Q â†’ TimelessP (P -â˜… Q).
-Proof.
-  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
-  apply or_mono, wand_intro_l; first done.
-  rewrite -{2}(lÃ¶b Q); apply impl_intro_l.
-  rewrite HQ /uPred_except_last !and_or_r. apply or_elim; last auto.
-  rewrite -(always_pure) -always_later always_and_sep_l'.
-  by rewrite assoc (comm _ _ P) -assoc -always_and_sep_l' impl_elim_r wand_elim_r.
-Qed.
-Global Instance forall_timeless {A} (Î¨ : A â†’ uPred M) :
-  (âˆ€ x, TimelessP (Î¨ x)) â†’ TimelessP (âˆ€ x, Î¨ x).
-Proof.
-  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
-  apply or_mono; first done. apply forall_intro=> x.
-  rewrite -(lÃ¶b (Î¨ x)); apply impl_intro_l.
-  rewrite HQ /uPred_except_last !and_or_r. apply or_elim; last auto.
-  by rewrite impl_elim_r (forall_elim x).
-Qed.
-Global Instance exist_timeless {A} (Î¨ : A â†’ uPred M) :
-  (âˆ€ x, TimelessP (Î¨ x)) â†’ TimelessP (âˆƒ x, Î¨ x).
-Proof.
-  rewrite /TimelessP=> ?. rewrite later_exist_false. apply or_elim.
-  - rewrite /uPred_except_last; auto.
-  - apply exist_elim=> x. rewrite -(exist_intro x); auto.
-Qed.
-Global Instance always_timeless P : TimelessP P â†’ TimelessP (â–¡ P).
-Proof. intros; rewrite /TimelessP except_last_always -always_later; auto. Qed.
-Global Instance always_if_timeless p P : TimelessP P â†’ TimelessP (â–¡?p P).
-Proof. destruct p; apply _. Qed.
-Global Instance eq_timeless {A : cofeT} (a b : A) :
-  Timeless a â†’ TimelessP (a â‰¡ b : uPred M)%I.
-Proof. intros. rewrite /TimelessP !timeless_eq. apply (timelessP _). Qed.
-Global Instance ownM_timeless (a : M) : Timeless a â†’ TimelessP (uPred_ownM a).
-Proof.
-  intros ?. rewrite /TimelessP later_ownM. apply exist_elim=> b.
-  rewrite (timelessP (aâ‰¡b)) (except_last_intro (uPred_ownM b)) -except_last_and.
-  apply except_last_mono. rewrite eq_sym.
-  apply (eq_rewrite b a (uPred_ownM)); first apply _; auto.
-Qed.
-
-(* Persistence *)
-Global Instance pure_persistent Ï† : PersistentP (â–  Ï† : uPred M)%I.
-Proof. by rewrite /PersistentP always_pure. Qed.
-Global Instance always_persistent P : PersistentP (â–¡ P).
-Proof. by intros; apply always_intro'. Qed.
-Global Instance and_persistent P Q :
-  PersistentP P â†’ PersistentP Q â†’ PersistentP (P âˆ§ Q).
-Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed.
-Global Instance or_persistent P Q :
-  PersistentP P â†’ PersistentP Q â†’ PersistentP (P âˆ¨ Q).
-Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
-Global Instance sep_persistent P Q :
-  PersistentP P â†’ PersistentP Q â†’ PersistentP (P â˜… Q).
-Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
-Global Instance forall_persistent {A} (Î¨ : A â†’ uPred M) :
-  (âˆ€ x, PersistentP (Î¨ x)) â†’ PersistentP (âˆ€ x, Î¨ x).
-Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
-Global Instance exist_persistent {A} (Î¨ : A â†’ uPred M) :
-  (âˆ€ x, PersistentP (Î¨ x)) â†’ PersistentP (âˆƒ x, Î¨ x).
-Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
-Global Instance eq_persistent {A : cofeT} (a b : A) :
-  PersistentP (a â‰¡ b : uPred M)%I.
-Proof. by intros; rewrite /PersistentP always_eq. Qed.
-Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
-  PersistentP (âœ“ a : uPred M)%I.
-Proof. by intros; rewrite /PersistentP always_cmra_valid. Qed.
-Global Instance later_persistent P : PersistentP P â†’ PersistentP (â–· P).
-Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
-Global Instance ownM_persistent : Persistent a â†’ PersistentP (@uPred_ownM M a).
-Proof. intros. by rewrite /PersistentP always_ownM. Qed.
-Global Instance from_option_persistent {A} P (Î¨ : A â†’ uPred M) (mx : option A) :
-  (âˆ€ x, PersistentP (Î¨ x)) â†’ PersistentP P â†’ PersistentP (from_option Î¨ P mx).
-Proof. destruct mx; apply _. Qed.
-
-(* Derived lemmas for persistence *)
-Lemma always_always P `{!PersistentP P} : â–¡ P âŠ£âŠ¢ P.
-Proof. apply (anti_symm (âŠ¢)); auto using always_elim. Qed.
-Lemma always_if_always p P `{!PersistentP P} : â–¡?p P âŠ£âŠ¢ P.
-Proof. destruct p; simpl; auto using always_always. Qed.
-Lemma always_intro P Q `{!PersistentP P} : (P âŠ¢ Q) â†’ P âŠ¢ â–¡ Q.
-Proof. rewrite -(always_always P); apply always_intro'. Qed.
-Lemma always_and_sep_l P Q `{!PersistentP P} : P âˆ§ Q âŠ£âŠ¢ P â˜… Q.
-Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
-Lemma always_and_sep_r P Q `{!PersistentP Q} : P âˆ§ Q âŠ£âŠ¢ P â˜… Q.
-Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
-Lemma always_sep_dup P `{!PersistentP P} : P âŠ£âŠ¢ P â˜… P.
-Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
-Lemma always_entails_l P Q `{!PersistentP Q} : (P âŠ¢ Q) â†’ P âŠ¢ Q â˜… P.
-Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
-Lemma always_entails_r P Q `{!PersistentP Q} : (P âŠ¢ Q) â†’ P âŠ¢ P â˜… Q.
-Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
-
-(** Consistency and adequancy statements *)
-Lemma adequacy Ï† n : (True âŠ¢ Nat.iter n (Î» P, |==> â–· P) (â–  Ï†)) â†’ Ï†.
-Proof.
-  cut (âˆ€ x, âœ“{n} x â†’ Nat.iter n (Î» P, |==> â–· P)%I (â–  Ï†)%I n x â†’ Ï†).
-  { intros help H. eapply (help âˆ…); eauto using ucmra_unit_validN.
-    eapply H; try unseal; eauto using ucmra_unit_validN. }
-  unseal. induction n as [|n IH]=> x Hx Hupd; auto.
-  destruct (Hupd (S n) âˆ…) as (x'&?&?); rewrite ?right_id; auto.
-  eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
-Qed.
-
-Corollary consistency_modal n : Â¬ (True âŠ¢ Nat.iter n (Î» P, |==> â–· P) False).
-Proof. exact (adequacy False n). Qed.
-
-Corollary consistency : Â¬ (True âŠ¢ False).
-Proof. exact (consistency_modal 0). Qed.
-End uPred_logic.
-
-(* Hint DB for the logic *)
-Hint Resolve pure_intro.
-Hint Resolve or_elim or_intro_l' or_intro_r' : I.
-Hint Resolve and_intro and_elim_l' and_elim_r' : I.
-Hint Resolve always_mono : I.
-Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
-Hint Immediate True_intro False_elim : I.
-Hint Immediate iff_refl eq_refl' : I.
-End uPred.
-
-Import uPred.
-
-(* CMRA structure on uPred *)
-Section cmra.
-  Context {M : ucmraT}.
-
-  Instance uPred_valid : Valid (uPred M) := Î» P, âˆ€ n x, âœ“{n} x â†’ P n x.
-  Instance uPred_validN : ValidN (uPred M) := Î» n P,
-    âˆ€ n' x, n' â‰¤ n â†’ âœ“{n'} x â†’ P n' x.
-  Instance uPred_op : Op (uPred M) := uPred_sep.
-  Instance uPred_pcore : PCore (uPred M) := Î» _, Some True%I.
-
-  Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN n).
-  Proof. intros P Q HPQ; split=> H n' x ??; by apply HPQ, H. Qed.
-
-  Lemma uPred_validN_alt n (P : uPred M) : âœ“{n} P â†’ P â‰¡{n}â‰¡ True%I.
-  Proof.
-    unseal=> HP; split=> n' x ??; split; [done|].
-    intros _. by apply HP.
-  Qed.
-
-  Lemma uPred_cmra_validN_op_l n P Q : âœ“{n} (P â˜… Q)%I â†’ âœ“{n} P.
-  Proof.
-    unseal. intros HPQ n' x ??.
-    destruct (HPQ n' x) as (x1&x2&->&?&?); auto.
-    eapply uPred_mono with x1; eauto using cmra_includedN_l.
-  Qed.
-
-  Lemma uPred_included P Q : P â‰¼ Q â†’ Q âŠ¢ P.
-  Proof. intros [P' ->]. apply sep_elim_l. Qed.
-
-  Definition uPred_cmra_mixin : CMRAMixin (uPred M).
-  Proof.
-    apply cmra_total_mixin; try apply _ || by eauto.
-    - intros n P Q ??. by cofe_subst.
-    - intros P; split.
-      + intros HP n n' x ?. apply HP.
-      + intros HP n x. by apply (HP n).
-    - intros n P HP n' x ?. apply HP; auto.
-    - intros P. by rewrite left_id.
-    - intros P Q _. exists True%I. by rewrite left_id.
-    - intros n P Q. apply uPred_cmra_validN_op_l.
-    - intros n P Q1 Q2 HP HPQ. exists True%I, P; split_and!.
-      + by rewrite left_id.
-      + move: HP; by rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt.
-      + move: HP; rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt=> ->.
-        by rewrite left_id.
-  Qed.
-
-  Canonical Structure uPredR :=
-    CMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin.
-
-  Instance uPred_empty : Empty (uPred M) := True%I.
-
-  Definition uPred_ucmra_mixin : UCMRAMixin (uPred M).
-  Proof.
-    split; last done.
-    - by rewrite /empty /uPred_empty uPred_pure_eq.
-    - intros P. by rewrite left_id.
-  Qed.
-
-  Canonical Structure uPredUR :=
-    UCMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.
-
-  Global Instance uPred_always_homomorphism : UCMRAHomomorphism uPred_always.
-  Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.
-  Global Instance uPred_always_if_homomorphism b :
-    UCMRAHomomorphism (uPred_always_if b).
-  Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed.
-  Global Instance uPred_later_homomorphism : UCMRAHomomorphism uPred_later.
-  Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed.
-  Global Instance uPred_except_last_homomorphism :
-    CMRAHomomorphism uPred_except_last.
-  Proof. split. apply _. apply except_last_sep. Qed.
-  Global Instance uPred_ownM_homomorphism : UCMRAHomomorphism uPred_ownM.
-  Proof. split; [split|]. apply _. apply ownM_op. apply ownM_empty'. Qed.
-End cmra.
-
-Arguments uPredR : clear implicits.
-Arguments uPredUR : clear implicits.
diff --git a/base_logic/base_logic.v b/base_logic/base_logic.v
new file mode 100644
index 000000000..31e643b15
--- /dev/null
+++ b/base_logic/base_logic.v
@@ -0,0 +1,17 @@
+From iris.base_logic Require Export derived.
+
+Module uPred.
+  Include uPred_entails.
+  Include uPred_primitive.
+  Include uPred_derived.
+End uPred.
+
+(* Hint DB for the logic *)
+Import uPred.
+Hint Resolve pure_intro.
+Hint Resolve or_elim or_intro_l' or_intro_r' : I.
+Hint Resolve and_intro and_elim_l' and_elim_r' : I.
+Hint Resolve always_mono : I.
+Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
+Hint Immediate True_intro False_elim : I.
+Hint Immediate iff_refl eq_refl' : I.
diff --git a/algebra/upred_big_op.v b/base_logic/big_op.v
similarity index 85%
rename from algebra/upred_big_op.v
rename to base_logic/big_op.v
index 9f2dded3d..214c9e69e 100644
--- a/algebra/upred_big_op.v
+++ b/base_logic/big_op.v
@@ -1,7 +1,89 @@
-From iris.algebra Require Export upred list cmra_big_op.
+From iris.algebra Require Export list cmra_big_op.
+From iris.base_logic Require Export base_logic.
 From iris.prelude Require Import gmap fin_collections functions.
 Import uPred.
 
+(* We make use of the bigops on CMRAs, so we first define a (somewhat ad-hoc)
+CMRA structure on uPred. *)
+Section cmra.
+  Context {M : ucmraT}.
+
+  Instance uPred_valid : Valid (uPred M) := Î» P, âˆ€ n x, âœ“{n} x â†’ P n x.
+  Instance uPred_validN : ValidN (uPred M) := Î» n P,
+    âˆ€ n' x, n' â‰¤ n â†’ âœ“{n'} x â†’ P n' x.
+  Instance uPred_op : Op (uPred M) := uPred_sep.
+  Instance uPred_pcore : PCore (uPred M) := Î» _, Some True%I.
+
+  Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN n).
+  Proof. intros P Q HPQ; split=> H n' x ??; by apply HPQ, H. Qed.
+
+  Lemma uPred_validN_alt n (P : uPred M) : âœ“{n} P â†’ P â‰¡{n}â‰¡ True%I.
+  Proof.
+    unseal=> HP; split=> n' x ??; split; [done|].
+    intros _. by apply HP.
+  Qed.
+
+  Lemma uPred_cmra_validN_op_l n P Q : âœ“{n} (P â˜… Q)%I â†’ âœ“{n} P.
+  Proof.
+    unseal. intros HPQ n' x ??.
+    destruct (HPQ n' x) as (x1&x2&->&?&?); auto.
+    eapply uPred_mono with x1; eauto using cmra_includedN_l.
+  Qed.
+
+  Lemma uPred_included P Q : P â‰¼ Q â†’ Q âŠ¢ P.
+  Proof. intros [P' ->]. apply sep_elim_l. Qed.
+
+  Definition uPred_cmra_mixin : CMRAMixin (uPred M).
+  Proof.
+    apply cmra_total_mixin; try apply _ || by eauto.
+    - intros n P Q ??. by cofe_subst.
+    - intros P; split.
+      + intros HP n n' x ?. apply HP.
+      + intros HP n x. by apply (HP n).
+    - intros n P HP n' x ?. apply HP; auto.
+    - intros P. by rewrite left_id.
+    - intros P Q _. exists True%I. by rewrite left_id.
+    - intros n P Q. apply uPred_cmra_validN_op_l.
+    - intros n P Q1 Q2 HP HPQ. exists True%I, P; split_and!.
+      + by rewrite left_id.
+      + move: HP; by rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt.
+      + move: HP; rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt=> ->.
+        by rewrite left_id.
+  Qed.
+
+  Canonical Structure uPredR :=
+    CMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin.
+
+  Instance uPred_empty : Empty (uPred M) := True%I.
+
+  Definition uPred_ucmra_mixin : UCMRAMixin (uPred M).
+  Proof.
+    split; last done.
+    - by rewrite /empty /uPred_empty uPred_pure_eq.
+    - intros P. by rewrite left_id.
+  Qed.
+
+  Canonical Structure uPredUR :=
+    UCMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.
+
+  Global Instance uPred_always_homomorphism : UCMRAHomomorphism uPred_always.
+  Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.
+  Global Instance uPred_always_if_homomorphism b :
+    UCMRAHomomorphism (uPred_always_if b).
+  Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed.
+  Global Instance uPred_later_homomorphism : UCMRAHomomorphism uPred_later.
+  Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed.
+  Global Instance uPred_except_0_homomorphism :
+    CMRAHomomorphism uPred_except_0.
+  Proof. split. apply _. apply except_0_sep. Qed.
+  Global Instance uPred_ownM_homomorphism : UCMRAHomomorphism uPred_ownM.
+  Proof. split; [split|]. apply _. apply ownM_op. apply ownM_empty'. Qed.
+End cmra.
+
+Arguments uPredR : clear implicits.
+Arguments uPredUR : clear implicits.
+
+(* Notations *)
 Notation "'[â˜…]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.
 
 Notation "'[â˜…' 'list' ] k â†¦ x âˆˆ l , P" := (big_opL (M:=uPredUR _) l (Î» k x, P))
diff --git a/base_logic/derived.v b/base_logic/derived.v
new file mode 100644
index 000000000..7cb853696
--- /dev/null
+++ b/base_logic/derived.v
@@ -0,0 +1,751 @@
+From iris.base_logic Require Export primitive.
+Import uPred_entails uPred_primitive.
+
+Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P â†’ Q) âˆ§ (Q â†’ P))%I.
+Instance: Params (@uPred_iff) 1.
+Infix "â†”" := uPred_iff : uPred_scope.
+
+Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
+  (if p then â–¡ P else P)%I.
+Instance: Params (@uPred_always_if) 2.
+Arguments uPred_always_if _ !_ _/.
+Notation "â–¡? p P" := (uPred_always_if p P)
+  (at level 20, p at level 0, P at level 20, format "â–¡? p  P").
+
+Definition uPred_except_last {M} (P : uPred M) : uPred M := â–· False âˆ¨ P.
+Notation "â—‡ P" := (uPred_except_last P)
+  (at level 20, right associativity) : uPred_scope.
+Instance: Params (@uPred_except_last) 1.
+Typeclasses Opaque uPred_except_last.
+
+Class TimelessP {M} (P : uPred M) := timelessP : â–· P âŠ¢ â—‡ P.
+Arguments timelessP {_} _ {_}.
+
+Class PersistentP {M} (P : uPred M) := persistentP : P âŠ¢ â–¡ P.
+Arguments persistentP {_} _ {_}.
+
+Module uPred_derived.
+Section derived.
+Context {M : ucmraT}.
+Implicit Types Ï† : Prop.
+Implicit Types P Q : uPred M.
+Implicit Types A : Type.
+Notation "P âŠ¢ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
+Notation "P âŠ£âŠ¢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *)
+
+(* Derived logical stuff *)
+Lemma False_elim P : False âŠ¢ P.
+Proof. by apply (pure_elim False). Qed.
+Lemma True_intro P : P âŠ¢ True.
+Proof. by apply pure_intro. Qed.
+
+Lemma and_elim_l' P Q R : (P âŠ¢ R) â†’ P âˆ§ Q âŠ¢ R.
+Proof. by rewrite and_elim_l. Qed.
+Lemma and_elim_r' P Q R : (Q âŠ¢ R) â†’ P âˆ§ Q âŠ¢ R.
+Proof. by rewrite and_elim_r. Qed.
+Lemma or_intro_l' P Q R : (P âŠ¢ Q) â†’ P âŠ¢ Q âˆ¨ R.
+Proof. intros ->; apply or_intro_l. Qed.
+Lemma or_intro_r' P Q R : (P âŠ¢ R) â†’ P âŠ¢ Q âˆ¨ R.
+Proof. intros ->; apply or_intro_r. Qed.
+Lemma exist_intro' {A} P (Î¨ : A â†’ uPred M) a : (P âŠ¢ Î¨ a) â†’ P âŠ¢ âˆƒ a, Î¨ a.
+Proof. intros ->; apply exist_intro. Qed.
+Lemma forall_elim' {A} P (Î¨ : A â†’ uPred M) : (P âŠ¢ âˆ€ a, Î¨ a) â†’ âˆ€ a, P âŠ¢ Î¨ a.
+Proof. move=> HP a. by rewrite HP forall_elim. Qed.
+
+Hint Resolve pure_intro.
+Hint Resolve or_elim or_intro_l' or_intro_r'.
+Hint Resolve and_intro and_elim_l' and_elim_r'.
+Hint Immediate True_intro False_elim.
+
+Lemma impl_intro_l P Q R : (Q âˆ§ P âŠ¢ R) â†’ P âŠ¢ Q â†’ R.
+Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
+Lemma impl_elim_l P Q : (P â†’ Q) âˆ§ P âŠ¢ Q.
+Proof. apply impl_elim with P; auto. Qed.
+Lemma impl_elim_r P Q : P âˆ§ (P â†’ Q) âŠ¢ Q.
+Proof. apply impl_elim with P; auto. Qed.
+Lemma impl_elim_l' P Q R : (P âŠ¢ Q â†’ R) â†’ P âˆ§ Q âŠ¢ R.
+Proof. intros; apply impl_elim with Q; auto. Qed.
+Lemma impl_elim_r' P Q R : (Q âŠ¢ P â†’ R) â†’ P âˆ§ Q âŠ¢ R.
+Proof. intros; apply impl_elim with P; auto. Qed.
+Lemma impl_entails P Q : (True âŠ¢ P â†’ Q) â†’ P âŠ¢ Q.
+Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
+Lemma entails_impl P Q : (P âŠ¢ Q) â†’ True âŠ¢ P â†’ Q.
+Proof. auto using impl_intro_l. Qed.
+
+Lemma and_mono P P' Q Q' : (P âŠ¢ Q) â†’ (P' âŠ¢ Q') â†’ P âˆ§ P' âŠ¢ Q âˆ§ Q'.
+Proof. auto. Qed.
+Lemma and_mono_l P P' Q : (P âŠ¢ Q) â†’ P âˆ§ P' âŠ¢ Q âˆ§ P'.
+Proof. by intros; apply and_mono. Qed.
+Lemma and_mono_r P P' Q' : (P' âŠ¢ Q') â†’ P âˆ§ P' âŠ¢ P âˆ§ Q'.
+Proof. by apply and_mono. Qed.
+
+Lemma or_mono P P' Q Q' : (P âŠ¢ Q) â†’ (P' âŠ¢ Q') â†’ P âˆ¨ P' âŠ¢ Q âˆ¨ Q'.
+Proof. auto. Qed.
+Lemma or_mono_l P P' Q : (P âŠ¢ Q) â†’ P âˆ¨ P' âŠ¢ Q âˆ¨ P'.
+Proof. by intros; apply or_mono. Qed.
+Lemma or_mono_r P P' Q' : (P' âŠ¢ Q') â†’ P âˆ¨ P' âŠ¢ P âˆ¨ Q'.
+Proof. by apply or_mono. Qed.
+
+Lemma impl_mono P P' Q Q' : (Q âŠ¢ P) â†’ (P' âŠ¢ Q') â†’ (P â†’ P') âŠ¢ Q â†’ Q'.
+Proof.
+  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
+  apply impl_elim with P; eauto.
+Qed.
+Lemma forall_mono {A} (Î¦ Î¨ : A â†’ uPred M) :
+  (âˆ€ a, Î¦ a âŠ¢ Î¨ a) â†’ (âˆ€ a, Î¦ a) âŠ¢ âˆ€ a, Î¨ a.
+Proof.
+  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
+Qed.
+Lemma exist_mono {A} (Î¦ Î¨ : A â†’ uPred M) :
+  (âˆ€ a, Î¦ a âŠ¢ Î¨ a) â†’ (âˆƒ a, Î¦ a) âŠ¢ âˆƒ a, Î¨ a.
+Proof. intros HÎ¦. apply exist_elim=> a; rewrite (HÎ¦ a); apply exist_intro. Qed.
+
+Global Instance and_mono' : Proper ((âŠ¢) ==> (âŠ¢) ==> (âŠ¢)) (@uPred_and M).
+Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
+Global Instance and_flip_mono' :
+  Proper (flip (âŠ¢) ==> flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_and M).
+Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
+Global Instance or_mono' : Proper ((âŠ¢) ==> (âŠ¢) ==> (âŠ¢)) (@uPred_or M).
+Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
+Global Instance or_flip_mono' :
+  Proper (flip (âŠ¢) ==> flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_or M).
+Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
+Global Instance impl_mono' :
+  Proper (flip (âŠ¢) ==> (âŠ¢) ==> (âŠ¢)) (@uPred_impl M).
+Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
+Global Instance forall_mono' A :
+  Proper (pointwise_relation _ (âŠ¢) ==> (âŠ¢)) (@uPred_forall M A).
+Proof. intros P1 P2; apply forall_mono. Qed.
+Global Instance exist_mono' A :
+  Proper (pointwise_relation _ (âŠ¢) ==> (âŠ¢)) (@uPred_exist M A).
+Proof. intros P1 P2; apply exist_mono. Qed.
+
+Global Instance and_idem : IdemP (âŠ£âŠ¢) (@uPred_and M).
+Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance or_idem : IdemP (âŠ£âŠ¢) (@uPred_or M).
+Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance and_comm : Comm (âŠ£âŠ¢) (@uPred_and M).
+Proof. intros P Q; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance True_and : LeftId (âŠ£âŠ¢) True%I (@uPred_and M).
+Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance and_True : RightId (âŠ£âŠ¢) True%I (@uPred_and M).
+Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance False_and : LeftAbsorb (âŠ£âŠ¢) False%I (@uPred_and M).
+Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance and_False : RightAbsorb (âŠ£âŠ¢) False%I (@uPred_and M).
+Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance True_or : LeftAbsorb (âŠ£âŠ¢) True%I (@uPred_or M).
+Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance or_True : RightAbsorb (âŠ£âŠ¢) True%I (@uPred_or M).
+Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance False_or : LeftId (âŠ£âŠ¢) False%I (@uPred_or M).
+Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance or_False : RightId (âŠ£âŠ¢) False%I (@uPred_or M).
+Proof. intros P; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance and_assoc : Assoc (âŠ£âŠ¢) (@uPred_and M).
+Proof. intros P Q R; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance or_comm : Comm (âŠ£âŠ¢) (@uPred_or M).
+Proof. intros P Q; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance or_assoc : Assoc (âŠ£âŠ¢) (@uPred_or M).
+Proof. intros P Q R; apply (anti_symm (âŠ¢)); auto. Qed.
+Global Instance True_impl : LeftId (âŠ£âŠ¢) True%I (@uPred_impl M).
+Proof.
+  intros P; apply (anti_symm (âŠ¢)).
+  - by rewrite -(left_id True%I uPred_and (_ â†’ _)%I) impl_elim_r.
+  - by apply impl_intro_l; rewrite left_id.
+Qed.
+
+Lemma exists_impl_forall {A} P (Î¨ : A â†’ uPred M) :
+  ((âˆƒ x : A, Î¨ x) â†’ P) âŠ£âŠ¢ âˆ€ x : A, Î¨ x â†’ P.
+Proof.
+  apply equiv_spec; split.
+  - apply forall_intro=>x. by rewrite -exist_intro.
+  - apply impl_intro_r, impl_elim_r', exist_elim=>x.
+    apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r.
+Qed.
+
+Lemma or_and_l P Q R : P âˆ¨ Q âˆ§ R âŠ£âŠ¢ (P âˆ¨ Q) âˆ§ (P âˆ¨ R).
+Proof.
+  apply (anti_symm (âŠ¢)); first auto.
+  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
+Qed.
+Lemma or_and_r P Q R : P âˆ§ Q âˆ¨ R âŠ£âŠ¢ (P âˆ¨ R) âˆ§ (Q âˆ¨ R).
+Proof. by rewrite -!(comm _ R) or_and_l. Qed.
+Lemma and_or_l P Q R : P âˆ§ (Q âˆ¨ R) âŠ£âŠ¢ P âˆ§ Q âˆ¨ P âˆ§ R.
+Proof.
+  apply (anti_symm (âŠ¢)); last auto.
+  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
+Qed.
+Lemma and_or_r P Q R : (P âˆ¨ Q) âˆ§ R âŠ£âŠ¢ P âˆ§ R âˆ¨ Q âˆ§ R.
+Proof. by rewrite -!(comm _ R) and_or_l. Qed.
+Lemma and_exist_l {A} P (Î¨ : A â†’ uPred M) : P âˆ§ (âˆƒ a, Î¨ a) âŠ£âŠ¢ âˆƒ a, P âˆ§ Î¨ a.
+Proof.
+  apply (anti_symm (âŠ¢)).
+  - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
+    by rewrite -(exist_intro a).
+  - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
+    by rewrite -(exist_intro a) and_elim_r.
+Qed.
+Lemma and_exist_r {A} P (Î¦: A â†’ uPred M) : (âˆƒ a, Î¦ a) âˆ§ P âŠ£âŠ¢ âˆƒ a, Î¦ a âˆ§ P.
+Proof.
+  rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
+Qed.
+
+Lemma pure_mono Ï†1 Ï†2 : (Ï†1 â†’ Ï†2) â†’ â–  Ï†1 âŠ¢ â–  Ï†2.
+Proof. intros; apply pure_elim with Ï†1; eauto. Qed.
+Global Instance pure_mono' : Proper (impl ==> (âŠ¢)) (@uPred_pure M).
+Proof. intros Ï†1 Ï†2; apply pure_mono. Qed.
+Lemma pure_iff Ï†1 Ï†2 : (Ï†1 â†” Ï†2) â†’ â–  Ï†1 âŠ£âŠ¢ â–  Ï†2.
+Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
+Lemma pure_intro_l Ï† Q R : Ï† â†’ (â–  Ï† âˆ§ Q âŠ¢ R) â†’ Q âŠ¢ R.
+Proof. intros ? <-; auto using pure_intro. Qed.
+Lemma pure_intro_r Ï† Q R : Ï† â†’ (Q âˆ§ â–  Ï† âŠ¢ R) â†’ Q âŠ¢ R.
+Proof. intros ? <-; auto. Qed.
+Lemma pure_intro_impl Ï† Q R : Ï† â†’ (Q âŠ¢ â–  Ï† â†’ R) â†’ Q âŠ¢ R.
+Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
+Lemma pure_elim_l Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ â–  Ï† âˆ§ Q âŠ¢ R.
+Proof. intros; apply pure_elim with Ï†; eauto. Qed.
+Lemma pure_elim_r Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ Q âˆ§ â–  Ï† âŠ¢ R.
+Proof. intros; apply pure_elim with Ï†; eauto. Qed.
+Lemma pure_equiv (Ï† : Prop) : Ï† â†’ â–  Ï† âŠ£âŠ¢ True.
+Proof. intros; apply (anti_symm _); auto. Qed.
+
+Lemma pure_and Ï†1 Ï†2 : â–  (Ï†1 âˆ§ Ï†2) âŠ£âŠ¢ â–  Ï†1 âˆ§ â–  Ï†2.
+Proof.
+  apply (anti_symm _).
+  - eapply pure_elim=> // -[??]; auto.
+  - eapply (pure_elim Ï†1); [auto|]=> ?. eapply (pure_elim Ï†2); auto.
+Qed.
+Lemma pure_or Ï†1 Ï†2 : â–  (Ï†1 âˆ¨ Ï†2) âŠ£âŠ¢ â–  Ï†1 âˆ¨ â–  Ï†2.
+Proof.
+  apply (anti_symm _).
+  - eapply pure_elim=> // -[?|?]; auto.
+  - apply or_elim; eapply pure_elim; eauto.
+Qed.
+Lemma pure_impl Ï†1 Ï†2 : â–  (Ï†1 â†’ Ï†2) âŠ£âŠ¢ (â–  Ï†1 â†’ â–  Ï†2).
+Proof.
+  apply (anti_symm _).
+  - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
+  - rewrite -pure_forall_2. apply forall_intro=> ?.
+    by rewrite -(left_id True uPred_and (_â†’_))%I (pure_equiv Ï†1) // impl_elim_r.
+Qed.
+Lemma pure_forall {A} (Ï† : A â†’ Prop) : â–  (âˆ€ x, Ï† x) âŠ£âŠ¢ âˆ€ x, â–  Ï† x.
+Proof.
+  apply (anti_symm _); auto using pure_forall_2.
+  apply forall_intro=> x. eauto using pure_mono.
+Qed.
+Lemma pure_exist {A} (Ï† : A â†’ Prop) : â–  (âˆƒ x, Ï† x) âŠ£âŠ¢ âˆƒ x, â–  Ï† x.
+Proof.
+  apply (anti_symm _).
+  - eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto.
+  - apply exist_elim=> x. eauto using pure_mono.
+Qed.
+
+Lemma eq_refl' {A : cofeT} (a : A) P : P âŠ¢ a â‰¡ a.
+Proof. rewrite (True_intro P). apply eq_refl. Qed.
+Hint Resolve eq_refl'.
+Lemma equiv_eq {A : cofeT} P (a b : A) : a â‰¡ b â†’ P âŠ¢ a â‰¡ b.
+Proof. by intros ->. Qed.
+Lemma eq_sym {A : cofeT} (a b : A) : a â‰¡ b âŠ¢ b â‰¡ a.
+Proof. apply (eq_rewrite a b (Î» b, b â‰¡ a)%I); auto. solve_proper. Qed.
+
+Lemma pure_alt Ï† : â–  Ï† âŠ£âŠ¢ âˆƒ _ : Ï†, True.
+Proof.
+  apply (anti_symm _).
+  - eapply pure_elim; eauto=> H. rewrite -(exist_intro H); auto.
+  - by apply exist_elim, pure_intro.
+Qed.
+Lemma and_alt P Q : P âˆ§ Q âŠ£âŠ¢ âˆ€ b : bool, if b then P else Q.
+Proof.
+  apply (anti_symm _); first apply forall_intro=> -[]; auto.
+  apply and_intro. by rewrite (forall_elim true). by rewrite (forall_elim false).
+Qed.
+Lemma or_alt P Q : P âˆ¨ Q âŠ£âŠ¢ âˆƒ b : bool, if b then P else Q.
+Proof.
+  apply (anti_symm _); last apply exist_elim=> -[]; auto.
+  apply or_elim. by rewrite -(exist_intro true). by rewrite -(exist_intro false).
+Qed.
+
+Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
+Proof. unfold uPred_iff; solve_proper. Qed.
+Global Instance iff_proper :
+  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_iff M) := ne_proper_2 _.
+
+Lemma iff_refl Q P : Q âŠ¢ P â†” P.
+Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
+Lemma iff_equiv P Q : (True âŠ¢ P â†” Q) â†’ (P âŠ£âŠ¢ Q).
+Proof.
+  intros HPQ; apply (anti_symm (âŠ¢));
+    apply impl_entails; rewrite HPQ /uPred_iff; auto.
+Qed.
+Lemma equiv_iff P Q : (P âŠ£âŠ¢ Q) â†’ True âŠ¢ P â†” Q.
+Proof. intros ->; apply iff_refl. Qed.
+Lemma eq_iff P Q : P â‰¡ Q âŠ¢ P â†” Q.
+Proof.
+  apply (eq_rewrite P Q (Î» Q, P â†” Q))%I; first solve_proper; auto using iff_refl.
+Qed.
+
+(* Derived BI Stuff *)
+Hint Resolve sep_mono.
+Lemma sep_mono_l P P' Q : (P âŠ¢ Q) â†’ P â˜… P' âŠ¢ Q â˜… P'.
+Proof. by intros; apply sep_mono. Qed.
+Lemma sep_mono_r P P' Q' : (P' âŠ¢ Q') â†’ P â˜… P' âŠ¢ P â˜… Q'.
+Proof. by apply sep_mono. Qed.
+Global Instance sep_mono' : Proper ((âŠ¢) ==> (âŠ¢) ==> (âŠ¢)) (@uPred_sep M).
+Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
+Global Instance sep_flip_mono' :
+  Proper (flip (âŠ¢) ==> flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_sep M).
+Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
+Lemma wand_mono P P' Q Q' : (Q âŠ¢ P) â†’ (P' âŠ¢ Q') â†’ (P -â˜… P') âŠ¢ Q -â˜… Q'.
+Proof.
+  intros HP HQ; apply wand_intro_r. rewrite HP -HQ. by apply wand_elim_l'.
+Qed.
+Global Instance wand_mono' : Proper (flip (âŠ¢) ==> (âŠ¢) ==> (âŠ¢)) (@uPred_wand M).
+Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
+
+Global Instance sep_comm : Comm (âŠ£âŠ¢) (@uPred_sep M).
+Proof. intros P Q; apply (anti_symm _); auto using sep_comm'. Qed.
+Global Instance sep_assoc : Assoc (âŠ£âŠ¢) (@uPred_sep M).
+Proof.
+  intros P Q R; apply (anti_symm _); auto using sep_assoc'.
+  by rewrite !(comm _ P) !(comm _ _ R) sep_assoc'.
+Qed.
+Global Instance True_sep : LeftId (âŠ£âŠ¢) True%I (@uPred_sep M).
+Proof. intros P; apply (anti_symm _); auto using True_sep_1, True_sep_2. Qed.
+Global Instance sep_True : RightId (âŠ£âŠ¢) True%I (@uPred_sep M).
+Proof. by intros P; rewrite comm left_id. Qed.
+Lemma sep_elim_l P Q : P â˜… Q âŠ¢ P.
+Proof. by rewrite (True_intro Q) right_id. Qed.
+Lemma sep_elim_r P Q : P â˜… Q âŠ¢ Q.
+Proof. by rewrite (comm (â˜…))%I; apply sep_elim_l. Qed.
+Lemma sep_elim_l' P Q R : (P âŠ¢ R) â†’ P â˜… Q âŠ¢ R.
+Proof. intros ->; apply sep_elim_l. Qed.
+Lemma sep_elim_r' P Q R : (Q âŠ¢ R) â†’ P â˜… Q âŠ¢ R.
+Proof. intros ->; apply sep_elim_r. Qed.
+Hint Resolve sep_elim_l' sep_elim_r'.
+Lemma sep_intro_True_l P Q R : (True âŠ¢ P) â†’ (R âŠ¢ Q) â†’ R âŠ¢ P â˜… Q.
+Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
+Lemma sep_intro_True_r P Q R : (R âŠ¢ P) â†’ (True âŠ¢ Q) â†’ R âŠ¢ P â˜… Q.
+Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
+Lemma sep_elim_True_l P Q R : (True âŠ¢ P) â†’ (P â˜… R âŠ¢ Q) â†’ R âŠ¢ Q.
+Proof. by intros HP; rewrite -HP left_id. Qed.
+Lemma sep_elim_True_r P Q R : (True âŠ¢ P) â†’ (R â˜… P âŠ¢ Q) â†’ R âŠ¢ Q.
+Proof. by intros HP; rewrite -HP right_id. Qed.
+Lemma wand_intro_l P Q R : (Q â˜… P âŠ¢ R) â†’ P âŠ¢ Q -â˜… R.
+Proof. rewrite comm; apply wand_intro_r. Qed.
+Lemma wand_elim_l P Q : (P -â˜… Q) â˜… P âŠ¢ Q.
+Proof. by apply wand_elim_l'. Qed.
+Lemma wand_elim_r P Q : P â˜… (P -â˜… Q) âŠ¢ Q.
+Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
+Lemma wand_elim_r' P Q R : (Q âŠ¢ P -â˜… R) â†’ P â˜… Q âŠ¢ R.
+Proof. intros ->; apply wand_elim_r. Qed.
+Lemma wand_apply_l P Q Q' R R' : (P âŠ¢ Q' -â˜… R') â†’ (R' âŠ¢ R) â†’ (Q âŠ¢ Q') â†’ P â˜… Q âŠ¢ R.
+Proof. intros -> -> <-; apply wand_elim_l. Qed.
+Lemma wand_apply_r P Q Q' R R' : (P âŠ¢ Q' -â˜… R') â†’ (R' âŠ¢ R) â†’ (Q âŠ¢ Q') â†’ Q â˜… P âŠ¢ R.
+Proof. intros -> -> <-; apply wand_elim_r. Qed.
+Lemma wand_apply_l' P Q Q' R : (P âŠ¢ Q' -â˜… R) â†’ (Q âŠ¢ Q') â†’ P â˜… Q âŠ¢ R.
+Proof. intros -> <-; apply wand_elim_l. Qed.
+Lemma wand_apply_r' P Q Q' R : (P âŠ¢ Q' -â˜… R) â†’ (Q âŠ¢ Q') â†’ Q â˜… P âŠ¢ R.
+Proof. intros -> <-; apply wand_elim_r. Qed.
+Lemma wand_frame_l P Q R : (Q -â˜… R) âŠ¢ P â˜… Q -â˜… P â˜… R.
+Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
+Lemma wand_frame_r P Q R : (Q -â˜… R) âŠ¢ Q â˜… P -â˜… R â˜… P.
+Proof.
+  apply wand_intro_l. rewrite ![(_ â˜… P)%I]comm -assoc.
+  apply sep_mono_r, wand_elim_r.
+Qed.
+Lemma wand_diag P : (P -â˜… P) âŠ£âŠ¢ True.
+Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
+Lemma wand_True P : (True -â˜… P) âŠ£âŠ¢ P.
+Proof.
+  apply (anti_symm _); last by auto using wand_intro_l.
+  eapply sep_elim_True_l; first reflexivity. by rewrite wand_elim_r.
+Qed.
+Lemma wand_entails P Q : (True âŠ¢ P -â˜… Q) â†’ P âŠ¢ Q.
+Proof.
+  intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
+Qed.
+Lemma entails_wand P Q : (P âŠ¢ Q) â†’ True âŠ¢ P -â˜… Q.
+Proof. auto using wand_intro_l. Qed.
+Lemma wand_curry P Q R : (P -â˜… Q -â˜… R) âŠ£âŠ¢ (P â˜… Q -â˜… R).
+Proof.
+  apply (anti_symm _).
+  - apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r.
+  - do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) wand_elim_r.
+Qed.
+
+Lemma sep_and P Q : (P â˜… Q) âŠ¢ (P âˆ§ Q).
+Proof. auto. Qed.
+Lemma impl_wand P Q : (P â†’ Q) âŠ¢ P -â˜… Q.
+Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
+Lemma pure_elim_sep_l Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ â–  Ï† â˜… Q âŠ¢ R.
+Proof. intros; apply pure_elim with Ï†; eauto. Qed.
+Lemma pure_elim_sep_r Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ Q â˜… â–  Ï† âŠ¢ R.
+Proof. intros; apply pure_elim with Ï†; eauto. Qed.
+
+Global Instance sep_False : LeftAbsorb (âŠ£âŠ¢) False%I (@uPred_sep M).
+Proof. intros P; apply (anti_symm _); auto. Qed.
+Global Instance False_sep : RightAbsorb (âŠ£âŠ¢) False%I (@uPred_sep M).
+Proof. intros P; apply (anti_symm _); auto. Qed.
+
+Lemma sep_and_l P Q R : P â˜… (Q âˆ§ R) âŠ¢ (P â˜… Q) âˆ§ (P â˜… R).
+Proof. auto. Qed.
+Lemma sep_and_r P Q R : (P âˆ§ Q) â˜… R âŠ¢ (P â˜… R) âˆ§ (Q â˜… R).
+Proof. auto. Qed.
+Lemma sep_or_l P Q R : P â˜… (Q âˆ¨ R) âŠ£âŠ¢ (P â˜… Q) âˆ¨ (P â˜… R).
+Proof.
+  apply (anti_symm (âŠ¢)); last by eauto 8.
+  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
+Qed.
+Lemma sep_or_r P Q R : (P âˆ¨ Q) â˜… R âŠ£âŠ¢ (P â˜… R) âˆ¨ (Q â˜… R).
+Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
+Lemma sep_exist_l {A} P (Î¨ : A â†’ uPred M) : P â˜… (âˆƒ a, Î¨ a) âŠ£âŠ¢ âˆƒ a, P â˜… Î¨ a.
+Proof.
+  intros; apply (anti_symm (âŠ¢)).
+  - apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
+    by rewrite -(exist_intro a).
+  - apply exist_elim=> a; apply sep_mono; auto using exist_intro.
+Qed.
+Lemma sep_exist_r {A} (Î¦: A â†’ uPred M) Q: (âˆƒ a, Î¦ a) â˜… Q âŠ£âŠ¢ âˆƒ a, Î¦ a â˜… Q.
+Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
+Lemma sep_forall_l {A} P (Î¨ : A â†’ uPred M) : P â˜… (âˆ€ a, Î¨ a) âŠ¢ âˆ€ a, P â˜… Î¨ a.
+Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
+Lemma sep_forall_r {A} (Î¦ : A â†’ uPred M) Q : (âˆ€ a, Î¦ a) â˜… Q âŠ¢ âˆ€ a, Î¦ a â˜… Q.
+Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
+
+(* Always derived *)
+Hint Resolve always_mono always_elim.
+Global Instance always_mono' : Proper ((âŠ¢) ==> (âŠ¢)) (@uPred_always M).
+Proof. intros P Q; apply always_mono. Qed.
+Global Instance always_flip_mono' :
+  Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_always M).
+Proof. intros P Q; apply always_mono. Qed.
+
+Lemma always_intro' P Q : (â–¡ P âŠ¢ Q) â†’ â–¡ P âŠ¢ â–¡ Q.
+Proof. intros <-. apply always_idemp. Qed.
+
+Lemma always_pure Ï† : â–¡ â–  Ï† âŠ£âŠ¢ â–  Ï†.
+Proof. apply (anti_symm _); auto using always_pure_2. Qed.
+Lemma always_forall {A} (Î¨ : A â†’ uPred M) : (â–¡ âˆ€ a, Î¨ a) âŠ£âŠ¢ (âˆ€ a, â–¡ Î¨ a).
+Proof.
+  apply (anti_symm _); auto using always_forall_2.
+  apply forall_intro=> x. by rewrite (forall_elim x).
+Qed.
+Lemma always_exist {A} (Î¨ : A â†’ uPred M) : (â–¡ âˆƒ a, Î¨ a) âŠ£âŠ¢ (âˆƒ a, â–¡ Î¨ a).
+Proof.
+  apply (anti_symm _); auto using always_exist_1.
+  apply exist_elim=> x. by rewrite (exist_intro x).
+Qed.
+Lemma always_and P Q : â–¡ (P âˆ§ Q) âŠ£âŠ¢ â–¡ P âˆ§ â–¡ Q.
+Proof. rewrite !and_alt always_forall. by apply forall_proper=> -[]. Qed.
+Lemma always_or P Q : â–¡ (P âˆ¨ Q) âŠ£âŠ¢ â–¡ P âˆ¨ â–¡ Q.
+Proof. rewrite !or_alt always_exist. by apply exist_proper=> -[]. Qed.
+Lemma always_impl P Q : â–¡ (P â†’ Q) âŠ¢ â–¡ P â†’ â–¡ Q.
+Proof.
+  apply impl_intro_l; rewrite -always_and.
+  apply always_mono, impl_elim with P; auto.
+Qed.
+Lemma always_eq {A:cofeT} (a b : A) : â–¡ (a â‰¡ b) âŠ£âŠ¢ a â‰¡ b.
+Proof.
+  apply (anti_symm (âŠ¢)); auto using always_elim.
+  apply (eq_rewrite a b (Î» b, â–¡ (a â‰¡ b))%I); auto.
+  { intros n; solve_proper. }
+  rewrite -(eq_refl a) always_pure; auto.
+Qed.
+
+Lemma always_and_sep P Q : â–¡ (P âˆ§ Q) âŠ£âŠ¢ â–¡ (P â˜… Q).
+Proof. apply (anti_symm (âŠ¢)); auto using always_and_sep_1. Qed.
+Lemma always_and_sep_l' P Q : â–¡ P âˆ§ Q âŠ£âŠ¢ â–¡ P â˜… Q.
+Proof. apply (anti_symm (âŠ¢)); auto using always_and_sep_l_1. Qed.
+Lemma always_and_sep_r' P Q : P âˆ§ â–¡ Q âŠ£âŠ¢ P â˜… â–¡ Q.
+Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
+Lemma always_sep P Q : â–¡ (P â˜… Q) âŠ£âŠ¢ â–¡ P â˜… â–¡ Q.
+Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
+Lemma always_sep_dup' P : â–¡ P âŠ£âŠ¢ â–¡ P â˜… â–¡ P.
+Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.
+
+Lemma always_wand P Q : â–¡ (P -â˜… Q) âŠ¢ â–¡ P -â˜… â–¡ Q.
+Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
+Lemma always_wand_impl P Q : â–¡ (P -â˜… Q) âŠ£âŠ¢ â–¡ (P â†’ Q).
+Proof.
+  apply (anti_symm (âŠ¢)); [|by rewrite -impl_wand].
+  apply always_intro', impl_intro_r.
+  by rewrite always_and_sep_l' always_elim wand_elim_l.
+Qed.
+Lemma always_entails_l' P Q : (P âŠ¢ â–¡ Q) â†’ P âŠ¢ â–¡ Q â˜… P.
+Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
+Lemma always_entails_r' P Q : (P âŠ¢ â–¡ Q) â†’ P âŠ¢ P â˜… â–¡ Q.
+Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
+
+(* Later derived *)
+Lemma later_proper P Q : (P âŠ£âŠ¢ Q) â†’ â–· P âŠ£âŠ¢ â–· Q.
+Proof. by intros ->. Qed.
+Hint Resolve later_mono later_proper.
+Global Instance later_mono' : Proper ((âŠ¢) ==> (âŠ¢)) (@uPred_later M).
+Proof. intros P Q; apply later_mono. Qed.
+Global Instance later_flip_mono' :
+  Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_later M).
+Proof. intros P Q; apply later_mono. Qed.
+
+Lemma later_intro P : P âŠ¢ â–· P.
+Proof.
+  rewrite -(and_elim_l (â–· P) P) -(lÃ¶b (â–· P âˆ§ P)).
+  apply impl_intro_l. by rewrite {1}(and_elim_r (â–· P)).
+Qed.
+
+Lemma later_True : â–· True âŠ£âŠ¢ True.
+Proof. apply (anti_symm (âŠ¢)); auto using later_intro. Qed.
+Lemma later_forall {A} (Î¦ : A â†’ uPred M) : (â–· âˆ€ a, Î¦ a) âŠ£âŠ¢ (âˆ€ a, â–· Î¦ a).
+Proof.
+  apply (anti_symm _); auto using later_forall_2.
+  apply forall_intro=> x. by rewrite (forall_elim x).
+Qed.
+Lemma later_exist `{Inhabited A} (Î¦ : A â†’ uPred M) :
+  â–· (âˆƒ a, Î¦ a) âŠ£âŠ¢ (âˆƒ a, â–· Î¦ a).
+Proof.
+  apply: anti_symm; [|apply exist_elim; eauto using exist_intro].
+  rewrite later_exist_false. apply or_elim; last done.
+  rewrite -(exist_intro inhabitant); auto.
+Qed.
+Lemma later_and P Q : â–· (P âˆ§ Q) âŠ£âŠ¢ â–· P âˆ§ â–· Q.
+Proof. rewrite !and_alt later_forall. by apply forall_proper=> -[]. Qed.
+Lemma later_or P Q : â–· (P âˆ¨ Q) âŠ£âŠ¢ â–· P âˆ¨ â–· Q.
+Proof. rewrite !or_alt later_exist. by apply exist_proper=> -[]. Qed.
+Lemma later_impl P Q : â–· (P â†’ Q) âŠ¢ â–· P â†’ â–· Q.
+Proof. apply impl_intro_l; rewrite -later_and; eauto using impl_elim. Qed.
+Lemma later_wand P Q : â–· (P -â˜… Q) âŠ¢ â–· P -â˜… â–· Q.
+Proof. apply wand_intro_r; rewrite -later_sep; eauto using wand_elim_l. Qed.
+Lemma later_iff P Q : â–· (P â†” Q) âŠ¢ â–· P â†” â–· Q.
+Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
+
+
+(* Conditional always *)
+Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
+Proof. solve_proper. Qed.
+Global Instance always_if_proper p : Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_always_if M p).
+Proof. solve_proper. Qed.
+Global Instance always_if_mono p : Proper ((âŠ¢) ==> (âŠ¢)) (@uPred_always_if M p).
+Proof. solve_proper. Qed.
+
+Lemma always_if_elim p P : â–¡?p P âŠ¢ P.
+Proof. destruct p; simpl; auto using always_elim. Qed.
+Lemma always_elim_if p P : â–¡ P âŠ¢ â–¡?p P.
+Proof. destruct p; simpl; auto using always_elim. Qed.
+
+Lemma always_if_pure p Ï† : â–¡?p â–  Ï† âŠ£âŠ¢ â–  Ï†.
+Proof. destruct p; simpl; auto using always_pure. Qed.
+Lemma always_if_and p P Q : â–¡?p (P âˆ§ Q) âŠ£âŠ¢ â–¡?p P âˆ§ â–¡?p Q.
+Proof. destruct p; simpl; auto using always_and. Qed.
+Lemma always_if_or p P Q : â–¡?p (P âˆ¨ Q) âŠ£âŠ¢ â–¡?p P âˆ¨ â–¡?p Q.
+Proof. destruct p; simpl; auto using always_or. Qed.
+Lemma always_if_exist {A} p (Î¨ : A â†’ uPred M) : (â–¡?p âˆƒ a, Î¨ a) âŠ£âŠ¢ âˆƒ a, â–¡?p Î¨ a.
+Proof. destruct p; simpl; auto using always_exist. Qed.
+Lemma always_if_sep p P Q : â–¡?p (P â˜… Q) âŠ£âŠ¢ â–¡?p P â˜… â–¡?p Q.
+Proof. destruct p; simpl; auto using always_sep. Qed.
+Lemma always_if_later p P : â–¡?p â–· P âŠ£âŠ¢ â–· â–¡?p P.
+Proof. destruct p; simpl; auto using always_later. Qed.
+
+
+(* True now *)
+Global Instance except_last_ne n : Proper (dist n ==> dist n) (@uPred_except_last M).
+Proof. solve_proper. Qed.
+Global Instance except_last_proper : Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_except_last M).
+Proof. solve_proper. Qed.
+Global Instance except_last_mono' : Proper ((âŠ¢) ==> (âŠ¢)) (@uPred_except_last M).
+Proof. solve_proper. Qed.
+Global Instance except_last_flip_mono' :
+  Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_except_last M).
+Proof. solve_proper. Qed.
+
+Lemma except_last_intro P : P âŠ¢ â—‡ P.
+Proof. rewrite /uPred_except_last; auto. Qed.
+Lemma except_last_mono P Q : (P âŠ¢ Q) â†’ â—‡ P âŠ¢ â—‡ Q.
+Proof. by intros ->. Qed.
+Lemma except_last_idemp P : â—‡ â—‡ P âŠ¢ â—‡ P.
+Proof. rewrite /uPred_except_last; auto. Qed.
+
+Lemma except_last_True : â—‡ True âŠ£âŠ¢ True.
+Proof. rewrite /uPred_except_last. apply (anti_symm _); auto. Qed.
+Lemma except_last_or P Q : â—‡ (P âˆ¨ Q) âŠ£âŠ¢ â—‡ P âˆ¨ â—‡ Q.
+Proof. rewrite /uPred_except_last. apply (anti_symm _); auto. Qed.
+Lemma except_last_and P Q : â—‡ (P âˆ§ Q) âŠ£âŠ¢ â—‡ P âˆ§ â—‡ Q.
+Proof. by rewrite /uPred_except_last or_and_l. Qed.
+Lemma except_last_sep P Q : â—‡ (P â˜… Q) âŠ£âŠ¢ â—‡ P â˜… â—‡ Q.
+Proof.
+  rewrite /uPred_except_last. apply (anti_symm _).
+  - apply or_elim; last by auto.
+    by rewrite -!or_intro_l -always_pure -always_later -always_sep_dup'.
+  - rewrite sep_or_r sep_elim_l sep_or_l; auto.
+Qed.
+Lemma except_last_forall {A} (Î¦ : A â†’ uPred M) : â—‡ (âˆ€ a, Î¦ a) âŠ¢ âˆ€ a, â—‡ Î¦ a.
+Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
+Lemma except_last_exist {A} (Î¦ : A â†’ uPred M) : (âˆƒ a, â—‡ Î¦ a) âŠ¢ â—‡ âˆƒ a, Î¦ a.
+Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
+Lemma except_last_later P : â—‡ â–· P âŠ¢ â–· P.
+Proof. by rewrite /uPred_except_last -later_or False_or. Qed.
+Lemma except_last_always P : â—‡ â–¡ P âŠ£âŠ¢ â–¡ â—‡ P.
+Proof. by rewrite /uPred_except_last always_or always_later always_pure. Qed.
+Lemma except_last_always_if p P : â—‡ â–¡?p P âŠ£âŠ¢ â–¡?p â—‡ P.
+Proof. destruct p; simpl; auto using except_last_always. Qed.
+Lemma except_last_frame_l P Q : P â˜… â—‡ Q âŠ¢ â—‡ (P â˜… Q).
+Proof. by rewrite {1}(except_last_intro P) except_last_sep. Qed.
+Lemma except_last_frame_r P Q : â—‡ P â˜… Q âŠ¢ â—‡ (P â˜… Q).
+Proof. by rewrite {1}(except_last_intro Q) except_last_sep. Qed.
+
+(* Own and valid derived *)
+Lemma always_ownM (a : M) : Persistent a â†’ â–¡ uPred_ownM a âŠ£âŠ¢ uPred_ownM a.
+Proof.
+  intros; apply (anti_symm _); first by apply:always_elim.
+  by rewrite {1}always_ownM_core persistent_core.
+Qed.
+Lemma ownM_invalid (a : M) : Â¬ âœ“{0} a â†’ uPred_ownM a âŠ¢ False.
+Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
+Global Instance ownM_mono : Proper (flip (â‰¼) ==> (âŠ¢)) (@uPred_ownM M).
+Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
+Lemma ownM_empty' : uPred_ownM âˆ… âŠ£âŠ¢ True.
+Proof. apply (anti_symm _); auto using ownM_empty. Qed.
+Lemma always_cmra_valid {A : cmraT} (a : A) : â–¡ âœ“ a âŠ£âŠ¢ âœ“ a.
+Proof.
+  intros; apply (anti_symm _); first by apply:always_elim.
+  apply:always_cmra_valid_1.
+Qed.
+
+(** * Derived rules *)
+Global Instance bupd_mono' : Proper ((âŠ¢) ==> (âŠ¢)) (@uPred_bupd M).
+Proof. intros P Q; apply bupd_mono. Qed.
+Global Instance bupd_flip_mono' : Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_bupd M).
+Proof. intros P Q; apply bupd_mono. Qed.
+Lemma bupd_frame_l R Q : (R â˜… |==> Q) ==â˜… R â˜… Q.
+Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
+Lemma bupd_wand_l P Q : (P -â˜… Q) â˜… (|==> P) ==â˜… Q.
+Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
+Lemma bupd_wand_r P Q : (|==> P) â˜… (P -â˜… Q) ==â˜… Q.
+Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
+Lemma bupd_sep P Q : (|==> P) â˜… (|==> Q) ==â˜… P â˜… Q.
+Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
+Lemma bupd_ownM_update x y : x ~~> y â†’ uPred_ownM x âŠ¢ |==> uPred_ownM y.
+Proof.
+  intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
+  by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
+Qed.
+Lemma except_last_bupd P : â—‡ (|==> P) âŠ¢ (|==> â—‡ P).
+Proof.
+  rewrite /uPred_except_last. apply or_elim; auto using bupd_mono.
+  by rewrite -bupd_intro -or_intro_l.
+Qed.
+
+(* Timeless instances *)
+Global Instance pure_timeless Ï† : TimelessP (â–  Ï† : uPred M)%I.
+Proof.
+  rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True.
+Qed.
+Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
+  TimelessP (âœ“ a : uPred M)%I.
+Proof. rewrite /TimelessP !discrete_valid. apply (timelessP _). Qed.
+Global Instance and_timeless P Q: TimelessP P â†’ TimelessP Q â†’ TimelessP (P âˆ§ Q).
+Proof. intros; rewrite /TimelessP except_last_and later_and; auto. Qed.
+Global Instance or_timeless P Q : TimelessP P â†’ TimelessP Q â†’ TimelessP (P âˆ¨ Q).
+Proof. intros; rewrite /TimelessP except_last_or later_or; auto. Qed.
+Global Instance impl_timeless P Q : TimelessP Q â†’ TimelessP (P â†’ Q).
+Proof.
+  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
+  apply or_mono, impl_intro_l; first done.
+  rewrite -{2}(lÃ¶b Q); apply impl_intro_l.
+  rewrite HQ /uPred_except_last !and_or_r. apply or_elim; last auto.
+  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
+Qed.
+Global Instance sep_timeless P Q: TimelessP P â†’ TimelessP Q â†’ TimelessP (P â˜… Q).
+Proof. intros; rewrite /TimelessP except_last_sep later_sep; auto. Qed.
+Global Instance wand_timeless P Q : TimelessP Q â†’ TimelessP (P -â˜… Q).
+Proof.
+  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
+  apply or_mono, wand_intro_l; first done.
+  rewrite -{2}(lÃ¶b Q); apply impl_intro_l.
+  rewrite HQ /uPred_except_last !and_or_r. apply or_elim; last auto.
+  rewrite -(always_pure) -always_later always_and_sep_l'.
+  by rewrite assoc (comm _ _ P) -assoc -always_and_sep_l' impl_elim_r wand_elim_r.
+Qed.
+Global Instance forall_timeless {A} (Î¨ : A â†’ uPred M) :
+  (âˆ€ x, TimelessP (Î¨ x)) â†’ TimelessP (âˆ€ x, Î¨ x).
+Proof.
+  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
+  apply or_mono; first done. apply forall_intro=> x.
+  rewrite -(lÃ¶b (Î¨ x)); apply impl_intro_l.
+  rewrite HQ /uPred_except_last !and_or_r. apply or_elim; last auto.
+  by rewrite impl_elim_r (forall_elim x).
+Qed.
+Global Instance exist_timeless {A} (Î¨ : A â†’ uPred M) :
+  (âˆ€ x, TimelessP (Î¨ x)) â†’ TimelessP (âˆƒ x, Î¨ x).
+Proof.
+  rewrite /TimelessP=> ?. rewrite later_exist_false. apply or_elim.
+  - rewrite /uPred_except_last; auto.
+  - apply exist_elim=> x. rewrite -(exist_intro x); auto.
+Qed.
+Global Instance always_timeless P : TimelessP P â†’ TimelessP (â–¡ P).
+Proof. intros; rewrite /TimelessP except_last_always -always_later; auto. Qed.
+Global Instance always_if_timeless p P : TimelessP P â†’ TimelessP (â–¡?p P).
+Proof. destruct p; apply _. Qed.
+Global Instance eq_timeless {A : cofeT} (a b : A) :
+  Timeless a â†’ TimelessP (a â‰¡ b : uPred M)%I.
+Proof. intros. rewrite /TimelessP !timeless_eq. apply (timelessP _). Qed.
+Global Instance ownM_timeless (a : M) : Timeless a â†’ TimelessP (uPred_ownM a).
+Proof.
+  intros ?. rewrite /TimelessP later_ownM. apply exist_elim=> b.
+  rewrite (timelessP (aâ‰¡b)) (except_last_intro (uPred_ownM b)) -except_last_and.
+  apply except_last_mono. rewrite eq_sym.
+  apply (eq_rewrite b a (uPred_ownM)); first apply _; auto.
+Qed.
+
+(* Persistence *)
+Global Instance pure_persistent Ï† : PersistentP (â–  Ï† : uPred M)%I.
+Proof. by rewrite /PersistentP always_pure. Qed.
+Global Instance always_persistent P : PersistentP (â–¡ P).
+Proof. by intros; apply always_intro'. Qed.
+Global Instance and_persistent P Q :
+  PersistentP P â†’ PersistentP Q â†’ PersistentP (P âˆ§ Q).
+Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed.
+Global Instance or_persistent P Q :
+  PersistentP P â†’ PersistentP Q â†’ PersistentP (P âˆ¨ Q).
+Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
+Global Instance sep_persistent P Q :
+  PersistentP P â†’ PersistentP Q â†’ PersistentP (P â˜… Q).
+Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
+Global Instance forall_persistent {A} (Î¨ : A â†’ uPred M) :
+  (âˆ€ x, PersistentP (Î¨ x)) â†’ PersistentP (âˆ€ x, Î¨ x).
+Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
+Global Instance exist_persistent {A} (Î¨ : A â†’ uPred M) :
+  (âˆ€ x, PersistentP (Î¨ x)) â†’ PersistentP (âˆƒ x, Î¨ x).
+Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
+Global Instance eq_persistent {A : cofeT} (a b : A) :
+  PersistentP (a â‰¡ b : uPred M)%I.
+Proof. by intros; rewrite /PersistentP always_eq. Qed.
+Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
+  PersistentP (âœ“ a : uPred M)%I.
+Proof. by intros; rewrite /PersistentP always_cmra_valid. Qed.
+Global Instance later_persistent P : PersistentP P â†’ PersistentP (â–· P).
+Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
+Global Instance ownM_persistent : Persistent a â†’ PersistentP (@uPred_ownM M a).
+Proof. intros. by rewrite /PersistentP always_ownM. Qed.
+Global Instance from_option_persistent {A} P (Î¨ : A â†’ uPred M) (mx : option A) :
+  (âˆ€ x, PersistentP (Î¨ x)) â†’ PersistentP P â†’ PersistentP (from_option Î¨ P mx).
+Proof. destruct mx; apply _. Qed.
+
+(* Derived lemmas for persistence *)
+Lemma always_always P `{!PersistentP P} : â–¡ P âŠ£âŠ¢ P.
+Proof. apply (anti_symm (âŠ¢)); auto using always_elim. Qed.
+Lemma always_if_always p P `{!PersistentP P} : â–¡?p P âŠ£âŠ¢ P.
+Proof. destruct p; simpl; auto using always_always. Qed.
+Lemma always_intro P Q `{!PersistentP P} : (P âŠ¢ Q) â†’ P âŠ¢ â–¡ Q.
+Proof. rewrite -(always_always P); apply always_intro'. Qed.
+Lemma always_and_sep_l P Q `{!PersistentP P} : P âˆ§ Q âŠ£âŠ¢ P â˜… Q.
+Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
+Lemma always_and_sep_r P Q `{!PersistentP Q} : P âˆ§ Q âŠ£âŠ¢ P â˜… Q.
+Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
+Lemma always_sep_dup P `{!PersistentP P} : P âŠ£âŠ¢ P â˜… P.
+Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
+Lemma always_entails_l P Q `{!PersistentP Q} : (P âŠ¢ Q) â†’ P âŠ¢ Q â˜… P.
+Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
+Lemma always_entails_r P Q `{!PersistentP Q} : (P âŠ¢ Q) â†’ P âŠ¢ P â˜… Q.
+Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
+End derived.
+End uPred_derived.
diff --git a/algebra/double_negation.v b/base_logic/double_negation.v
similarity index 99%
rename from algebra/double_negation.v
rename to base_logic/double_negation.v
index 875045d22..123d5b831 100644
--- a/algebra/double_negation.v
+++ b/base_logic/double_negation.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import upred.
+From iris.base_logic Require Import base_logic.
 Import upred.
 
 (* In this file we show that the bupd can be thought of a kind of
diff --git a/algebra/upred_hlist.v b/base_logic/hlist.v
similarity index 96%
rename from algebra/upred_hlist.v
rename to base_logic/hlist.v
index 82d0e55aa..e70bd6eac 100644
--- a/algebra/upred_hlist.v
+++ b/base_logic/hlist.v
@@ -1,5 +1,5 @@
 From iris.prelude Require Export hlist.
-From iris.algebra Require Export upred.
+From iris.base_logic Require Export base_logic.
 Import uPred.
 
 Fixpoint uPred_hexist {M As} : himpl As (uPred M) â†’ uPred M :=
diff --git a/base_logic/primitive.v b/base_logic/primitive.v
new file mode 100644
index 000000000..5c8f15f1a
--- /dev/null
+++ b/base_logic/primitive.v
@@ -0,0 +1,592 @@
+From iris.base_logic Require Export upred.
+From iris.algebra Require Export updates.
+Local Hint Extern 1 (_ â‰¼ _) => etrans; [eassumption|].
+Local Hint Extern 1 (_ â‰¼ _) => etrans; [|eassumption].
+Local Hint Extern 10 (_ â‰¤ _) => omega.
+
+(** logical connectives *)
+Program Definition uPred_pure_def {M} (Ï† : Prop) : uPred M :=
+  {| uPred_holds n x := Ï† |}.
+Solve Obligations with done.
+Definition uPred_pure_aux : { x | x = @uPred_pure_def }. by eexists. Qed.
+Definition uPred_pure {M} := proj1_sig uPred_pure_aux M.
+Definition uPred_pure_eq :
+  @uPred_pure = @uPred_pure_def := proj2_sig uPred_pure_aux.
+
+Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_pure True).
+
+Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
+  {| uPred_holds n x := P n x âˆ§ Q n x |}.
+Solve Obligations with naive_solver eauto 2 with uPred_def.
+Definition uPred_and_aux : { x | x = @uPred_and_def }. by eexists. Qed.
+Definition uPred_and {M} := proj1_sig uPred_and_aux M.
+Definition uPred_and_eq: @uPred_and = @uPred_and_def := proj2_sig uPred_and_aux.
+
+Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
+  {| uPred_holds n x := P n x âˆ¨ Q n x |}.
+Solve Obligations with naive_solver eauto 2 with uPred_def.
+Definition uPred_or_aux : { x | x = @uPred_or_def }. by eexists. Qed.
+Definition uPred_or {M} := proj1_sig uPred_or_aux M.
+Definition uPred_or_eq: @uPred_or = @uPred_or_def := proj2_sig uPred_or_aux.
+
+Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
+  {| uPred_holds n x := âˆ€ n' x',
+       x â‰¼ x' â†’ n' â‰¤ n â†’ âœ“{n'} x' â†’ P n' x' â†’ Q n' x' |}.
+Next Obligation.
+  intros M P Q n1 x1 x1' HPQ [x2 Hx1'] n2 x3 [x4 Hx3] ?; simpl in *.
+  rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
+  eapply HPQ; auto. exists (x2 â‹… x4); by rewrite assoc.
+Qed.
+Next Obligation. intros M P Q [|n1] [|n2] x; auto with lia. Qed.
+Definition uPred_impl_aux : { x | x = @uPred_impl_def }. by eexists. Qed.
+Definition uPred_impl {M} := proj1_sig uPred_impl_aux M.
+Definition uPred_impl_eq :
+  @uPred_impl = @uPred_impl_def := proj2_sig uPred_impl_aux.
+
+Program Definition uPred_forall_def {M A} (Î¨ : A â†’ uPred M) : uPred M :=
+  {| uPred_holds n x := âˆ€ a, Î¨ a n x |}.
+Solve Obligations with naive_solver eauto 2 with uPred_def.
+Definition uPred_forall_aux : { x | x = @uPred_forall_def }. by eexists. Qed.
+Definition uPred_forall {M A} := proj1_sig uPred_forall_aux M A.
+Definition uPred_forall_eq :
+  @uPred_forall = @uPred_forall_def := proj2_sig uPred_forall_aux.
+
+Program Definition uPred_exist_def {M A} (Î¨ : A â†’ uPred M) : uPred M :=
+  {| uPred_holds n x := âˆƒ a, Î¨ a n x |}.
+Solve Obligations with naive_solver eauto 2 with uPred_def.
+Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed.
+Definition uPred_exist {M A} := proj1_sig uPred_exist_aux M A.
+Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := proj2_sig uPred_exist_aux.
+
+Program Definition uPred_eq_def {M} {A : cofeT} (a1 a2 : A) : uPred M :=
+  {| uPred_holds n x := a1 â‰¡{n}â‰¡ a2 |}.
+Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
+Definition uPred_eq_aux : { x | x = @uPred_eq_def }. by eexists. Qed.
+Definition uPred_eq {M A} := proj1_sig uPred_eq_aux M A.
+Definition uPred_eq_eq: @uPred_eq = @uPred_eq_def := proj2_sig uPred_eq_aux.
+
+Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
+  {| uPred_holds n x := âˆƒ x1 x2, x â‰¡{n}â‰¡ x1 â‹… x2 âˆ§ P n x1 âˆ§ Q n x2 |}.
+Next Obligation.
+  intros M P Q n x y (x1&x2&Hx&?&?) [z Hy].
+  exists x1, (x2 â‹… z); split_and?; eauto using uPred_mono, cmra_includedN_l.
+  by rewrite Hy Hx assoc.
+Qed.
+Next Obligation.
+  intros M P Q n1 n2 x (x1&x2&Hx&?&?) ?; rewrite {1}(dist_le _ _ _ _ Hx) // =>?.
+  exists x1, x2; cofe_subst; split_and!;
+    eauto using dist_le, uPred_closed, cmra_validN_op_l, cmra_validN_op_r.
+Qed.
+Definition uPred_sep_aux : { x | x = @uPred_sep_def }. by eexists. Qed.
+Definition uPred_sep {M} := proj1_sig uPred_sep_aux M.
+Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := proj2_sig uPred_sep_aux.
+
+Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
+  {| uPred_holds n x := âˆ€ n' x',
+       n' â‰¤ n â†’ âœ“{n'} (x â‹… x') â†’ P n' x' â†’ Q n' (x â‹… x') |}.
+Next Obligation.
+  intros M P Q n x1 x1' HPQ ? n3 x3 ???; simpl in *.
+  apply uPred_mono with (x1 â‹… x3);
+    eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
+Qed.
+Next Obligation. naive_solver. Qed.
+Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
+Definition uPred_wand {M} := proj1_sig uPred_wand_aux M.
+Definition uPred_wand_eq :
+  @uPred_wand = @uPred_wand_def := proj2_sig uPred_wand_aux.
+
+Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
+  {| uPred_holds n x := P n (core x) |}.
+Next Obligation.
+  intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
+Qed.
+Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
+Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
+Definition uPred_always {M} := proj1_sig uPred_always_aux M.
+Definition uPred_always_eq :
+  @uPred_always = @uPred_always_def := proj2_sig uPred_always_aux.
+
+Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
+  {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
+Next Obligation.
+  intros M P [|n] x1 x2; eauto using uPred_mono, cmra_includedN_S.
+Qed.
+Next Obligation.
+  intros M P [|n1] [|n2] x; eauto using uPred_closed, cmra_validN_S with lia.
+Qed.
+Definition uPred_later_aux : { x | x = @uPred_later_def }. by eexists. Qed.
+Definition uPred_later {M} := proj1_sig uPred_later_aux M.
+Definition uPred_later_eq :
+  @uPred_later = @uPred_later_def := proj2_sig uPred_later_aux.
+
+Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
+  {| uPred_holds n x := a â‰¼{n} x |}.
+Next Obligation.
+  intros M a n x1 x [a' Hx1] [x2 ->].
+  exists (a' â‹… x2). by rewrite (assoc op) Hx1.
+Qed.
+Next Obligation. naive_solver eauto using cmra_includedN_le. Qed.
+Definition uPred_ownM_aux : { x | x = @uPred_ownM_def }. by eexists. Qed.
+Definition uPred_ownM {M} := proj1_sig uPred_ownM_aux M.
+Definition uPred_ownM_eq :
+  @uPred_ownM = @uPred_ownM_def := proj2_sig uPred_ownM_aux.
+
+Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M :=
+  {| uPred_holds n x := âœ“{n} a |}.
+Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
+Definition uPred_cmra_valid_aux : { x | x = @uPred_cmra_valid_def }. by eexists. Qed.
+Definition uPred_cmra_valid {M A} := proj1_sig uPred_cmra_valid_aux M A.
+Definition uPred_cmra_valid_eq :
+  @uPred_cmra_valid = @uPred_cmra_valid_def := proj2_sig uPred_cmra_valid_aux.
+
+Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
+  {| uPred_holds n x := âˆ€ k yf,
+      k â‰¤ n â†’ âœ“{k} (x â‹… yf) â†’ âˆƒ x', âœ“{k} (x' â‹… yf) âˆ§ Q k x' |}.
+Next Obligation.
+  intros M Q n x1 x2 HQ [x3 Hx] k yf Hk.
+  rewrite (dist_le _ _ _ _ Hx); last lia. intros Hxy.
+  destruct (HQ k (x3 â‹… yf)) as (x'&?&?); [auto|by rewrite assoc|].
+  exists (x' â‹… x3); split; first by rewrite -assoc.
+  apply uPred_mono with x'; eauto using cmra_includedN_l.
+Qed.
+Next Obligation. naive_solver. Qed.
+Definition uPred_bupd_aux : { x | x = @uPred_bupd_def }. by eexists. Qed.
+Definition uPred_bupd {M} := proj1_sig uPred_bupd_aux M.
+Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := proj2_sig uPred_bupd_aux.
+
+Notation "â–  Ï†" := (uPred_pure Ï†%C%type)
+  (at level 20, right associativity) : uPred_scope.
+Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) : uPred_scope.
+Notation "x âŠ¥ y" := (uPred_pure (x%C%type âŠ¥ y%C%type)) : uPred_scope.
+Notation "'False'" := (uPred_pure False) : uPred_scope.
+Notation "'True'" := (uPred_pure True) : uPred_scope.
+Infix "âˆ§" := uPred_and : uPred_scope.
+Notation "(âˆ§)" := uPred_and (only parsing) : uPred_scope.
+Infix "âˆ¨" := uPred_or : uPred_scope.
+Notation "(âˆ¨)" := uPred_or (only parsing) : uPred_scope.
+Infix "â†’" := uPred_impl : uPred_scope.
+Infix "â˜…" := uPred_sep (at level 80, right associativity) : uPred_scope.
+Notation "(â˜…)" := uPred_sep (only parsing) : uPred_scope.
+Notation "P -â˜… Q" := (uPred_wand P Q)
+  (at level 99, Q at level 200, right associativity) : uPred_scope.
+Notation "âˆ€ x .. y , P" :=
+  (uPred_forall (Î» x, .. (uPred_forall (Î» y, P)) ..)%I) : uPred_scope.
+Notation "âˆƒ x .. y , P" :=
+  (uPred_exist (Î» x, .. (uPred_exist (Î» y, P)) ..)%I) : uPred_scope.
+Notation "â–¡ P" := (uPred_always P)
+  (at level 20, right associativity) : uPred_scope.
+Notation "â–· P" := (uPred_later P)
+  (at level 20, right associativity) : uPred_scope.
+Infix "â‰¡" := uPred_eq : uPred_scope.
+Notation "âœ“ x" := (uPred_cmra_valid x) (at level 20) : uPred_scope.
+Notation "|==> Q" := (uPred_bupd Q)
+  (at level 99, Q at level 200, format "|==>  Q") : uPred_scope.
+Notation "P ==â˜… Q" := (P âŠ¢ |==> Q)
+  (at level 99, Q at level 200, only parsing) : C_scope.
+Notation "P ==â˜… Q" := (P -â˜… |==> Q)%I
+  (at level 99, Q at level 200, format "P  ==â˜…  Q") : uPred_scope.
+
+Module uPred_primitive.
+Definition unseal :=
+  (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
+  uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
+  uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, uPred_bupd_eq).
+Ltac unseal := rewrite !unseal /=.
+
+Section primitive.
+Context {M : ucmraT}.
+Implicit Types Ï† : Prop.
+Implicit Types P Q : uPred M.
+Implicit Types A : Type.
+Notation "P âŠ¢ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
+Notation "P âŠ£âŠ¢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *)
+Arguments uPred_holds {_} !_ _ _ /.
+Hint Immediate uPred_in_entails.
+
+(** Non-expansiveness and setoid morphisms *)
+Global Instance pure_proper : Proper (iff ==> (âŠ£âŠ¢)) (@uPred_pure M).
+Proof. intros Ï†1 Ï†2 HÏ†. by unseal; split=> -[|n] ?; try apply HÏ†. Qed.
+Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
+Proof.
+  intros P P' HP Q Q' HQ; unseal; split=> x n' ??.
+  split; (intros [??]; split; [by apply HP|by apply HQ]).
+Qed.
+Global Instance and_proper :
+  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_and M) := ne_proper_2 _.
+Global Instance or_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
+Proof.
+  intros P P' HP Q Q' HQ; split=> x n' ??.
+  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
+Qed.
+Global Instance or_proper :
+  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_or M) := ne_proper_2 _.
+Global Instance impl_ne n :
+  Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
+Proof.
+  intros P P' HP Q Q' HQ; split=> x n' ??.
+  unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
+Qed.
+Global Instance impl_proper :
+  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_impl M) := ne_proper_2 _.
+Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
+Proof.
+  intros P P' HP Q Q' HQ; split=> n' x ??.
+  unseal; split; intros (x1&x2&?&?&?); cofe_subst x;
+    exists x1, x2; split_and!; try (apply HP || apply HQ);
+    eauto using cmra_validN_op_l, cmra_validN_op_r.
+Qed.
+Global Instance sep_proper :
+  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_sep M) := ne_proper_2 _.
+Global Instance wand_ne n :
+  Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
+Proof.
+  intros P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
+    apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
+Qed.
+Global Instance wand_proper :
+  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_wand M) := ne_proper_2 _.
+Global Instance eq_ne (A : cofeT) n :
+  Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
+Proof.
+  intros x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
+  - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
+  - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
+Qed.
+Global Instance eq_proper (A : cofeT) :
+  Proper ((â‰¡) ==> (â‰¡) ==> (âŠ£âŠ¢)) (@uPred_eq M A) := ne_proper_2 _.
+Global Instance forall_ne A n :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
+Proof.
+  by intros Î¨1 Î¨2 HÎ¨; unseal; split=> n' x; split; intros HP a; apply HÎ¨.
+Qed.
+Global Instance forall_proper A :
+  Proper (pointwise_relation _ (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_forall M A).
+Proof.
+  by intros Î¨1 Î¨2 HÎ¨; unseal; split=> n' x; split; intros HP a; apply HÎ¨.
+Qed.
+Global Instance exist_ne A n :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
+Proof.
+  intros Î¨1 Î¨2 HÎ¨.
+  unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HÎ¨.
+Qed.
+Global Instance exist_proper A :
+  Proper (pointwise_relation _ (âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_exist M A).
+Proof.
+  intros Î¨1 Î¨2 HÎ¨.
+  unseal; split=> n' x ?; split; intros [a ?]; exists a; by apply HÎ¨.
+Qed.
+Global Instance later_contractive : Contractive (@uPred_later M).
+Proof.
+  intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|].
+  apply (HPQ n'); eauto using cmra_validN_S.
+Qed.
+Global Instance later_proper' :
+  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_later M) := ne_proper _.
+Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
+Proof.
+  intros P1 P2 HP.
+  unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
+Qed.
+Global Instance always_proper :
+  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_always M) := ne_proper _.
+Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
+Proof.
+  intros a b Ha.
+  unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
+Qed.
+Global Instance ownM_proper: Proper ((â‰¡) ==> (âŠ£âŠ¢)) (@uPred_ownM M) := ne_proper _.
+Global Instance cmra_valid_ne {A : cmraT} n :
+Proper (dist n ==> dist n) (@uPred_cmra_valid M A).
+Proof.
+  intros a b Ha; unseal; split=> n' x ? /=.
+  by rewrite (dist_le _ _ _ _ Ha); last lia.
+Qed.
+Global Instance cmra_valid_proper {A : cmraT} :
+  Proper ((â‰¡) ==> (âŠ£âŠ¢)) (@uPred_cmra_valid M A) := ne_proper _.
+Global Instance bupd_ne n : Proper (dist n ==> dist n) (@uPred_bupd M).
+Proof.
+  intros P Q HPQ.
+  unseal; split=> n' x; split; intros HP k yf ??;
+    destruct (HP k yf) as (x'&?&?); auto;
+    exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
+Qed.
+Global Instance bupd_proper : Proper ((â‰¡) ==> (â‰¡)) (@uPred_bupd M) := ne_proper _.
+
+(** Introduction and elimination rules *)
+Lemma pure_intro Ï† P : Ï† â†’ P âŠ¢ â–  Ï†.
+Proof. by intros ?; unseal; split. Qed.
+Lemma pure_elim Ï† Q R : (Q âŠ¢ â–  Ï†) â†’ (Ï† â†’ Q âŠ¢ R) â†’ Q âŠ¢ R.
+Proof.
+  unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
+Qed.
+Lemma pure_forall_2 {A} (Ï† : A â†’ Prop) : (âˆ€ x : A, â–  Ï† x) âŠ¢ â–  (âˆ€ x : A, Ï† x).
+Proof. by unseal. Qed.
+
+Lemma and_elim_l P Q : P âˆ§ Q âŠ¢ P.
+Proof. by unseal; split=> n x ? [??]. Qed.
+Lemma and_elim_r P Q : P âˆ§ Q âŠ¢ Q.
+Proof. by unseal; split=> n x ? [??]. Qed.
+Lemma and_intro P Q R : (P âŠ¢ Q) â†’ (P âŠ¢ R) â†’ P âŠ¢ Q âˆ§ R.
+Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
+
+Lemma or_intro_l P Q : P âŠ¢ P âˆ¨ Q.
+Proof. unseal; split=> n x ??; left; auto. Qed.
+Lemma or_intro_r P Q : Q âŠ¢ P âˆ¨ Q.
+Proof. unseal; split=> n x ??; right; auto. Qed.
+Lemma or_elim P Q R : (P âŠ¢ R) â†’ (Q âŠ¢ R) â†’ P âˆ¨ Q âŠ¢ R.
+Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
+
+Lemma impl_intro_r P Q R : (P âˆ§ Q âŠ¢ R) â†’ P âŠ¢ Q â†’ R.
+Proof.
+  unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ;
+    naive_solver eauto using uPred_mono, uPred_closed, cmra_included_includedN.
+Qed.
+Lemma impl_elim P Q R : (P âŠ¢ Q â†’ R) â†’ (P âŠ¢ Q) â†’ P âŠ¢ R.
+Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
+
+Lemma forall_intro {A} P (Î¨ : A â†’ uPred M): (âˆ€ a, P âŠ¢ Î¨ a) â†’ P âŠ¢ âˆ€ a, Î¨ a.
+Proof. unseal; intros HPÎ¨; split=> n x ?? a; by apply HPÎ¨. Qed.
+Lemma forall_elim {A} {Î¨ : A â†’ uPred M} a : (âˆ€ a, Î¨ a) âŠ¢ Î¨ a.
+Proof. unseal; split=> n x ? HP; apply HP. Qed.
+
+Lemma exist_intro {A} {Î¨ : A â†’ uPred M} a : Î¨ a âŠ¢ âˆƒ a, Î¨ a.
+Proof. unseal; split=> n x ??; by exists a. Qed.
+Lemma exist_elim {A} (Î¦ : A â†’ uPred M) Q : (âˆ€ a, Î¦ a âŠ¢ Q) â†’ (âˆƒ a, Î¦ a) âŠ¢ Q.
+Proof. unseal; intros HÎ¦Î¨; split=> n x ? [a ?]; by apply HÎ¦Î¨ with a. Qed.
+
+Lemma eq_refl {A : cofeT} (a : A) : True âŠ¢ a â‰¡ a.
+Proof. unseal; by split=> n x ??; simpl. Qed.
+Lemma eq_rewrite {A : cofeT} a b (Î¨ : A â†’ uPred M) P
+  {HÎ¨ : âˆ€ n, Proper (dist n ==> dist n) Î¨} : (P âŠ¢ a â‰¡ b) â†’ (P âŠ¢ Î¨ a) â†’ P âŠ¢ Î¨ b.
+Proof.
+  unseal; intros Hab Ha; split=> n x ??. apply HÎ¨ with n a; auto.
+  - by symmetry; apply Hab with x.
+  - by apply Ha.
+Qed.
+Lemma eq_equiv {A : cofeT} (a b : A) : (True âŠ¢ a â‰¡ b) â†’ a â‰¡ b.
+Proof.
+  unseal=> Hab; apply equiv_dist; intros n; apply Hab with âˆ…; last done.
+  apply cmra_valid_validN, ucmra_unit_valid.
+Qed.
+Lemma eq_rewrite_contractive {A : cofeT} a b (Î¨ : A â†’ uPred M) P
+  {HÎ¨ : Contractive Î¨} : (P âŠ¢ â–· (a â‰¡ b)) â†’ (P âŠ¢ Î¨ a) â†’ P âŠ¢ Î¨ b.
+Proof.
+  unseal; intros Hab Ha; split=> n x ??. apply HÎ¨ with n a; auto.
+  - destruct n; intros m ?; first omega. apply (dist_le n); last omega.
+    symmetry. by destruct Hab as [Hab]; eapply (Hab (S n)).
+  - by apply Ha.
+Qed.
+
+(* BI connectives *)
+Lemma sep_mono P P' Q Q' : (P âŠ¢ Q) â†’ (P' âŠ¢ Q') â†’ P â˜… P' âŠ¢ Q â˜… Q'.
+Proof.
+  intros HQ HQ'; unseal.
+  split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; cofe_subst x;
+    eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
+Qed.
+Lemma True_sep_1 P : P âŠ¢ True â˜… P.
+Proof.
+  unseal; split; intros n x ??. exists (core x), x. by rewrite cmra_core_l.
+Qed.
+Lemma True_sep_2 P : True â˜… P âŠ¢ P.
+Proof.
+  unseal; split; intros n x ? (x1&x2&?&_&?); cofe_subst;
+    eauto using uPred_mono, cmra_includedN_r.
+Qed.
+Lemma sep_comm' P Q : P â˜… Q âŠ¢ Q â˜… P.
+Proof.
+  unseal; split; intros n x ? (x1&x2&?&?&?); exists x2, x1; by rewrite (comm op).
+Qed.
+Lemma sep_assoc' P Q R : (P â˜… Q) â˜… R âŠ¢ P â˜… (Q â˜… R).
+Proof.
+  unseal; split; intros n x ? (x1&x2&Hx&(y1&y2&Hy&?&?)&?).
+  exists y1, (y2 â‹… x2); split_and?; auto.
+  + by rewrite (assoc op) -Hy -Hx.
+  + by exists y2, x2.
+Qed.
+Lemma wand_intro_r P Q R : (P â˜… Q âŠ¢ R) â†’ P âŠ¢ Q -â˜… R.
+Proof.
+  unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
+  exists x, x'; split_and?; auto.
+  eapply uPred_closed with n; eauto using cmra_validN_op_l.
+Qed.
+Lemma wand_elim_l' P Q R : (P âŠ¢ Q -â˜… R) â†’ P â˜… Q âŠ¢ R.
+Proof.
+  unseal =>HPQR. split; intros n x ? (?&?&?&?&?). cofe_subst.
+  eapply HPQR; eauto using cmra_validN_op_l.
+Qed.
+
+(* Always *)
+Lemma always_mono P Q : (P âŠ¢ Q) â†’ â–¡ P âŠ¢ â–¡ Q.
+Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
+Lemma always_elim P : â–¡ P âŠ¢ P.
+Proof.
+  unseal; split=> n x ? /=.
+  eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
+Qed.
+Lemma always_idemp P : â–¡ P âŠ¢ â–¡ â–¡ P.
+Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
+
+Lemma always_pure_2 Ï† : â–  Ï† âŠ¢ â–¡ â–  Ï†.
+Proof. by unseal. Qed.
+Lemma always_forall_2 {A} (Î¨ : A â†’ uPred M) : (âˆ€ a, â–¡ Î¨ a) âŠ¢ (â–¡ âˆ€ a, Î¨ a).
+Proof. by unseal. Qed.
+Lemma always_exist_1 {A} (Î¨ : A â†’ uPred M) : (â–¡ âˆƒ a, Î¨ a) âŠ¢ (âˆƒ a, â–¡ Î¨ a).
+Proof. by unseal. Qed.
+
+Lemma always_and_sep_1 P Q : â–¡ (P âˆ§ Q) âŠ¢ â–¡ (P â˜… Q).
+Proof.
+  unseal; split=> n x ? [??].
+  exists (core x), (core x); rewrite -cmra_core_dup; auto.
+Qed.
+Lemma always_and_sep_l_1 P Q : â–¡ P âˆ§ Q âŠ¢ â–¡ P â˜… Q.
+Proof.
+  unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
+  by rewrite cmra_core_l cmra_core_idemp.
+Qed.
+
+(* Later *)
+Lemma later_mono P Q : (P âŠ¢ Q) â†’ â–· P âŠ¢ â–· Q.
+Proof.
+  unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
+Qed.
+Lemma lÃ¶b P : (â–· P â†’ P) âŠ¢ P.
+Proof.
+  unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|].
+  apply HP, IH, uPred_closed with (S n); eauto using cmra_validN_S.
+Qed.
+Lemma later_forall_2 {A} (Î¦ : A â†’ uPred M) : (âˆ€ a, â–· Î¦ a) âŠ¢ â–· âˆ€ a, Î¦ a.
+Proof. unseal; by split=> -[|n] x. Qed.
+Lemma later_exist_false {A} (Î¦ : A â†’ uPred M) :
+  (â–· âˆƒ a, Î¦ a) âŠ¢ â–· False âˆ¨ (âˆƒ a, â–· Î¦ a).
+Proof. unseal; split=> -[|[|n]] x /=; eauto. Qed.
+Lemma later_sep P Q : â–· (P â˜… Q) âŠ£âŠ¢ â–· P â˜… â–· Q.
+Proof.
+  unseal; split=> n x ?; split.
+  - destruct n as [|n]; simpl.
+    { by exists x, (core x); rewrite cmra_core_r. }
+    intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
+      as (y1&y2&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
+    exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
+  - destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
+    exists x1, x2; eauto using dist_S.
+Qed.
+Lemma later_false_excluded_middle P : â–· P âŠ¢ â–· False âˆ¨ (â–· False â†’ P).
+Proof.
+  unseal; split=> -[|n] x ? /= HP; [by left|right].
+  intros [|n'] x' ????; [|done].
+  eauto using uPred_closed, uPred_mono, cmra_included_includedN.
+Qed.
+Lemma always_later P : â–¡ â–· P âŠ£âŠ¢ â–· â–¡ P.
+Proof. by unseal. Qed.
+
+(* Own *)
+Lemma ownM_op (a1 a2 : M) :
+  uPred_ownM (a1 â‹… a2) âŠ£âŠ¢ uPred_ownM a1 â˜… uPred_ownM a2.
+Proof.
+  unseal; split=> n x ?; split.
+  - intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
+    split. by exists (core a1); rewrite cmra_core_r. by exists z.
+  - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
+    by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
+      -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
+Qed.
+Lemma always_ownM_core (a : M) : uPred_ownM a âŠ¢ â–¡ uPred_ownM (core a).
+Proof.
+  split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
+Qed.
+Lemma ownM_empty : True âŠ¢ uPred_ownM âˆ….
+Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
+Lemma later_ownM a : â–· uPred_ownM a âŠ¢ âˆƒ b, uPred_ownM b âˆ§ â–· (a â‰¡ b).
+Proof.
+  unseal; split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
+  destruct Hax as [y ?].
+  destruct (cmra_extend n x a y) as (a'&y'&Hx&?&?); auto using cmra_validN_S.
+  exists a'. rewrite Hx. eauto using cmra_includedN_l.
+Qed.
+
+(* Valid *)
+Lemma ownM_valid (a : M) : uPred_ownM a âŠ¢ âœ“ a.
+Proof.
+  unseal; split=> n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l.
+Qed.
+Lemma cmra_valid_intro {A : cmraT} (a : A) : âœ“ a â†’ True âŠ¢ âœ“ a.
+Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
+Lemma cmra_valid_elim {A : cmraT} (a : A) : Â¬ âœ“{0} a â†’ âœ“ a âŠ¢ False.
+Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
+Lemma always_cmra_valid_1 {A : cmraT} (a : A) : âœ“ a âŠ¢ â–¡ âœ“ a.
+Proof. by unseal. Qed.
+Lemma cmra_valid_weaken {A : cmraT} (a b : A) : âœ“ (a â‹… b) âŠ¢ âœ“ a.
+Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
+
+(* Basic update modality *)
+Lemma bupd_intro P : P ==â˜… P.
+Proof.
+  unseal. split=> n x ? HP k yf ?; exists x; split; first done.
+  apply uPred_closed with n; eauto using cmra_validN_op_l.
+Qed.
+Lemma bupd_mono P Q : (P âŠ¢ Q) â†’ (|==> P) ==â˜… Q.
+Proof.
+  unseal. intros HPQ; split=> n x ? HP k yf ??.
+  destruct (HP k yf) as (x'&?&?); eauto.
+  exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
+Qed.
+Lemma bupd_trans P : (|==> |==> P) ==â˜… P.
+Proof. unseal; split; naive_solver. Qed.
+Lemma bupd_frame_r P R : (|==> P) â˜… R ==â˜… P â˜… R.
+Proof.
+  unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
+  destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto.
+  { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
+  exists (x' â‹… x2); split; first by rewrite -assoc.
+  exists x', x2; split_and?; auto.
+  apply uPred_closed with n; eauto 3 using cmra_validN_op_l, cmra_validN_op_r.
+Qed.
+Lemma bupd_ownM_updateP x (Î¦ : M â†’ Prop) :
+  x ~~>: Î¦ â†’ uPred_ownM x ==â˜… âˆƒ y, â–  Î¦ y âˆ§ uPred_ownM y.
+Proof.
+  unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
+  destruct (Hup k (Some (x3 â‹… yf))) as (y&?&?); simpl in *.
+  { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. }
+  exists (y â‹… x3); split; first by rewrite -assoc.
+  exists y; eauto using cmra_includedN_l.
+Qed.
+
+(* Products *)
+Lemma prod_equivI {A B : cofeT} (x y : A * B) : x â‰¡ y âŠ£âŠ¢ x.1 â‰¡ y.1 âˆ§ x.2 â‰¡ y.2.
+Proof. by unseal. Qed.
+Lemma prod_validI {A B : cmraT} (x : A * B) : âœ“ x âŠ£âŠ¢ âœ“ x.1 âˆ§ âœ“ x.2.
+Proof. by unseal. Qed.
+
+(* Later *)
+Lemma later_equivI {A : cofeT} (x y : A) : Next x â‰¡ Next y âŠ£âŠ¢ â–· (x â‰¡ y).
+Proof. by unseal. Qed.
+
+(* Discrete *)
+Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : âœ“ a âŠ£âŠ¢ â–  âœ“ a.
+Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
+Lemma timeless_eq {A : cofeT} (a b : A) : Timeless a â†’ a â‰¡ b âŠ£âŠ¢ â–  (a â‰¡ b).
+Proof.
+  unseal=> ?. apply (anti_symm (âŠ¢)); split=> n x ?; by apply (timeless_iff n).
+Qed.
+
+(* Option *)
+Lemma option_equivI {A : cofeT} (mx my : option A) :
+  mx â‰¡ my âŠ£âŠ¢ match mx, my with
+             | Some x, Some y => x â‰¡ y | None, None => True | _, _ => False
+             end.
+Proof.
+  unseal. do 2 split. by destruct 1. by destruct mx, my; try constructor.
+Qed.
+Lemma option_validI {A : cmraT} (mx : option A) :
+  âœ“ mx âŠ£âŠ¢ match mx with Some x => âœ“ x | None => True end.
+Proof. unseal. by destruct mx. Qed.
+
+(* Functions *)
+Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f â‰¡ g âŠ£âŠ¢ âˆ€ x, f x â‰¡ g x.
+Proof. by unseal. Qed.
+Lemma cofe_moreC_equivI {A B : cofeT} (f g : A -n> B) : f â‰¡ g âŠ£âŠ¢ âˆ€ x, f x â‰¡ g x.
+Proof. by unseal. Qed.
+End primitive.
+End uPred_primitive.
diff --git a/base_logic/soundness.v b/base_logic/soundness.v
new file mode 100644
index 000000000..4f3c5f793
--- /dev/null
+++ b/base_logic/soundness.v
@@ -0,0 +1,24 @@
+From iris.base_logic Require Export primitive.
+Import uPred_entails uPred_primitive.
+
+Section adequacy.
+Context {M : ucmraT}.
+
+(** Consistency and adequancy statements *)
+Lemma soundness Ï† n : (True âŠ¢ Nat.iter n (Î» P, |==> â–· P) (@uPred_pure M Ï†)) â†’ Ï†.
+Proof.
+  cut (âˆ€ x, âœ“{n} x â†’ Nat.iter n (Î» P, |==> â–· P)%I (@uPred_pure M Ï†) n x â†’ Ï†).
+  { intros help H. eapply (help âˆ…); eauto using ucmra_unit_validN.
+    eapply H; try unseal; by eauto using ucmra_unit_validN. }
+  unseal. induction n as [|n IH]=> x Hx Hupd; auto.
+  destruct (Hupd (S n) âˆ…) as (x'&?&?); rewrite ?right_id; auto.
+  eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
+Qed.
+
+Corollary consistency_modal n :
+  Â¬ (True âŠ¢ Nat.iter n (Î» P, |==> â–· P) (False : uPred M)).
+Proof. exact (soundness False n). Qed.
+
+Corollary consistency : Â¬ (True âŠ¢ False : uPred M).
+Proof. exact (consistency_modal 0). Qed.
+End adequacy.
diff --git a/algebra/upred_tactics.v b/base_logic/tactics.v
similarity index 98%
rename from algebra/upred_tactics.v
rename to base_logic/tactics.v
index 8ccf0c127..750dd0f83 100644
--- a/algebra/upred_tactics.v
+++ b/base_logic/tactics.v
@@ -1,6 +1,5 @@
 From iris.prelude Require Import gmap.
-From iris.algebra Require Export upred.
-From iris.algebra Require Export upred_big_op.
+From iris.base_logic Require Export base_logic big_op.
 Import uPred.
 
 Module uPred_reflection. Section uPred_reflection.
diff --git a/base_logic/upred.v b/base_logic/upred.v
new file mode 100644
index 000000000..710effb26
--- /dev/null
+++ b/base_logic/upred.v
@@ -0,0 +1,172 @@
+From iris.algebra Require Export cmra.
+
+Record uPred (M : ucmraT) : Type := IProp {
+  uPred_holds :> nat â†’ M â†’ Prop;
+  uPred_mono n x1 x2 : uPred_holds n x1 â†’ x1 â‰¼{n} x2 â†’ uPred_holds n x2;
+  uPred_closed n1 n2 x : uPred_holds n1 x â†’ n2 â‰¤ n1 â†’ âœ“{n2} x â†’ uPred_holds n2 x
+}.
+Arguments uPred_holds {_} _ _ _ : simpl never.
+Add Printing Constructor uPred.
+Instance: Params (@uPred_holds) 3.
+
+Delimit Scope uPred_scope with I.
+Bind Scope uPred_scope with uPred.
+Arguments uPred_holds {_} _%I _ _.
+
+Section cofe.
+  Context {M : ucmraT}.
+
+  Inductive uPred_equiv' (P Q : uPred M) : Prop :=
+    { uPred_in_equiv : âˆ€ n x, âœ“{n} x â†’ P n x â†” Q n x }.
+  Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
+  Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
+    { uPred_in_dist : âˆ€ n' x, n' â‰¤ n â†’ âœ“{n'} x â†’ P n' x â†” Q n' x }.
+  Instance uPred_dist : Dist (uPred M) := uPred_dist'.
+  Program Instance uPred_compl : Compl (uPred M) := Î» c,
+    {| uPred_holds n x := c n n x |}.
+  Next Obligation. naive_solver eauto using uPred_mono. Qed.
+  Next Obligation.
+    intros c n1 n2 x ???; simpl in *.
+    apply (chain_cauchy c n2 n1); eauto using uPred_closed.
+  Qed.
+  Definition uPred_cofe_mixin : CofeMixin (uPred M).
+  Proof.
+    split.
+    - intros P Q; split.
+      + by intros HPQ n; split=> i x ??; apply HPQ.
+      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
+    - intros n; split.
+      + by intros P; split=> x i.
+      + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
+      + intros P Q Q' HP HQ; split=> i x ??.
+        by trans (Q i x);[apply HP|apply HQ].
+    - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
+    - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
+  Qed.
+  Canonical Structure uPredC : cofeT := CofeT (uPred M) uPred_cofe_mixin.
+End cofe.
+Arguments uPredC : clear implicits.
+
+Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
+Proof.
+  intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx.
+Qed.
+Instance uPred_proper {M} (P : uPred M) n : Proper ((â‰¡) ==> iff) (P n).
+Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.
+
+Lemma uPred_holds_ne {M} (P Q : uPred M) n1 n2 x :
+  P â‰¡{n2}â‰¡ Q â†’ n2 â‰¤ n1 â†’ âœ“{n2} x â†’ Q n1 x â†’ P n2 x.
+Proof.
+  intros [Hne] ???. eapply Hne; try done.
+  eapply uPred_closed; eauto using cmra_validN_le.
+Qed.
+
+(** functor *)
+Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
+  `{!CMRAMonotone f} (P : uPred M1) :
+  uPred M2 := {| uPred_holds n x := P n (f x) |}.
+Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
+Next Obligation. naive_solver eauto using uPred_closed, cmra_monotone_validN. Qed.
+
+Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
+  `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
+Proof.
+  intros x1 x2 Hx; split=> n' y ??.
+  split; apply Hx; auto using cmra_monotone_validN.
+Qed.
+Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P â‰¡ P.
+Proof. by split=> n x ?. Qed.
+Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3)
+    `{!CMRAMonotone f, !CMRAMonotone g} (P : uPred M3):
+  uPred_map (g â—Ž f) P â‰¡ uPred_map f (uPred_map g P).
+Proof. by split=> n x Hx. Qed.
+Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2)
+      `{!CMRAMonotone f} `{!CMRAMonotone g}:
+  (âˆ€ x, f x â‰¡ g x) â†’ âˆ€ x, uPred_map f x â‰¡ uPred_map g x.
+Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
+Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
+  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 â†’ uPredC M2).
+Lemma uPredC_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
+    `{!CMRAMonotone f, !CMRAMonotone g} n :
+  f â‰¡{n}â‰¡ g â†’ uPredC_map f â‰¡{n}â‰¡ uPredC_map g.
+Proof.
+  by intros Hfg P; split=> n' y ??;
+    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
+Qed.
+
+Program Definition uPredCF (F : urFunctor) : cFunctor := {|
+  cFunctor_car A B := uPredC (urFunctor_car F B A);
+  cFunctor_map A1 A2 B1 B2 fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
+|}.
+Next Obligation.
+  intros F A1 A2 B1 B2 n P Q HPQ.
+  apply uPredC_map_ne, urFunctor_ne; split; by apply HPQ.
+Qed.
+Next Obligation.
+  intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
+  apply uPred_map_ext=>y. by rewrite urFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' P; simpl. rewrite -uPred_map_compose.
+  apply uPred_map_ext=>y; apply urFunctor_compose.
+Qed.
+
+Instance uPredCF_contractive F :
+  urFunctorContractive F â†’ cFunctorContractive (uPredCF F).
+Proof.
+  intros ? A1 A2 B1 B2 n P Q HPQ.
+  apply uPredC_map_ne, urFunctor_contractive=> i ?; split; by apply HPQ.
+Qed.
+
+(** logical entailement *)
+Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
+  { uPred_in_entails : âˆ€ n x, âœ“{n} x â†’ P n x â†’ Q n x }.
+Hint Extern 0 (uPred_entails _ _) => reflexivity.
+Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
+
+Hint Resolve uPred_mono uPred_closed : uPred_def.
+
+(** Notations *)
+Notation "P âŠ¢ Q" := (uPred_entails P%I Q%I)
+  (at level 99, Q at level 200, right associativity) : C_scope.
+Notation "(âŠ¢)" := uPred_entails (only parsing) : C_scope.
+Notation "P âŠ£âŠ¢ Q" := (equiv (A:=uPred _) P%I Q%I)
+  (at level 95, no associativity) : C_scope.
+Notation "(âŠ£âŠ¢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
+
+Module uPred_entails.
+Section entails.
+Context {M : ucmraT}.
+Implicit Types P Q : uPred M.
+
+Global Instance: PreOrder (@uPred_entails M).
+Proof.
+  split.
+  - by intros P; split=> x i.
+  - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
+Qed.
+Global Instance: AntiSymm (âŠ£âŠ¢) (@uPred_entails M).
+Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
+
+Lemma equiv_spec P Q : (P âŠ£âŠ¢ Q) â†” (P âŠ¢ Q) âˆ§ (Q âŠ¢ P).
+Proof.
+  split; [|by intros [??]; apply (anti_symm (âŠ¢))].
+  intros HPQ; split; split=> x i; apply HPQ.
+Qed.
+Lemma equiv_entails P Q : (P âŠ£âŠ¢ Q) â†’ (P âŠ¢ Q).
+Proof. apply equiv_spec. Qed.
+Lemma equiv_entails_sym P Q : (Q âŠ£âŠ¢ P) â†’ (P âŠ¢ Q).
+Proof. apply equiv_spec. Qed.
+Global Instance entails_proper :
+  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢) ==> iff) ((âŠ¢) : relation (uPred M)).
+Proof.
+  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
+  - by trans P1; [|trans Q1].
+  - by trans P2; [|trans Q2].
+Qed.
+Lemma entails_equiv_l (P Q R : uPred M) : (P âŠ£âŠ¢ Q) â†’ (Q âŠ¢ R) â†’ (P âŠ¢ R).
+Proof. by intros ->. Qed.
+Lemma entails_equiv_r (P Q R : uPred M) : (P âŠ¢ Q) â†’ (Q âŠ£âŠ¢ R) â†’ (P âŠ¢ R).
+Proof. by intros ? <-. Qed.
+End entails.
+End uPred_entails.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index be6417d58..a9b9db7fb 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.prelude Require Import functions.
-From iris.algebra Require Import upred_big_op.
+From iris.base_logic Require Import big_op.
 From iris.program_logic Require Import saved_prop sts.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib.barrier Require Import protocol.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index a140c5b5b..de9d3c55b 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Export weakestpre.
-From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
+From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.base_logic Require Import big_op soundness.
 From iris.program_logic Require Import wsat.
 From iris.proofmode Require Import tactics.
 Import uPred.
@@ -144,12 +145,12 @@ Theorem wp_adequacy Î£ `{irisPreG Î› Î£} e Ïƒ Ï† :
 Proof.
   intros Hwp; split.
   - intros t2 Ïƒ2 v2 [n ?]%rtc_nsteps.
-    eapply (adequacy (M:=iResUR Î£) _ (S (S (S n)))); iIntros "".
+    eapply (soundness (M:=iResUR Î£) _ (S (S (S n)))); iIntros "".
     rewrite Nat_iter_S. iUpd (iris_alloc Ïƒ) as (?) "(?&?&?&HÏƒ)".
     iUpdIntro. iNext. iApply wptp_result; eauto.
     iFrame. iSplitL. by iApply Hwp. by iApply big_sepL_nil.
   - intros t2 Ïƒ2 e2 [n ?]%rtc_nsteps ?.
-    eapply (adequacy (M:=iResUR Î£) _ (S (S (S n)))); iIntros "".
+    eapply (soundness (M:=iResUR Î£) _ (S (S (S n)))); iIntros "".
     rewrite Nat_iter_S. iUpd (iris_alloc Ïƒ) as (?) "(Hw & HE & HÏƒ & HÏƒf)".
     iUpdIntro. iNext. iApply wptp_safe; eauto.
     iFrame "Hw HE HÏƒ". iSplitL. by iApply Hwp. by iApply big_sepL_nil.
@@ -162,7 +163,7 @@ Theorem wp_invariance Î£ `{irisPreG Î› Î£} e Ïƒ1 t2 Ïƒ2 I Ï† Î¦ :
   Ï† Ïƒ2.
 Proof.
   intros Hwp HI [n ?]%rtc_nsteps.
-  eapply (adequacy (M:=iResUR Î£) _ (S (S (S n)))); iIntros "".
+  eapply (soundness (M:=iResUR Î£) _ (S (S (S n)))); iIntros "".
   rewrite Nat_iter_S. iUpd (iris_alloc Ïƒ1) as (?) "(Hw & HE & ? & HÏƒ)".
   rewrite fupd_eq in Hwp.
   iUpd (Hwp _ with "HÏƒ [Hw HE]") as ">(? & ? & ? & ?)"; first by iFrame.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index d089851c4..28d2f6c83 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,6 +1,7 @@
 From iris.program_logic Require Export invariants.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
+From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 Import uPred.
 
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index bfb964e97..afba03c55 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Export invariants.
-From iris.algebra Require Import auth gmap agree upred_big_op.
+From iris.algebra Require Import auth gmap agree.
+From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 Import uPred.
 
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 7b1d8a00b..ec7d171e5 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import upred.
+From iris.base_logic Require Import base_logic soundness.
 From iris.proofmode Require Import tactics.
 
 (** This proves that we need the â–· in a "Saved Proposition" construction with
@@ -39,7 +39,7 @@ Module savedprop. Section savedprop.
 
   Lemma contradiction : False.
   Proof.
-    apply (@uPred.adequacy M False 1); simpl.
+    apply (@soundness M False 1); simpl.
     iIntros "". iUpd A_alloc as (i) "#H".
     iPoseProof (saved_NA with "H") as "HN".
     iUpdIntro. iNext.
diff --git a/program_logic/fancy_updates.v b/program_logic/fancy_updates.v
index f1c5ec814..7d5a78443 100644
--- a/program_logic/fancy_updates.v
+++ b/program_logic/fancy_updates.v
@@ -1,6 +1,7 @@
 From iris.program_logic Require Export iris.
 From iris.program_logic Require Import wsat.
-From iris.algebra Require Import upred_big_op gmap.
+From iris.algebra Require Import gmap.
+From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
 Import uPred.
 
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 826dd1234..a69bd62bd 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Export model.
 From iris.algebra Require Import iprod gmap.
+From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import classes.
 Import uPred.
 
diff --git a/program_logic/iris.v b/program_logic/iris.v
index 8269a5982..17d827315 100644
--- a/program_logic/iris.v
+++ b/program_logic/iris.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export ghost_ownership language.
 From iris.prelude Require Export coPset.
-From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
+From iris.algebra Require Import gmap auth agree gset coPset.
 
 Class irisPreG (Î› : language) (Î£ : gFunctors) : Set := IrisPreG {
   state_inG :> inG Î£ (authR (optionUR (exclR (stateC Î›))));
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 9cf5f0ae6..410250333 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import wsat.
-From iris.algebra Require Export upred_big_op.
+From iris.base_logic Require Export big_op.
 From iris.proofmode Require Import tactics.
 
 Section lifting.
diff --git a/program_logic/model.v b/program_logic/model.v
index f0199b825..62c7ceb05 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export upred.
+From iris.base_logic Require Export base_logic.
 From iris.algebra Require Import iprod gmap.
 From iris.algebra Require cofe_solver.
 
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 582174638..e38b71ea6 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export fancy_updates.
 From iris.program_logic Require Import wsat.
-From iris.algebra Require Import upred_big_op.
+From iris.base_logic Require Import big_op.
 From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics classes.
 Import uPred.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index f4d33686a..3315aa668 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Export iris.
-From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
+From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 
 Definition invariant_unfold {Î£} (P : iProp Î£) : agree (later (iPreProp Î£)) :=
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 31c2b0471..7dc421a0e 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -1,5 +1,6 @@
 From iris.proofmode Require Export classes.
-From iris.algebra Require Import upred_big_op gmap.
+From iris.algebra Require Import gmap.
+From iris.base_logic Require Import big_op.
 Import uPred.
 
 Section classes.
diff --git a/proofmode/classes.v b/proofmode/classes.v
index 3cc3e6995..3c3316bf2 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export upred.
+From iris.base_logic Require Export base_logic.
 Import uPred.
 
 Section classes.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index ffe86380c..30a1dfd38 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Export upred.
-From iris.algebra Require Import upred_big_op upred_tactics.
+From iris.base_logic Require Export base_logic.
+From iris.base_logic Require Import big_op tactics.
 From iris.proofmode Require Export environments classes.
 From iris.prelude Require Import stringmap hlist.
 Import uPred.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index f2a640bb1..06b6e95e9 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Import intro_patterns spec_patterns sel_patterns.
-From iris.algebra Require Export upred.
+From iris.base_logic Require Export base_logic.
 From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.
 From iris.prelude Require Import stringmap hlist.
diff --git a/tests/atomic.v b/tests/atomic.v
index 251f033f7..151517dbb 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export hoare weakestpre.
-From iris.algebra Require Import upred_big_op.
+From iris.base_logic Require Import big_op.
 From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics.
 Import uPred.
-- 
GitLab