diff --git a/_CoqProject b/_CoqProject
index 582ae30e99b1093d48784ab918f0eaaab6ec6308..1c6bf74ca80877a9eeb8858e30a552b7395cc1c1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -26,6 +26,7 @@ theories/algebra/gmultiset.v
 theories/algebra/coPset.v
 theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
+theories/bi/notation.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v
 theories/bi/derived_laws_bi.v
@@ -44,9 +45,10 @@ theories/bi/lib/laterable.v
 theories/bi/lib/atomic.v
 theories/bi/lib/core.v
 theories/base_logic/upred.v
+theories/base_logic/bi.v
 theories/base_logic/derived.v
+theories/base_logic/proofmode.v
 theories/base_logic/base_logic.v
-theories/base_logic/soundness.v
 theories/base_logic/double_negation.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 40a3d9a3eea6dde15f21c9faa89123226605d00e..5059f6575fa7f53f83a3c406545d7ea703a88aca 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,52 +1,12 @@
-From iris.base_logic Require Export derived.
+From iris.base_logic Require Export derived proofmode.
 From iris.bi Require Export bi.
-From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 
 (* The trick of having multiple [uPred] modules, which are all exported in
 another [uPred] module is by Jason Gross and described in:
 https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00069.html *)
 Module Import uPred.
-  Export upred.uPred.
+  Export base_logic.bi.uPred.
   Export derived.uPred.
-  Export bi.
+  Export bi.bi.
 End uPred.
-
-(* Setup of the proof mode *)
-Section class_instances.
-Context {M : ucmraT}.
-Implicit Types P Q R : uPred M.
-
-Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
-  @IntoPure (uPredI M) (✓ a) (✓ a).
-Proof. by rewrite /IntoPure discrete_valid. Qed.
-
-Global Instance from_pure_cmra_valid {A : cmraT} af (a : A) :
-  @FromPure (uPredI M) af (✓ a) (✓ a).
-Proof.
-  rewrite /FromPure. eapply bi.pure_elim; [by apply affinely_if_elim|]=> ?.
-  rewrite -cmra_valid_intro //. by apply pure_intro.
-Qed.
-
-Global Instance from_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 →
-  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
-Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
-  IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
-  FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros ? H. rewrite /FromAnd (is_op a) ownM_op.
-  destruct H; by rewrite persistent_and_sep.
-Qed.
-
-Global Instance into_and_ownM p (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros. apply intuitionistically_if_mono. by rewrite (is_op a) ownM_op sep_and.
-Qed.
-
-Global Instance into_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
-End class_instances.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
new file mode 100644
index 0000000000000000000000000000000000000000..1b7fdb09dd1713dc4c55bbb7390d58783e760de7
--- /dev/null
+++ b/theories/base_logic/bi.v
@@ -0,0 +1,227 @@
+From iris.bi Require Export derived_connectives updates plainly.
+From iris.base_logic Require Export upred.
+Import uPred_primitive.
+
+(** BI instances for uPred, and re-stating the remaining primitive laws in terms
+of the BI interface.  This file does *not* unseal. *)
+
+Definition uPred_emp {M} : uPred M := uPred_pure True.
+
+Local Existing Instance entails_po.
+
+Lemma uPred_bi_mixin (M : ucmraT) :
+  BiMixin
+    uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
+    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
+    uPred_persistently.
+Proof.
+  split.
+  - exact: entails_po.
+  - exact: equiv_spec.
+  - exact: pure_ne.
+  - exact: and_ne.
+  - exact: or_ne.
+  - exact: impl_ne.
+  - exact: forall_ne.
+  - exact: exist_ne.
+  - exact: sep_ne.
+  - exact: wand_ne.
+  - exact: persistently_ne.
+  - exact: pure_intro.
+  - exact: pure_elim'.
+  - exact: @pure_forall_2.
+  - exact: and_elim_l.
+  - exact: and_elim_r.
+  - exact: and_intro.
+  - exact: or_intro_l.
+  - exact: or_intro_r.
+  - exact: or_elim.
+  - exact: impl_intro_r.
+  - exact: impl_elim_l'.
+  - exact: @forall_intro.
+  - exact: @forall_elim.
+  - exact: @exist_intro.
+  - exact: @exist_elim.
+  - exact: sep_mono.
+  - exact: True_sep_1. 
+  - exact: True_sep_2.
+  - exact: sep_comm'.
+  - exact: sep_assoc'.
+  - exact: wand_intro_r.
+  - exact: wand_elim_l'.
+  - exact: persistently_mono.
+  - exact: persistently_idemp_2.
+  - (* emp ⊢ <pers> emp (ADMISSIBLE) *)
+    trans (uPred_forall (M:=M) (λ _ : False, uPred_persistently uPred_emp)).
+    + apply forall_intro=>[[]].
+    + etrans; first exact: persistently_forall_2.
+      apply persistently_mono. exact: pure_intro.
+  - exact: @persistently_forall_2.
+  - exact: @persistently_exist_1.
+  - (* <pers> P ∗ Q ⊢ <pers> P (ADMISSIBLE) *)
+    intros. etrans; first exact: sep_comm'.
+    etrans; last exact: True_sep_2.
+    apply sep_mono; last done.
+    exact: pure_intro.
+  - exact: persistently_and_sep_l_1.
+Qed.
+
+Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
+  uPred_entails uPred_pure uPred_or uPred_impl
+  (@uPred_forall M) (@uPred_exist M) uPred_sep
+  uPred_persistently (@uPred_internal_eq M) uPred_later.
+Proof.
+  split.
+  - exact: later_contractive.
+  - exact: internal_eq_ne.
+  - exact: @internal_eq_refl.
+  - exact: @internal_eq_rewrite.
+  - exact: @fun_ext.
+  - exact: @sig_eq.
+  - exact: @discrete_eq_1.
+  - exact: @later_eq_1.
+  - exact: @later_eq_2.
+  - exact: later_mono.
+  - exact: later_intro.
+  - exact: @later_forall_2.
+  - exact: @later_exist_false.
+  - exact: later_sep_1.
+  - exact: later_sep_2.
+  - exact: later_persistently_1.
+  - exact: later_persistently_2.
+  - exact: later_false_em.
+Qed.
+
+Canonical Structure uPredI (M : ucmraT) : bi :=
+  {| bi_ofe_mixin := ofe_mixin_of (uPred M); bi_bi_mixin := uPred_bi_mixin M |}.
+Canonical Structure uPredSI (M : ucmraT) : sbi :=
+  {| sbi_ofe_mixin := ofe_mixin_of (uPred M);
+     sbi_bi_mixin := uPred_bi_mixin M; sbi_sbi_mixin := uPred_sbi_mixin M |}.
+
+Coercion uPred_valid {M} : uPred M → Prop := bi_emp_valid.
+
+Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly.
+Proof.
+  split.
+  - exact: plainly_ne.
+  - exact: plainly_mono.
+  - exact: plainly_elim_persistently.
+  - exact: plainly_idemp_2.
+  - exact: @plainly_forall_2.
+  - exact: persistently_impl_plainly.
+  - exact: plainly_impl_plainly.
+  - (* P ⊢ ■ emp (ADMISSIBLE) *)
+    intros P.
+    trans (uPred_forall (M:=M) (λ _ : False , uPred_plainly uPred_emp)).
+    + apply forall_intro=>[[]].
+    + etrans; first exact: plainly_forall_2.
+      apply plainly_mono. exact: pure_intro.
+  - (* ■ P ∗ Q ⊢ ■ P (ADMISSIBLE) *)
+    intros P Q. etrans; last exact: True_sep_2.
+    etrans; first exact: sep_comm'.
+    apply sep_mono; last done.
+    exact: pure_intro.
+  - exact: prop_ext.
+  - exact: later_plainly_1.
+  - exact: later_plainly_2.
+Qed.
+Global Instance uPred_plainlyC M : BiPlainly (uPredSI M) :=
+  {| bi_plainly_mixin := uPred_plainly_mixin M |}.
+
+Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
+Proof.
+  split.
+  - exact: bupd_ne.
+  - exact: bupd_intro.
+  - exact: bupd_mono.
+  - exact: bupd_trans.
+  - exact: bupd_frame_r.
+Qed.
+Global Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
+
+Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredSI M).
+Proof. exact: bupd_plainly. Qed.
+
+(** extra BI instances *)
+
+Global Instance uPred_affine : BiAffine (uPredI M) | 0.
+Proof. intros P Q. exact: pure_intro. Qed.
+(* Also add this to the global hint database, otherwise [eauto] won't work for
+many lemmas that have [BiAffine] as a premise. *)
+Hint Immediate uPred_affine.
+
+Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M).
+Proof. exact: @plainly_exist_1. Qed.
+
+(** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
+
+Module uPred.
+
+Section restate.
+Context {M : ucmraT}.
+Implicit Types φ : Prop.
+Implicit Types P Q : uPred M.
+Implicit Types A : Type.
+
+(* Force implicit argument M *)
+Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
+Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
+
+Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
+Global Instance cmra_valid_ne {A : cmraT} : NonExpansive (@uPred_cmra_valid M A)
+  := uPred_primitive.cmra_valid_ne.
+
+(** Re-exporting primitive Own and valid lemmas *)
+Lemma ownM_op (a1 a2 : M) :
+  uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
+Proof. exact: uPred_primitive.ownM_op. Qed.
+Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
+Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
+Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
+Proof. exact: uPred_primitive.ownM_unit. Qed.
+Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
+Proof. exact: uPred_primitive.later_ownM. Qed.
+Lemma bupd_ownM_updateP x (Φ : M → Prop) :
+  x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
+Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
+
+Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
+Proof. exact: uPred_primitive.ownM_valid. Qed.
+Lemma cmra_valid_intro {A : cmraT} P (a : A) : ✓ a → P ⊢ (✓ a).
+Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
+Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
+Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
+Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■ ✓ a.
+Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
+Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
+Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
+Proof. exact: uPred_primitive.prod_validI. Qed.
+Lemma option_validI {A : cmraT} (mx : option A) :
+  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
+Proof. exact: uPred_primitive.option_validI. Qed.
+Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+Proof. exact: uPred_primitive.discrete_valid. Qed.
+Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
+
+(** Consistency/soundness statement *)
+Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
+Proof. exact: uPred_primitive.soundness. Qed.
+
+End restate.
+
+(** New unseal tactic that also unfolds the BI layer.
+    This is used by [base_logic.double_negation].
+    TODO: Can we get rid of this? *)
+Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
+  unfold bi_emp; simpl; unfold sbi_emp; simpl;
+  unfold uPred_emp, bupd, bi_bupd_bupd, bi_pure,
+  bi_and, bi_or, bi_impl, bi_forall, bi_exist,
+  bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl;
+  unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
+  sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently; simpl;
+  unfold plainly, bi_plainly_plainly; simpl;
+  uPred_primitive.unseal.
+
+End uPred.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index e1c324096dbb1f37b9d3f34de057d45cf4a5987f..8ea72840f1c1e62ec2aab270564fca39b25b64e5 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,7 +1,10 @@
-From iris.base_logic Require Export upred.
+From iris.base_logic Require Export bi.
 From iris.bi Require Export bi.
 Set Default Proof Using "Type".
-Import upred.uPred bi.
+Import bi base_logic.bi.uPred.
+
+(** Derived laws for Iris-specific primitive connectives (own, valid).
+    This file does NOT unseal! *)
 
 Module uPred.
 Section derived.
@@ -14,7 +17,20 @@ Implicit Types A : Type.
 Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
-(* Own and valid derived *)
+(** Propers *)
+Global Instance uPred_valid_proper : Proper ((⊣⊢) ==> iff) (@uPred_valid M).
+Proof. solve_proper. Qed.
+Global Instance uPred_valid_mono : Proper ((⊢) ==> impl) (@uPred_valid M).
+Proof. solve_proper. Qed.
+Global Instance uPred_valid_flip_mono :
+  Proper (flip (⊢) ==> flip impl) (@uPred_valid M).
+Proof. solve_proper. Qed.
+
+Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
+Global Instance cmra_valid_proper {A : cmraT} :
+  Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
+
+(** Own and valid derived *)
 Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
 Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
 Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
@@ -43,7 +59,7 @@ Proof.
   by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
 Qed.
 
-(* Timeless instances *)
+(** Timeless instances *)
 Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
   Timeless (✓ a : uPred M)%I.
 Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
@@ -56,12 +72,12 @@ Proof.
     auto using and_elim_l, and_elim_r.
 Qed.
 
-(* Plainness *)
+(** Plainness *)
 Global Instance cmra_valid_plain {A : cmraT} (a : A) :
   Plain (✓ a : uPred M)%I.
 Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
 
-(* Persistence *)
+(** Persistence *)
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
   Persistent (✓ a : uPred M)%I.
 Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
@@ -70,13 +86,19 @@ Proof.
   intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
 Qed.
 
-(* For big ops *)
+(** For big ops *)
 Global Instance uPred_ownM_sep_homomorphism :
   MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
+
+
+(** Consistency/soundness statement *)
+Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I.
+Proof. exact (soundness False n). Qed.
+
+Corollary consistency : ¬(False : uPred M)%I.
+Proof. exact (consistency_modal 0). Qed.
+
 End derived.
 
-(* Also add this to the global hint database, otherwise [eauto] won't work for
-many lemmas that have [BiAffine] as a premise. *)
-Hint Immediate uPred_affine.
 End uPred.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index a2bdd3d2e073017132e306078a23ac8a5d461ee7..a9d78acb9ff6502969e1c11c83253d1c951d4cbf 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -118,7 +118,7 @@ Lemma own_alloc_strong a (G : gset gname) :
 Proof.
   intros Ha.
   rewrite -(bupd_mono (∃ m, ⌜∃ γ, γ ∉ G ∧ m = iRes_singleton γ a⌝ ∧ uPred_ownM m)%I).
-  - rewrite /uPred_valid /bi_emp_valid ownM_unit.
+  - rewrite /uPred_valid /bi_emp_valid (ownM_unit emp).
     eapply bupd_ownM_updateP, (ofe_fun_singleton_updateP_empty (inG_id _));
       first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
       naive_solver.
@@ -168,7 +168,7 @@ Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
 
 Lemma own_unit A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
 Proof.
-  rewrite /uPred_valid /bi_emp_valid ownM_unit !own_eq /own_def.
+  rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
   apply bupd_ownM_update, ofe_fun_singleton_update_empty.
   apply (alloc_unit_singleton_update (cmra_transport inG_prf ε)); last done.
   - apply cmra_transport_valid, ucmra_unit_valid.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
new file mode 100644
index 0000000000000000000000000000000000000000..6caa4627b3f435395fb0917bf1295258aff8c3db
--- /dev/null
+++ b/theories/base_logic/proofmode.v
@@ -0,0 +1,43 @@
+From iris.base_logic Require Export derived.
+From iris.algebra Require Import proofmode_classes.
+
+Import base_logic.bi.uPred.
+
+(* Setup of the proof mode *)
+Section class_instances.
+Context {M : ucmraT}.
+Implicit Types P Q R : uPred M.
+
+Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
+  @IntoPure (uPredI M) (✓ a) (✓ a).
+Proof. by rewrite /IntoPure discrete_valid. Qed.
+
+Global Instance from_pure_cmra_valid {A : cmraT} af (a : A) :
+  @FromPure (uPredI M) af (✓ a) (✓ a).
+Proof.
+  rewrite /FromPure. eapply bi.pure_elim; [by apply bi.affinely_if_elim|]=> ?.
+  rewrite -uPred.cmra_valid_intro //.
+Qed.
+
+Global Instance from_sep_ownM (a b1 b2 : M) :
+  IsOp a b1 b2 →
+  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
+Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
+  IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
+  FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  intros ? H. rewrite /FromAnd (is_op a) ownM_op.
+  destruct H; by rewrite bi.persistent_and_sep.
+Qed.
+
+Global Instance into_and_ownM p (a b1 b2 : M) :
+  IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  intros. apply bi.intuitionistically_if_mono. by rewrite (is_op a) ownM_op bi.sep_and.
+Qed.
+
+Global Instance into_sep_ownM (a b1 b2 : M) :
+  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
+End class_instances.
diff --git a/theories/base_logic/soundness.v b/theories/base_logic/soundness.v
deleted file mode 100644
index fc1093642099148d7ab34c0ac72dcd401eed90d7..0000000000000000000000000000000000000000
--- a/theories/base_logic/soundness.v
+++ /dev/null
@@ -1,21 +0,0 @@
-From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type".
-Import uPred.
-
-Section adequacy.
-Context {M : ucmraT}.
-
-(** Consistency and adequancy statements *)
-Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
-Proof.
-  cut ((▷^n ⌜ φ ⌝ : uPred M)%I n ε → φ).
-  { intros help H. eapply help, H; eauto using ucmra_unit_validN. by unseal. }
-  rewrite /sbi_laterN; unseal. induction n as [|n IH]=> H; auto.
-Qed.
-
-Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I.
-Proof. exact (soundness False n). Qed.
-
-Corollary consistency : ¬(False : uPred M)%I.
-Proof. exact (consistency_modal 0). Qed.
-End adequacy.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 2c628625d0f8ae1ffbe7acfa07cbc25887121620..5f1f20de0d7b30ad11936b54529fcf378206e6aa 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export cmra updates.
-From iris.bi Require Export derived_connectives updates plainly.
+From iris.bi Require Import notation.
 From stdpp Require Import finite.
+From Coq.Init Require Import Nat.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption].
@@ -52,13 +53,11 @@ Record uPred (M : ucmraT) : Type := IProp {
   uPred_mono n1 n2 x1 x2 :
     uPred_holds n1 x1 → x1 ≼{n1} x2 → n2 ≤ n1 → uPred_holds n2 x2
 }.
-Arguments uPred_holds {_} _ _ _ : simpl never.
+Bind Scope bi_scope with uPred.
+Arguments uPred_holds {_} _%I _ _ : simpl never.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.
 
-Bind Scope bi_scope with uPred.
-Arguments uPred_holds {_} _%I _ _.
-
 Section cofe.
   Context {M : ucmraT}.
 
@@ -199,8 +198,6 @@ Definition uPred_pure {M} := uPred_pure_aux.(unseal) M.
 Definition uPred_pure_eq :
   @uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
 
-Definition uPred_emp {M} : uPred M := 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.
@@ -278,7 +275,7 @@ Definition uPred_wand_eq :
 (* Equivalently, this could be `∀ y, P n y`.  That's closer to the intuition
    of "embedding the step-indexed logic in Iris", but the two are equivalent
    because Iris is afine.  The following is easier to work with. *)
-Program Definition uPred_plainly_def {M} : Plainly (uPred M) := λ P,
+Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n ε |}.
 Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
 Definition uPred_plainly_aux : seal (@uPred_plainly_def). by eexists. Qed.
@@ -335,391 +332,481 @@ Next Obligation.
   exists (x' â‹… x3); split; first by rewrite -assoc.
   eauto using uPred_mono, cmra_includedN_l.
 Qed.
-Definition uPred_bupd_aux {M} : seal (@uPred_bupd_def M). by eexists. Qed.
-Definition uPred_bupd {M} : BUpd (uPred M) := uPred_bupd_aux.(unseal).
-Definition uPred_bupd_eq {M} :
-  @bupd _ uPred_bupd = @uPred_bupd_def M := uPred_bupd_aux.(seal_eq).
+Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. Qed.
+Definition uPred_bupd {M} := uPred_bupd_aux.(unseal) M.
+Definition uPred_bupd_eq :
+  @uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq).
+
+(** Global uPred-specific Notation *)
+Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
 
-Module uPred_unseal.
+(** Promitive logical rules.
+    These are not directly usable later because they do not refer to the BI
+    connectives. *)
+Module uPred_primitive.
 Definition unseal_eqs :=
   (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
   uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
   uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
   uPred_cmra_valid_eq, @uPred_bupd_eq).
-Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
-  unfold bi_emp; simpl; unfold sbi_emp; simpl;
-  unfold uPred_emp, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
-  bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl;
-  unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
-  sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently; simpl;
-  unfold plainly, bi_plainly_plainly; simpl;
+Ltac unseal :=
   rewrite !unseal_eqs /=.
-End uPred_unseal.
-Import uPred_unseal.
 
-Local Arguments uPred_holds {_} !_ _ _ /.
+Section primitive.
+Context {M : ucmraT}.
+Implicit Types φ : Prop.
+Implicit Types P Q : uPred M.
+Implicit Types A : Type.
+Arguments uPred_holds {_} !_ _ _ /.
+Hint Immediate uPred_in_entails.
 
-Lemma uPred_bi_mixin (M : ucmraT) :
-  BiMixin
-    uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
-    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
-    uPred_persistently.
+Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
+Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope.
+Notation "P ⊣⊢ Q" := (@uPred_equiv M P%I Q%I) : stdpp_scope.
+Notation "(⊣⊢)" := (@uPred_equiv M) (only parsing) : stdpp_scope.
+
+Notation "'True'" := (uPred_pure True) : bi_scope.
+Notation "'False'" := (uPred_pure False) : bi_scope.
+Notation "'⌜' φ '⌝'" := (uPred_pure φ%type%stdpp) : bi_scope.
+Infix "∧" := uPred_and : bi_scope.
+Infix "∨" := uPred_or : bi_scope.
+Infix "→" := uPred_impl : bi_scope.
+Notation "∀ x .. y , P" :=
+  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)) : bi_scope.
+Notation "∃ x .. y , P" :=
+  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)) : bi_scope.
+Infix "∗" := uPred_sep : bi_scope.
+Infix "-∗" := uPred_wand : bi_scope.
+Notation "â–¡ P" := (uPred_persistently P) : bi_scope.
+Notation "â–  P" := (uPred_plainly P) : bi_scope.
+Notation "x ≡ y" := (uPred_internal_eq x y) : bi_scope.
+Notation "â–· P" := (uPred_later P) : bi_scope.
+Notation "|==> P" := (uPred_bupd P) : bi_scope.
+
+(** Entailment *)
+Lemma entails_po : PreOrder (⊢).
 Proof.
   split.
-  - (* PreOrder uPred_entails *)
-    split.
-    + by intros P; split=> x i.
-    + by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
-  - (* (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P) *)
-    intros P Q. split.
-    + intros HPQ; split; split=> x i; apply HPQ.
-    + intros [HPQ HQP]; split=> x n; by split; [apply HPQ|apply HQP].
-  - (* Proper (iff ==> dist n) (@uPred_pure M) *)
-    intros φ1 φ2 Hφ. by unseal; split=> -[|n] ?; try apply Hφ.
-  - (* NonExpansive2 uPred_and *)
-    intros n P P' HP Q Q' HQ; unseal; split=> x n' ??.
-    split; (intros [??]; split; [by apply HP|by apply HQ]).
-  - (* NonExpansive2 uPred_or *)
-    intros n P P' HP Q Q' HQ; split=> x n' ??.
-    unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
-  - (* NonExpansive2 uPred_impl *)
-    intros n P P' HP Q Q' HQ; split=> x n' ??.
-    unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
-  - (* Proper (pointwise_relation A (dist n) ==> dist n) uPred_forall *)
-    by intros A n Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
-  - (* Proper (pointwise_relation A (dist n) ==> dist n) uPred_exist *)
-    intros A n Ψ1 Ψ2 HΨ.
-    unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
-  - (* NonExpansive2 uPred_sep *)
-    intros n P P' HP Q Q' HQ; split=> n' x ??.
-    unseal; split; intros (x1&x2&?&?&?); ofe_subst x;
-      exists x1, x2; split_and!; try (apply HP || apply HQ);
-      eauto using cmra_validN_op_l, cmra_validN_op_r.
-  - (* NonExpansive2 uPred_wand *)
-    intros n 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.
-  - (* NonExpansive uPred_persistently *)
-    intros n P1 P2 HP.
-    unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
-  - (* φ → P ⊢ ⌜φ⌝ *)
-    intros P φ ?. unseal; by split.
-  - (* (φ → True ⊢ P) → ⌜φ⌝ ⊢ P *)
-    intros φ P. unseal=> HP; split=> n x ??. by apply HP.
-  - (* (∀ x : A, ⌜φ x⌝) ⊢ ⌜∀ x : A, φ x⌝ *)
-    by unseal.
-  - (* P ∧ Q ⊢ P *)
-    intros P Q. unseal; by split=> n x ? [??].
-  - (* P ∧ Q ⊢ Q *)
-    intros P Q. unseal; by split=> n x ? [??].
-  - (* (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R *)
-    intros P Q R HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR].
-  - (* P ⊢ P ∨ Q *)
-    intros P Q. unseal; split=> n x ??; left; auto.
-  - (* Q ⊢ P ∨ Q *)
-    intros P Q. unseal; split=> n x ??; right; auto.
-  - (* (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R *)
-    intros P Q R HP HQ. unseal; split=> n x ? [?|?]. by apply HP. by apply HQ.
-  - (* (P ∧ Q ⊢ R) → P ⊢ Q → R. *)
-    intros P Q R. unseal => HQ; split=> n x ?? n' x' ????. apply HQ;
-      naive_solver eauto using uPred_mono, cmra_included_includedN.
-  - (* (P ⊢ Q → R) → P ∧ Q ⊢ R *)
-    intros P Q R. unseal=> HP; split=> n x ? [??]. apply HP with n x; auto.
-  - (* (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a *)
-    intros A P Ψ. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ.
-  - (* (∀ a, Ψ a) ⊢ Ψ a *)
-    intros A Ψ a. unseal; split=> n x ? HP; apply HP.
-  - (* Ψ a ⊢ ∃ a, Ψ a *)
-    intros A Ψ a. unseal; split=> n x ??; by exists a.
-  - (* (∀ a, Ψ a ⊢ Q) → (∃ a, Ψ a) ⊢ Q *)
-    intros A Ψ Q. unseal; intros HΨ; split=> n x ? [a ?]; by apply HΨ with a.
-  - (* (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q' *)
-    intros P P' Q Q' HQ HQ'; unseal.
-    split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; ofe_subst x;
-      eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
-  - (* P ⊢ emp ∗ P *)
-    intros P. rewrite /uPred_emp. unseal; split=> n x ?? /=.
-    exists (core x), x. by rewrite cmra_core_l.
-  - (* emp ∗ P ⊢ P *)
-    intros P. unseal; split; intros n x ? (x1&x2&?&_&?); ofe_subst;
-      eauto using uPred_mono, cmra_includedN_r.
-  - (* P ∗ Q ⊢ Q ∗ P *)
-    intros P Q. unseal; split; intros n x ? (x1&x2&?&?&?).
-    exists x2, x1; by rewrite (comm op).
-  - (* (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R) *)
-    intros P Q R. 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.
-  - (* (P ∗ Q ⊢ R) → P ⊢ Q -∗ R *)
-    intros P Q R. unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
-    exists x, x'; split_and?; auto.
-    eapply uPred_mono; eauto using cmra_validN_op_l.
-  - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
-    intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
-    eapply HPQR; eauto using cmra_validN_op_l.
-  - (* (P ⊢ Q) → <pers> P ⊢ <pers> Q *)
-    intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
-  - (* <pers> P ⊢ <pers> <pers> P *)
-    intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
-  - (* P ⊢ <pers> emp (ADMISSIBLE) *)
-    by unseal.
-  - (* (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a) *)
-    by unseal.
-  - (* <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a) *)
-    by unseal.
-  - (* <pers> P ∗ Q ⊢ <pers> P (ADMISSIBLE) *)
-    intros P Q. move: (uPred_persistently P)=> P'.
-    unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
-      eauto using uPred_mono, cmra_includedN_l.
-  - (* <pers> P ∧ Q ⊢ P ∗ Q *)
-    intros P Q. unseal; split=> n x ? [??]; simpl in *.
-    exists (core x), x; rewrite ?cmra_core_l; auto.
-Qed.
-
-Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
-  uPred_entails uPred_pure uPred_or uPred_impl
-  (@uPred_forall M) (@uPred_exist M) uPred_sep
-  uPred_persistently (@uPred_internal_eq M) uPred_later.
+  - by intros P; split=> x i.
+  - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
+Qed.
+Lemma entails_anti_sym : AntiSymm (⊣⊢) (⊢).
+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.
-  - (* Contractive sbi_later *)
-    unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
-    apply HPQ; eauto using cmra_validN_S.
-  - (* NonExpansive2 (@uPred_internal_eq M A) *)
-    intros A n 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.
-  - (* P ⊢ a ≡ a *)
-    intros A P a. unseal; by split=> n x ?? /=.
-  - (* a ≡ b ⊢ Ψ a → Ψ b *)
-    intros A a b Ψ Hnonexp.
-    unseal; split=> n x ? Hab n' x' ??? HΨ. eapply Hnonexp with n a; auto.
-  - (* (∀ x, f x ≡ g x) ⊢ f ≡ g *)
-    by unseal.
-  - (* `x ≡ `y ⊢ x ≡ y *)
-    by unseal.
-  - (* Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝ *)
-    intros A a b ?. unseal; split=> n x ?; by apply (discrete_iff n).
-  - (* Next x ≡ Next y ⊢ ▷ (x ≡ y) *)
-    by unseal.
-  - (* ▷ (x ≡ y) ⊢ Next x ≡ Next y *)
-    by unseal.
-  - (* (P ⊢ Q) → ▷ P ⊢ ▷ Q *)
-    intros P Q.
-    unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
-  - (* P ⊢ ▷ P *)
-    intros P. unseal; split=> -[|n] /= x ? HP; first done.
-    apply uPred_mono with (S n) x; eauto using cmra_validN_S.
-  - (* (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a *)
-    intros A Φ. unseal; by split=> -[|n] x.
-  - (* (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a) *)
-    intros A Φ. unseal; split=> -[|[|n]] x /=; eauto.
-  - (* ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q *)
-    intros P Q. unseal; split=> -[|n] x ? /=.
-    { 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].
-  - (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
-    intros P Q. unseal; split=> -[|n] x ? /=; [done|intros (x1&x2&Hx&?&?)].
-    exists x1, x2; eauto using dist_S.
-  - (* ▷ <pers> P ⊢ <pers> ▷ P *)
-    by unseal.
-  - (* <pers> ▷ P ⊢ ▷ <pers> P *)
-    by unseal.
-  - (* ▷ P ⊢ ▷ False ∨ (▷ False → P) *)
-    intros P. unseal; split=> -[|n] x ? /= HP; [by left|right].
-    intros [|n'] x' ????; [|done].
-    eauto using uPred_mono, cmra_included_includedN.
-Qed.
-
-Canonical Structure uPredI (M : ucmraT) : bi :=
-  {| bi_ofe_mixin := ofe_mixin_of (uPred M); bi_bi_mixin := uPred_bi_mixin M |}.
-Canonical Structure uPredSI (M : ucmraT) : sbi :=
-  {| sbi_ofe_mixin := ofe_mixin_of (uPred M);
-     sbi_bi_mixin := uPred_bi_mixin M; sbi_sbi_mixin := uPred_sbi_mixin M |}.
-
-Coercion uPred_valid {M} : uPred M → Prop := bi_emp_valid.
-
-(* Latest notation *)
-Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
+  - intros HPQ; split; split=> x i; apply HPQ.
+  - intros [??]. exact: entails_anti_sym.
+Qed.
+Lemma entails_lim (cP cQ : chain (uPredC M)) :
+  (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ.
+Proof.
+  intros Hlim; split=> n m ? HP.
+  eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl.
+Qed.
+
+(** Non-expansiveness and setoid morphisms *)
+Lemma pure_ne n : Proper (iff ==> dist n) (@uPred_pure M).
+Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|m] ?; try apply Hφ. Qed.
 
-Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly.
+Lemma and_ne : NonExpansive2 (@uPred_and M).
 Proof.
-  split.
-  - (* NonExpansive uPred_plainly *)
-    intros n P1 P2 HP.
-    unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
-  - (* (P ⊢ Q) → ■ P ⊢ ■ Q *)
-    intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN.
-  - (* ■ P ⊢ <pers> P *)
-    unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN.
-  - (* ■ P ⊢ ■ ■ P *)
-    unseal; split=> n x ?? //.
-  - (* (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a) *)
-    by unseal.
-  - (* (■ P → <pers> Q) ⊢ <pers> (■ P → Q) *)
-    unseal; split=> /= n x ? HPQ n' x' ????.
-    eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
-    apply (HPQ n' x); eauto using cmra_validN_le.
-  - (* (■ P → ■ Q) ⊢ ■ (■ P → Q) *)
-    unseal; split=> /= n x ? HPQ n' x' ????.
-    eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
-    apply (HPQ n' x); eauto using cmra_validN_le.
-  - (* P ⊢ ■ emp (ADMISSIBLE) *)
-    by unseal.
-  - (* ■ P ∗ Q ⊢ ■ P *)
-    intros P Q. move: (uPred_persistently P)=> P'.
-    unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
-      eauto using uPred_mono, cmra_includedN_l.
-  - (* ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *)
-    unseal; split=> n x ? /= HPQ. split=> n' x' ??.
-    move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
-    move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
-  - (* ▷ ■ P ⊢ ■ ▷ P *)
-    by unseal.
-  - (* ■ ▷ P ⊢ ▷ ■ P *)
-    by unseal.
+  intros n P P' HP Q Q' HQ; unseal; split=> x n' ??.
+  split; (intros [??]; split; [by apply HP|by apply HQ]).
 Qed.
-Instance uPred_plainlyC M : BiPlainly (uPredSI M) :=
-  {| bi_plainly_mixin := uPred_plainly_mixin M |}.
 
-Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
+Lemma or_ne : NonExpansive2 (@uPred_or M).
 Proof.
-  split.
-  - intros n 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.
-  - unseal. split=> n x ? HP k yf ?; exists x; split; first done.
-    apply uPred_mono with n x; eauto using cmra_validN_op_l.
-  - 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.
-  - unseal; split; naive_solver.
-  - 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. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
-Qed.
-Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
-
-Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredSI M).
-Proof.
-  rewrite /BiBUpdPlainly. unseal; split => n x Hnx /= Hng.
-  destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
-  eapply uPred_mono; eauto using ucmra_unit_leastN.
+  intros n P P' HP Q Q' HQ; split=> x n' ??.
+  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
 Qed.
 
-Module uPred.
-Include uPred_unseal.
-Section uPred.
-Context {M : ucmraT}.
-Implicit Types φ : Prop.
-Implicit Types P Q : uPred M.
-Implicit Types A : Type.
-Arguments uPred_holds {_} !_ _ _ /.
-Hint Immediate uPred_in_entails.
+Lemma impl_ne :
+  NonExpansive2 (@uPred_impl M).
+Proof.
+  intros n P P' HP Q Q' HQ; split=> x n' ??.
+  unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
+Qed.
+
+Lemma sep_ne : NonExpansive2 (@uPred_sep M).
+Proof.
+  intros n P P' HP Q Q' HQ; split=> n' x ??.
+  unseal; split; intros (x1&x2&?&?&?); ofe_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 ownM_ne : NonExpansive (@uPred_ownM M).
+Lemma wand_ne :
+  NonExpansive2 (@uPred_wand M).
+Proof.
+  intros n 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.
+
+Lemma internal_eq_ne (A : ofeT) :
+  NonExpansive2 (@uPred_internal_eq M A).
+Proof.
+  intros n 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.
+
+Lemma 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.
+
+Lemma 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.
+
+Lemma later_contractive : Contractive (@uPred_later M).
+Proof.
+  unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
+  apply HPQ; eauto using cmra_validN_S.
+Qed.
+
+Lemma plainly_ne : NonExpansive (@uPred_plainly M).
+Proof.
+  intros n P1 P2 HP.
+  unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
+Qed.
+
+Lemma persistently_ne : NonExpansive (@uPred_persistently M).
+Proof.
+  intros n P1 P2 HP.
+  unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
+Qed.
+
+Lemma ownM_ne : NonExpansive (@uPred_ownM M).
 Proof.
   intros n 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} :
+Lemma cmra_valid_ne {A : cmraT} :
   NonExpansive (@uPred_cmra_valid M A).
 Proof.
   intros n 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 _.
 
-(** BI instances *)
+Lemma bupd_ne : NonExpansive (@uPred_bupd M).
+Proof.
+  intros n 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 uPred_affine : BiAffine (uPredI M) | 0.
-Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
+(** Introduction and elimination rules *)
+Lemma pure_intro φ P : φ → P ⊢ ⌜φ⌝.
+Proof. by intros ?; unseal; split. Qed.
+Lemma pure_elim' φ P : (φ → True ⊢ P) → ⌜φ⌝ ⊢ P.
+Proof. unseal; intros HP; split=> n x ??. by apply HP. Qed.
+Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ x : A, ⌜φ x⌝) ⊢ ⌜∀ x : A, φ x⌝.
+Proof. by unseal. Qed.
 
-Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M).
-Proof. unfold BiPlainlyExist. 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, cmra_included_includedN.
+Qed.
+Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
+Proof. unseal; intros HP ; split=> n x ? [??]; apply HP with n x; auto. Qed.
 
-(** Limits *)
-Lemma entails_lim (cP cQ : chain (uPredC M)) :
-  (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ.
+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.
+
+(** BI connectives *)
+Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.
 Proof.
-  intros Hlim; split=> n m ? HP.
-  eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl.
+  intros HQ HQ'; unseal.
+  split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; ofe_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&?&_&?); ofe_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_mono with n x; 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 ? (?&?&?&?&?). ofe_subst.
+  eapply HPQR; eauto using cmra_validN_op_l.
+Qed.
+
+(** Persistently *)
+Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
+Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
+Lemma persistently_elim P : □ P ⊢ P.
+Proof.
+  unseal; split=> n x ? /=.
+  eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
+Qed.
+Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
+Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
+
+Lemma persistently_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
+Proof. by unseal. Qed.
+Lemma persistently_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
+Proof. by unseal. Qed.
+
+Lemma persistently_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.
+Qed.
+
+(** Plainly *)
+Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
+Proof. intros HP; unseal; split=> n x ? /=. apply HP, ucmra_unit_validN. Qed.
+Lemma plainly_elim_persistently P : ■ P ⊢ □ P.
+Proof. unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. Qed.
+Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
+Proof. unseal; split=> n x ?? //. Qed.
+
+Lemma plainly_forall_2 {A} (Ψ : A → uPred M) : (∀ a, ■ Ψ a) ⊢ (■ ∀ a, Ψ a).
+Proof. by unseal. Qed.
+Lemma plainly_exist_1 {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊢ (∃ a, ■ Ψ a).
+Proof. by unseal. Qed.
+
+Lemma prop_ext P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
+Proof.
+  unseal; split=> n x ? /= HPQ. split=> n' x' ??.
+    move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
+    move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
+Qed.
+
+(* The following two laws are very similar, and indeed they hold not just for â–¡
+   and ■, but for any modality defined as `M P n x := ∀ y, R x y → P n y`. *)
+Lemma persistently_impl_plainly P Q : (■ P → □ Q) ⊢ □ (■ P → Q).
+Proof.
+  unseal; split=> /= n x ? HPQ n' x' ????.
+  eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
+  apply (HPQ n' x); eauto using cmra_validN_le.
+Qed.
+
+Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
+Proof.
+  unseal; split=> /= n x ? HPQ n' x' ????.
+  eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
+  apply (HPQ n' x); eauto using cmra_validN_le.
+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 later_intro P : P ⊢ ▷ P.
+Proof.
+  unseal; split=> -[|n] /= x ? HP; first done.
+  apply uPred_mono with (S n) x; 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_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
+Proof.
+  unseal; split=> n x ?.
+  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].
+Qed.
+Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
+Proof.
+  unseal; split=> n x ?.
+  destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
+  exists x1, x2; eauto using dist_S.
+Qed.
+
+Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
+Proof.
+  unseal; split=> -[|n] x ? /= HP; [by left|right].
+  intros [|n'] x' ????; eauto using uPred_mono, cmra_included_includedN.
+Qed.
+
+Lemma later_persistently_1 P : ▷ □ P ⊢ □ ▷ P.
+Proof. by unseal. Qed.
+Lemma later_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
+Proof. by unseal. Qed.
+Lemma later_plainly_1 P : ▷ ■ P ⊢ ■ ▷ P.
+Proof. by unseal. Qed.
+Lemma later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P.
+Proof. by unseal. Qed.
+
+(** Internal equality *)
+Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ (a ≡ a).
+Proof. unseal; by split=> n x ??; simpl. Qed.
+Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) :
+  NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
+Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
+
+Lemma fun_ext `{B : A → ofeT} (g1 g2 : ofe_fun B) :
+  (∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
+Proof. by unseal. Qed.
+Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sigC P) :
+  proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
+Proof. by unseal. Qed.
+
+Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
+Proof. by unseal. Qed.
+Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
+Proof. by unseal. Qed.
+
+Lemma discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
+Proof.
+  unseal=> ?. split=> n x ?. by apply (discrete_iff n).
+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_mono with n x; 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. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
+Qed.
+Lemma bupd_plainly P : (|==> ■ P) ⊢ P.
+Proof.
+  unseal; split => n x Hnx /= Hng.
+  destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
+  eapply uPred_mono; eauto using ucmra_unit_leastN.
 Qed.
 
-(* Own *)
+(** Own *)
 Lemma ownM_op (a1 a2 : M) :
   uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
 Proof.
-  rewrite /bi_sep /=; unseal. split=> n x ?; split.
+  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 persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
+Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
 Proof.
-  rewrite /bi_persistently /=. unseal.
-  split=> n x Hx /=. by apply cmra_core_monoN.
+  split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
 Qed.
-Lemma ownM_unit : bi_emp_valid (uPred_ownM (ε:M)).
+Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
 Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
-Lemma later_ownM (a : M) : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
+Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
 Proof.
-  rewrite /bi_and /sbi_later /bi_exist /sbi_internal_eq /=; unseal.
-  split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
+  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 discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) :
-  ✓ a ⊣⊢ (⌜✓ a⌝ : uPred M).
-Proof. unseal. split=> n x _. by rewrite /= -cmra_discrete_valid_iff. 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.
+
+(** Valid *)
 Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
 Proof.
   unseal; split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
 Qed.
-Lemma cmra_valid_intro {A : cmraT} (a : A) :
-  ✓ a → bi_emp_valid (PROP:=uPredI M) (✓ a).
+Lemma cmra_valid_intro {A : cmraT} P (a : A) : ✓ a → P ⊢ (✓ a).
 Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
-Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ (False : uPred M).
-Proof.
-  intros Ha. unseal. split=> n x ??; apply Ha, cmra_validN_le with n; auto.
-Qed.
-Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■ (✓ a : uPred M).
+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 plainly_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 : uPred M).
+Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
 
-Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ (✓ x.1 ∧ ✓ x.2 : uPred M).
+Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
 Proof. by unseal. Qed.
 Lemma option_validI {A : cmraT} (mx : option A) :
   ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
 Proof. unseal. by destruct mx. Qed.
 
-Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) :
-  (✓ g : uPred M) ⊣⊢ ∀ i, ✓ g i.
-Proof. by uPred.unseal. Qed.
+Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
 
-Lemma bupd_ownM_updateP x (Φ : M → Prop) :
-  x ~~>: Φ → uPred_ownM x ==∗ ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
+Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Proof. by unseal. Qed.
+
+(** Consistency/soundness statement *)
+Lemma soundness φ n : (True ⊢ iter n uPred_later (⌜ φ ⌝)%I) → φ.
 Proof.
-  intros Hup. unseal. 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.
+  cut (iter n (@uPred_later M) (⌜ φ ⌝)%I n ε → φ).
+  { intros help H. eapply help, H; eauto using ucmra_unit_validN. by unseal. }
+  unseal. induction n as [|n IH]=> H; auto.
 Qed.
-End uPred.
-End uPred.
+
+End primitive.
+End uPred_primitive.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 277d29308e971469de904717ede6cfca051d6c69..4825fd55193aaaaa9186fb42c60b8f6864670aae 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -5,40 +5,26 @@ Set Default Proof Using "Type".
 Import interface.bi derived_laws_bi.bi.
 
 (* Notations *)
-Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL bi_sep (λ k x, P) l)
-  (at level 200, l at level 10, k, x at level 1, right associativity,
-   format "[∗  list]  k ↦ x  ∈  l ,  P") : bi_scope.
-Notation "'[∗' 'list]' x ∈ l , P" := (big_opL bi_sep (λ _ x, P) l)
-  (at level 200, l at level 10, x at level 1, right associativity,
-   format "[∗  list]  x  ∈  l ,  P") : bi_scope.
-
-Notation "'[∗]' Ps" :=
-  (big_opL bi_sep (λ _ x, x) Ps) (at level 20) : bi_scope.
-
-Notation "'[∧' 'list]' k ↦ x ∈ l , P" := (big_opL bi_and (λ k x, P) l)
-  (at level 200, l at level 10, k, x at level 1, right associativity,
-   format "[∧  list]  k ↦ x  ∈  l ,  P") : bi_scope.
-Notation "'[∧' 'list]' x ∈ l , P" := (big_opL bi_and (λ _ x, P) l)
-  (at level 200, l at level 10, x at level 1, right associativity,
-   format "[∧  list]  x  ∈  l ,  P") : bi_scope.
-
-Notation "'[∧]' Ps" :=
-  (big_opL bi_and (λ _ x, x) Ps) (at level 20) : bi_scope.
-
-Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m)
-  (at level 200, m at level 10, k, x at level 1, right associativity,
-   format "[∗  map]  k ↦ x  ∈  m ,  P") : bi_scope.
-Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m)
-  (at level 200, m at level 10, x at level 1, right associativity,
-   format "[∗  map]  x  ∈  m ,  P") : bi_scope.
-
-Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X)
-  (at level 200, X at level 10, x at level 1, right associativity,
-   format "[∗  set]  x  ∈  X ,  P") : bi_scope.
-
-Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
-  (at level 200, X at level 10, x at level 1, right associativity,
-   format "[∗  mset]  x  ∈  X ,  P") : bi_scope.
+Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
+  (big_opL bi_sep (λ k x, P) l) : bi_scope.
+Notation "'[∗' 'list]' x ∈ l , P" :=
+  (big_opL bi_sep (λ _ x, P) l) : bi_scope.
+
+Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope.
+
+Notation "'[∧' 'list]' k ↦ x ∈ l , P" :=
+  (big_opL bi_and (λ k x, P) l) : bi_scope.
+Notation "'[∧' 'list]' x ∈ l , P" :=
+  (big_opL bi_and (λ _ x, P) l) : bi_scope.
+
+Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps) : bi_scope.
+
+Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m) : bi_scope.
+Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m) : bi_scope.
+
+Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X) : bi_scope.
+
+Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X) : bi_scope.
 
 (** * Properties *)
 Section bi_big_op.
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 5857b235ef63233b2be00f2a7b77d64a8f883221..6cfef117eaa8da5d775c4c0dd27e382240238ff5 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -11,7 +11,7 @@ Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
   ((P -∗ Q) ∧ (Q -∗ P))%I.
 Arguments bi_wand_iff {_} _%I _%I : simpl never.
 Instance: Params (@bi_wand_iff) 1.
-Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
+Infix "∗-∗" := bi_wand_iff : bi_scope.
 
 Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
 Arguments Persistent {_} _%I : simpl never.
@@ -23,8 +23,7 @@ Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
 Arguments bi_affinely {_} _%I : simpl never.
 Instance: Params (@bi_affinely) 1.
 Typeclasses Opaque bi_affinely.
-Notation "'<affine>' P" := (bi_affinely P)
-  (at level 20, right associativity) : bi_scope.
+Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
 
 Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
 Arguments Affine {_} _%I : simpl never.
@@ -43,8 +42,7 @@ Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
 Arguments bi_absorbingly {_} _%I : simpl never.
 Instance: Params (@bi_absorbingly) 1.
 Typeclasses Opaque bi_absorbingly.
-Notation "'<absorb>' P" := (bi_absorbingly P)
-  (at level 20, right associativity) : bi_scope.
+Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
 
 Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
 Arguments Absorbing {_} _%I : simpl never.
@@ -56,35 +54,28 @@ Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
 Arguments bi_persistently_if {_} !_ _%I /.
 Instance: Params (@bi_persistently_if) 2.
 Typeclasses Opaque bi_persistently_if.
-Notation "'<pers>?' p P" := (bi_persistently_if p P)
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "'<pers>?' p  P") : bi_scope.
+Notation "'<pers>?' p P" := (bi_persistently_if p P) : bi_scope.
 
 Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <affine> P else P)%I.
 Arguments bi_affinely_if {_} !_ _%I /.
 Instance: Params (@bi_affinely_if) 2.
 Typeclasses Opaque bi_affinely_if.
-Notation "'<affine>?' p P" := (bi_affinely_if p P)
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "'<affine>?' p  P") : bi_scope.
+Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
 
 Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
   (<affine> <pers> P)%I.
 Arguments bi_intuitionistically {_} _%I : simpl never.
 Instance: Params (@bi_intuitionistically) 1.
 Typeclasses Opaque bi_intuitionistically.
-Notation "â–¡ P" := (bi_intuitionistically P)%I
-  (at level 20, right associativity) : bi_scope.
+Notation "â–¡ P" := (bi_intuitionistically P) : bi_scope.
 
 Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then â–¡ P else P)%I.
 Arguments bi_intuitionistically_if {_} !_ _%I /.
 Instance: Params (@bi_intuitionistically_if) 2.
 Typeclasses Opaque bi_intuitionistically_if.
-Notation "'â–¡?' p P" := (bi_intuitionistically_if p P)
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "'â–¡?' p  P") : bi_scope.
+Notation "'â–¡?' p P" := (bi_intuitionistically_if p P) : bi_scope.
 
 Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP :=
   match As return himpl As PROP → PROP with
@@ -101,14 +92,12 @@ Definition sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
   Nat.iter n sbi_later P.
 Arguments sbi_laterN {_} !_%nat_scope _%I.
 Instance: Params (@sbi_laterN) 2.
-Notation "â–·^ n P" := (sbi_laterN n P)
-  (at level 20, n at level 9, P at level 20, format "â–·^ n  P") : bi_scope.
-Notation "â–·? p P" := (sbi_laterN (Nat.b2n p) P)
-  (at level 20, p at level 9, P at level 20, format "â–·? p  P") : bi_scope.
+Notation "â–·^ n P" := (sbi_laterN n P) : bi_scope.
+Notation "â–·? p P" := (sbi_laterN (Nat.b2n p) P) : bi_scope.
 
 Definition sbi_except_0 {PROP : sbi} (P : PROP) : PROP := (▷ False ∨ P)%I.
 Arguments sbi_except_0 {_} _%I : simpl never.
-Notation "â—‡ P" := (sbi_except_0 P) (at level 20, right associativity) : bi_scope.
+Notation "â—‡ P" := (sbi_except_0 P) : bi_scope.
 Instance: Params (@sbi_except_0) 1.
 Typeclasses Opaque sbi_except_0.
 
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 123e83c1a2c44940e1f65b6006af634ce875bbaf..2abcd87d22c8d2ab010cc29ff00c653d213fc254 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -531,7 +531,7 @@ Lemma pure_wand_forall φ P `{!Absorbing P} : (⌜φ⌝ -∗ P) ⊣⊢ (∀ _ :
 Proof.
   apply (anti_symm _).
   - apply forall_intro=> Hφ.
-    by rewrite -(left_id emp%I _ (_ -∗ _)%I) (pure_intro emp%I φ) // wand_elim_r.
+    by rewrite -(left_id emp%I _ (_ -∗ _)%I) (pure_intro φ emp%I) // wand_elim_r.
   - apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ.
     apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing.
 Qed.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 71ebd6a09ad190859391a68457fefba11b0f0018..fb475c79d14e0cff196709c17b32e39bb2af41c0 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,19 +1,7 @@
 From iris.algebra Require Export ofe.
+From iris.bi Require Export notation.
 Set Primitive Projections.
 
-Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "('⊢@{' PROP } )" (at level 99).
-Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
-Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
-Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
-Reserved Notation "'emp'".
-Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
-Reserved Notation "P ∗ Q" (at level 80, right associativity).
-Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "'<pers>' P" (at level 20, right associativity).
-Reserved Notation "â–· P" (at level 20, right associativity).
-
 Section bi_mixin.
   Context {PROP : Type} `{Dist PROP, Equiv PROP}.
   Context (bi_entails : PROP → PROP → Prop).
@@ -77,7 +65,7 @@ Section bi_mixin.
     bi_mixin_persistently_ne : NonExpansive bi_persistently;
 
     (** Higher-order logic *)
-    bi_mixin_pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ ⌝;
+    bi_mixin_pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝;
     bi_mixin_pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P;
     (* This is actually derivable if we assume excluded middle in Coq,
        via [(∀ a, φ a) ∨ (∃ a, ¬φ a)]. *)
@@ -195,7 +183,6 @@ Instance: Params (@bi_sep) 1.
 Instance: Params (@bi_wand) 1.
 Instance: Params (@bi_persistently) 1.
 
-Delimit Scope bi_scope with I.
 Arguments bi_car : simpl never.
 Arguments bi_dist : simpl never.
 Arguments bi_equiv : simpl never.
@@ -347,7 +334,7 @@ Global Instance persistently_ne : NonExpansive (@bi_persistently PROP).
 Proof. eapply bi_mixin_persistently_ne, bi_bi_mixin. Qed.
 
 (* Higher-order logic *)
-Lemma pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ ⌝.
+Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
 Proof. eapply bi_mixin_pure_intro, bi_bi_mixin. Qed.
 Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
 Proof. eapply bi_mixin_pure_elim', bi_bi_mixin. Qed.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index e3191ffbf81bdcef0a705120c8b3180a7ab2aff9..0a01f4e0d7a5b014ab134772c2630efc1c2aef01 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -214,8 +214,8 @@ End Bi.
 
 Arguments monPred_objectively {_ _} _%I.
 Arguments monPred_subjectively {_ _} _%I.
-Notation "'<obj>' P" := (monPred_objectively P) (at level 20, right associativity) : bi_scope.
-Notation "'<subj>' P" := (monPred_subjectively P) (at level 20, right associativity) : bi_scope.
+Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
+Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
 
 Section Sbi.
 Context {I : biIndex} {PROP : sbi}.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
new file mode 100644
index 0000000000000000000000000000000000000000..5322e6d71455e81d56797cb4d7cc4fb529a66e86
--- /dev/null
+++ b/theories/bi/notation.v
@@ -0,0 +1,117 @@
+(** Just reserve the notation. *)
+
+(** Turnstiles *)
+Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "('⊢@{' PROP } )" (at level 99).
+Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
+Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
+Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
+
+(** BI connectives *)
+Reserved Notation "'emp'".
+Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
+Reserved Notation "P ∗ Q" (at level 80, right associativity).
+Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
+
+Reserved Notation "⎡ P ⎤".
+
+(** Modalities *)
+Reserved Notation "'<pers>' P" (at level 20, right associativity).
+Reserved Notation "'<pers>?' p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<pers>?' p  P").
+
+Reserved Notation "â–· P" (at level 20, right associativity).
+Reserved Notation "â–·? p P" (at level 20, p at level 9, P at level 20,
+   format "â–·? p  P").
+Reserved Notation "â–·^ n P" (at level 20, n at level 9, P at level 20,
+   format "â–·^ n  P").
+
+Reserved Infix "∗-∗" (at level 95, no associativity).
+
+Reserved Notation "'<affine>' P" (at level 20, right associativity).
+Reserved Notation "'<affine>?' p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<affine>?' p  P").
+
+Reserved Notation "'<absorb>' P" (at level 20, right associativity).
+
+Reserved Notation "â–¡ P" (at level 20, right associativity).
+Reserved Notation "'â–¡?' p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "'â–¡?' p  P").
+
+Reserved Notation "â—‡ P" (at level 20, right associativity).
+
+Reserved Notation "â–  P" (at level 20, right associativity).
+Reserved Notation "â– ? p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "â– ? p  P").
+
+Reserved Notation "'<obj>' P" (at level 20, right associativity).
+Reserved Notation "'<subj>' P" (at level 20, right associativity).
+
+(** Update modalities *)
+Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
+Reserved Notation "P ==∗ Q" (at level 99, Q at level 200, format "P  ==∗  Q").
+
+Reserved Notation "|={ E1 , E2 }=> Q"
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 }=>  Q").
+Reserved Notation "P ={ E1 , E2 }=∗ Q"
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }=∗  Q").
+
+Reserved Notation "|={ E }=> Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "|={ E }=>  Q").
+Reserved Notation "P ={ E }=∗ Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=∗  Q").
+
+Reserved Notation "|={ E1 , E2 }â–·=> Q"
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 }â–·=>  Q").
+Reserved Notation "P ={ E1 , E2 }▷=∗ Q"
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }▷=∗  Q").
+Reserved Notation "|={ E }â–·=> Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "|={ E }â–·=>  Q").
+Reserved Notation "P ={ E }▷=∗ Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }▷=∗  Q").
+
+(** Big Ops *)
+Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
+  (at level 200, l at level 10, k, x at level 1, right associativity,
+   format "[∗  list]  k ↦ x  ∈  l ,  P").
+Reserved Notation "'[∗' 'list]' x ∈ l , P"
+  (at level 200, l at level 10, x at level 1, right associativity,
+   format "[∗  list]  x  ∈  l ,  P").
+
+Reserved Notation "'[∗]' Ps" (at level 20).
+
+Reserved Notation "'[∧' 'list]' k ↦ x ∈ l , P"
+  (at level 200, l at level 10, k, x at level 1, right associativity,
+   format "[∧  list]  k ↦ x  ∈  l ,  P").
+Reserved Notation "'[∧' 'list]' x ∈ l , P"
+  (at level 200, l at level 10, x at level 1, right associativity,
+   format "[∧  list]  x  ∈  l ,  P").
+
+Reserved Notation "'[∧]' Ps" (at level 20).
+
+Reserved Notation "'[∗' 'map]' k ↦ x ∈ m , P"
+  (at level 200, m at level 10, k, x at level 1, right associativity,
+   format "[∗  map]  k ↦ x  ∈  m ,  P").
+Reserved Notation "'[∗' 'map]' x ∈ m , P"
+  (at level 200, m at level 10, x at level 1, right associativity,
+   format "[∗  map]  x  ∈  m ,  P").
+
+Reserved Notation "'[∗' 'set]' x ∈ X , P"
+  (at level 200, X at level 10, x at level 1, right associativity,
+   format "[∗  set]  x  ∈  X ,  P").
+
+Reserved Notation "'[∗' 'mset]' x ∈ X , P"
+  (at level 200, X at level 10, x at level 1, right associativity,
+   format "[∗  mset]  x  ∈  X ,  P").
+
+(** Define the scope *)
+Delimit Scope bi_scope with I.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 7f15fee347ba612055377ed20a23602d1074e986..012d646ea19d91bd7f199e6bb0353a3a13016518 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -5,8 +5,7 @@ Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 Class Plainly (A : Type) := plainly : A → A.
 Hint Mode Plainly ! : typeclass_instances.
 Instance: Params (@plainly) 2.
-Notation "â–  P" := (plainly P)%I
-  (at level 20, right associativity) : bi_scope.
+Notation "â–  P" := (plainly P) : bi_scope.
 
 (* Mixins allow us to create instances easily without having to use Program *)
 Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
@@ -96,9 +95,7 @@ Arguments plainly_if {_ _} !_ _%I /.
 Instance: Params (@plainly_if) 2.
 Typeclasses Opaque plainly_if.
 
-Notation "â– ? p P" := (plainly_if p P)%I
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "â– ? p  P") : bi_scope.
+Notation "â– ? p P" := (plainly_if p P) : bi_scope.
 
 (* Derived laws *)
 Section plainly_derived.
@@ -167,7 +164,7 @@ Proof.
   - by rewrite plainly_elim_persistently persistently_pure.
   - apply pure_elim'=> Hφ.
     trans (∀ x : False, ■ True : PROP)%I; [by apply forall_intro|].
-    rewrite plainly_forall_2. by rewrite -(pure_intro _ φ).
+    rewrite plainly_forall_2. by rewrite -(pure_intro φ).
 Qed.
 Lemma plainly_forall {A} (Ψ : A → PROP) : ■ (∀ a, Ψ a) ⊣⊢ ∀ a, ■ (Ψ a).
 Proof.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 43462afefd41d4f74b2c4dececac823d3e62c42b..a36798e9d63bcb93ecd6a93b3bb03cdc67168d53 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -7,48 +7,27 @@ Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
 Instance : Params (@bupd) 2.
 Hint Mode BUpd ! : typeclass_instances.
 
-Notation "|==> Q" := (bupd Q)
-  (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
-Notation "P ==∗ Q" := (P ⊢ |==> Q)
-  (at level 99, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ==∗ Q" := (P -∗ |==> Q)%I
-  (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.
+Notation "|==> Q" := (bupd Q) : bi_scope.
+Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope.
+Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
 
 Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
 Instance: Params (@fupd) 4.
 Hint Mode FUpd ! : typeclass_instances.
 
-Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }=>  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
-  (at level 99, E1,E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
-  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
-
-Notation "|={ E }=> Q" := (fupd E E Q)
-  (at level 99, E at level 50, Q at level 200,
-   format "|={ E }=>  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }=∗  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
-  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
+Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q) : stdpp_scope.
+
+Notation "|={ E }=> Q" := (fupd E E Q) : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q) : stdpp_scope.
 
 (** Fancy updates that take a step. *)
-Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }â–·=>  Q") : bi_scope.
-Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2 }▷=> Q)%I
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }▷=∗  Q") : bi_scope.
-Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "|={ E }â–·=>  Q") : bi_scope.
-Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }▷=∗  Q") : bi_scope.
+Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I : bi_scope.
+Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2 }▷=> Q)%I : bi_scope.
+Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I : bi_scope.
+Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I : bi_scope.
 
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index e48ae659604aa0d99e2aafac2c6d6dca5fe7994b..8479acf4007c5290471dd48dcb2038ba29b26ba1 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -1,6 +1,5 @@
 From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Import gmap auth agree gset coPset.
-From iris.base_logic Require Import soundness.
 From iris.base_logic.lib Require Import wsat.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 84954fee1e19ef624e1dd81222b2342ca3cf467f..ebb8c9b0c663541bd460479580ebf7258ea00eb6 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -1,7 +1,6 @@
 From iris.program_logic Require Export total_weakestpre adequacy.
 From iris.algebra Require Import gmap auth agree gset coPset list.
 From iris.bi Require Import big_op fixpoint.
-From iris.base_logic Require Import soundness.
 From iris.base_logic.lib Require Import wsat.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 37c079bcb3e69f319c83781356f158a29a534c38..0d00294122fce3ab6e7f1f0e3941ff0cba334fe5 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -354,7 +354,7 @@ Global Instance into_forall_wand_pure φ P Q :
 Proof.
   rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]] /=.
   apply forall_intro=>? /=.
-  by rewrite -(pure_intro True%I) // /bi_affinely right_id emp_wand.
+  by rewrite -(pure_intro _ True%I) // /bi_affinely right_id emp_wand.
 Qed.
 
 Global Instance into_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :