diff --git a/_CoqProject b/_CoqProject
index bf3984a5409510fc27dd0e08cfaf29847cf1f902..d82e63a7aee4b0a50ebf7a64010d502523aa2a52 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -72,11 +72,14 @@ iris/bi/derived_laws.v
 iris/bi/derived_laws_later.v
 iris/bi/plainly.v
 iris/bi/internal_eq.v
+iris/bi/cmra_valid.v
 iris/bi/big_op.v
 iris/bi/updates.v
 iris/bi/ascii.v
 iris/bi/bi.v
 iris/bi/sbi.v
+iris/bi/sbi_unfold.v
+iris/bi/algebra.v
 iris/bi/monpred.v
 iris/bi/embedding.v
 iris/bi/weakestpre.v
@@ -94,7 +97,6 @@ iris/base_logic/bi.v
 iris/base_logic/derived.v
 iris/base_logic/proofmode.v
 iris/base_logic/base_logic.v
-iris/base_logic/algebra.v
 iris/base_logic/bupd_alt.v
 iris/base_logic/lib/iprop.v
 iris/base_logic/lib/own.v
@@ -148,6 +150,7 @@ iris/proofmode/class_instances_updates.v
 iris/proofmode/class_instances_embedding.v
 iris/proofmode/class_instances_plainly.v
 iris/proofmode/class_instances_internal_eq.v
+iris/proofmode/class_instances_cmra_valid.v
 iris/proofmode/class_instances_frame.v
 iris/proofmode/class_instances_make.v
 iris/proofmode/monpred.v
@@ -188,7 +191,7 @@ iris_heap_lang/lib/array.v
 iris_heap_lang/lib/logatom_lock.v
 
 iris_unstable/algebra/list.v
-iris_unstable/base_logic/algebra.v
+iris_unstable/bi/algebra.v
 iris_unstable/base_logic/mono_list.v
 iris_unstable/heap_lang/interpreter.v
 
diff --git a/iris/base_logic/base_logic.v b/iris/base_logic/base_logic.v
index 66c98d955cdb804e0dcb8f4057c4f814a1c6af47..498686f4c586cd0cad99971df37f8df750a4d2f8 100644
--- a/iris/base_logic/base_logic.v
+++ b/iris/base_logic/base_logic.v
@@ -1,5 +1,5 @@
 From iris.bi Require Export bi.
-From iris.base_logic Require Export derived proofmode algebra.
+From iris.base_logic Require Export derived proofmode.
 From iris.prelude Require Import options.
 
 (* The trick of having multiple [uPred] modules, which are all exported in
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 213c1ae65539fec45f2a0cbf5a48fcdfa24b7ca6..2f574ee036152a5aaa2160775121e3bc1d3b3bb8 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -1,5 +1,5 @@
 From iris.bi Require Export derived_connectives extensions.
-From iris.bi Require Export sbi updates internal_eq plainly.
+From iris.bi Require Export sbi updates internal_eq plainly cmra_valid.
 From iris.si_logic Require Export bi.
 From iris.bi Require Import derived_laws derived_laws_later.
 From iris.base_logic Require Export upred.
@@ -14,6 +14,7 @@ Definition uPred_emp {M} : uPred M := uPred_pure True.
 
 Local Existing Instance entails_po.
 
+(* We need this property multiple times, so let's prove it once. *)
 Local Lemma True_intro M P : uPred_entails (M:=M) P (uPred_pure True).
 Proof.
   trans (uPred_si_pure (∀ x : False, True) : uPred M).
@@ -134,7 +135,6 @@ Proof.
   - exact: si_pure_later.
   - (* Absorbing (<si_pure> Pi) (ADMISSIBLE) *)
     intros Pi. apply True_sep_2.
-  - exact: @si_emp_valid_exist_1.
   - exact: @si_emp_valid_later_1.
   - (* <si_emp_valid> P -∗ <si_emp_valid> <affine> P (ADMISSIBLE) *)
     intros P. apply si_emp_valid_mono, and_intro; [|done].
@@ -142,50 +142,11 @@ Proof.
   - exact: si_emp_valid_si_pure.
   - exact: si_pure_si_emp_valid.
 Qed.
+Lemma uPred_sbi_prop_ext_mixin M : SbiPropExtMixin (uPredI M) uPred_si_emp_valid.
+Proof. split. apply prop_ext_2. Qed.
 Global Instance uPred_sbi M : Sbi (uPredI M) :=
-  {| sbi_sbi_mixin := uPred_sbi_mixin M |}.
-
-Lemma uPred_internal_eq_mixin M :
-  BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
-Proof.
-  split.
-  - 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.
-Qed.
-Global Instance uPred_internal_eq M : BiInternalEq (uPredI M) :=
-  {| bi_internal_eq_mixin := uPred_internal_eq_mixin M |}.
-
-Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredI M) uPred_plainly.
-Proof.
-  split.
-  - exact: plainly_ne.
-  - exact: plainly_mono.
-  - exact: plainly_elim_persistently.
-  - exact: plainly_idemp_2.
-  - exact: @plainly_forall_2.
-  - 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: bi.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: bi.pure_intro.
-  - exact: later_plainly_1.
-  - exact: later_plainly_2.
-Qed.
-Global Instance uPred_plainly M : BiPlainly (uPredI M) :=
-  {| bi_plainly_mixin := uPred_plainly_mixin M |}.
+  {| sbi_sbi_mixin := uPred_sbi_mixin M;
+     sbi_sbi_prop_ext_mixin := uPred_sbi_prop_ext_mixin M |}.
 
 Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
 Proof.
@@ -219,22 +180,15 @@ Qed.
 Global Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
 Proof. exact: @later_contractive. Qed.
 
-Global Instance uPred_persistently_impl_plainly M :
-  BiPersistentlyImplPlainly (uPredI M).
-Proof. exact: persistently_impl_plainly. Qed.
+Global Instance uPred_sbi_emp_valid_exist {M} : SbiEmpValidExist (uPredI M).
+Proof. exact: @si_emp_valid_exist_1. Qed.
 
 Global Instance uPred_persistently_impl_si_pure M :
   BiPersistentlyImplSiPure (uPredI M).
 Proof. exact: persistently_impl_si_pure. Qed.
 
-Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredI M).
-Proof. exact: @plainly_exist_1. Qed.
-
-Global Instance uPred_prop_ext M : BiPropExt (uPredI M).
-Proof. exact: prop_ext_2. Qed.
-
-Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredI M).
-Proof. exact: bupd_plainly. Qed.
+Global Instance uPred_bi_bupd_sbi M : BiBUpdSbi (uPredI M).
+Proof. exact: bupd_si_pure. Qed.
 
 (** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
 
@@ -251,16 +205,16 @@ Section restate.
   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 : cmra} : NonExpansive (@uPred_cmra_valid M A) :=
-    uPred_primitive.cmra_valid_ne.
 
   (** Re-exporting primitive lemmas that are not in any interface *)
+  Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
+  Proof. exact: uPred_primitive.ownM_valid. Qed.
   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 ε).
+  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.
@@ -268,43 +222,6 @@ Section restate.
     x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
   Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
 
-  (** This is really just a special case of an entailment
-  between two [siProp], but we do not have the infrastructure
-  to express the more general case. This temporary proof rule will
-  be replaced by the proper one eventually. *)
-  Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
-    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
-  Proof. exact: uPred_primitive.internal_eq_entails. Qed.
-
-  Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
-  Proof. exact: uPred_primitive.ownM_valid. Qed.
-  Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
-  Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
-  Lemma cmra_valid_elim {A : cmra} (a : A) : ✓ a ⊢ ⌜ ✓{0} a ⌝.
-  Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
-  Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
-  Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
-  Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
-  Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
-
-  (** This is really just a special case of an entailment
-  between two [siProp], but we do not have the infrastructure
-  to express the more general case. This temporary proof rule will
-  be replaced by the proper one eventually. *)
-  Lemma valid_entails {A B : cmra} (a : A) (b : B) :
-    (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
-  Proof. exact: uPred_primitive.valid_entails. Qed.
-
-  (** Consistency/soundness statement *)
-  Lemma pure_soundness φ : (⊢@{uPredI M} ⌜ φ ⌝) → φ.
-  Proof. apply pure_soundness. Qed.
-
-  Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
-  Proof. apply internal_eq_soundness. Qed.
-
-  Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
-  Proof. apply later_soundness. Qed.
-
   (** We restate the unsealing lemmas for the BI layer. The sealing lemmas
   are partially applied so that they also rewrite under binders. *)
   Local Lemma uPred_emp_unseal :
@@ -328,15 +245,10 @@ Section restate.
   Proof. by rewrite -upred.uPred_forall_unseal. Qed.
   Local Lemma uPred_exist_unseal : @bi_exist _ = @upred.uPred_exist_def M.
   Proof. by rewrite -upred.uPred_exist_unseal. Qed.
-  Local Lemma uPred_internal_eq_unseal :
-    @internal_eq _ _ = @upred.uPred_internal_eq_def M.
-  Proof. by rewrite -upred.uPred_internal_eq_unseal. Qed.
   Local Lemma uPred_sep_unseal : bi_sep = @upred.uPred_sep_def M.
   Proof. by rewrite -upred.uPred_sep_unseal. Qed.
   Local Lemma uPred_wand_unseal : bi_wand = @upred.uPred_wand_def M.
   Proof. by rewrite -upred.uPred_wand_unseal. Qed.
-  Local Lemma uPred_plainly_unseal : plainly = @upred.uPred_plainly_def M.
-  Proof. by rewrite -upred.uPred_plainly_unseal. Qed.
   Local Lemma uPred_persistently_unseal :
     bi_persistently = @upred.uPred_persistently_def M.
   Proof. by rewrite -upred.uPred_persistently_unseal. Qed.
@@ -350,9 +262,9 @@ Section restate.
     uPred_si_pure_unseal, uPred_si_emp_valid_unseal,
     uPred_and_unseal, uPred_or_unseal,
     uPred_impl_unseal, uPred_forall_unseal, uPred_exist_unseal,
-    uPred_internal_eq_unseal, uPred_sep_unseal, uPred_wand_unseal,
-    uPred_plainly_unseal, uPred_persistently_unseal, uPred_later_unseal,
-    upred.uPred_ownM_unseal, upred.uPred_cmra_valid_unseal, @uPred_bupd_unseal).
+    uPred_sep_unseal, uPred_wand_unseal,
+    uPred_persistently_unseal, uPred_later_unseal,
+    upred.uPred_ownM_unseal, @uPred_bupd_unseal).
 End restate.
 
 (** A tactic for rewriting with the above lemmas. Unfolds [uPred] goals that use
diff --git a/iris/base_logic/bupd_alt.v b/iris/base_logic/bupd_alt.v
index c466e2f5d528fcff027a3e6780f91b5e8ac2409a..1ad8f78b80bb6b8a3f32df4190509752b931988c 100644
--- a/iris/base_logic/bupd_alt.v
+++ b/iris/base_logic/bupd_alt.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type*".
 
 (** This file contains an alternative version of basic updates, that is
 expression in terms of just the plain modality [â– ]. *)
-Definition bupd_alt {PROP : bi} `{!BiPlainly PROP} (P : PROP) : PROP :=
+Definition bupd_alt {PROP : bi} `{!Sbi PROP} (P : PROP) : PROP :=
   ∀ R, (P -∗ ■ R) -∗ ■ R.
 
 (** This definition is stated for any BI with a plain modality. The above
@@ -28,7 +28,7 @@ The first two points are shown for any BI with a plain modality. *)
 Local Coercion uPred_holds : uPred >-> Funclass.
 
 Section bupd_alt.
-  Context {PROP : bi} `{!BiPlainly PROP}.
+  Context {PROP : bi} `{!Sbi PROP}.
   Implicit Types P Q R : PROP.
   Notation bupd_alt := (@bupd_alt PROP _).
 
@@ -57,7 +57,8 @@ Section bupd_alt.
 
   (** Any modality conforming with [BiBUpdPlainly] entails the alternative
   definition *)
-  Lemma bupd_bupd_alt `{!BiBUpd PROP, !BiBUpdPlainly PROP} P : (|==> P) ⊢ bupd_alt P.
+  Lemma bupd_bupd_alt `{!BiBUpd PROP, !BiBUpdSbi PROP, !BiAffine PROP} P :
+    (|==> P) ⊢ bupd_alt P.
   Proof. iIntros "HP" (R) "H". by iMod ("H" with "HP") as "?". Qed.
 
   (** We get the usual rule for frame preserving updates if we have an [own]
@@ -79,7 +80,7 @@ End bupd_alt.
 (** The alternative definition entails the ordinary basic update *)
 Lemma bupd_alt_bupd {M} (P : uPred M) : bupd_alt P ⊢ |==> P.
 Proof.
-  rewrite /bupd_alt. uPred.unseal; split=> n x Hx H k y ? Hxy.
+  rewrite /bupd_alt /plainly. uPred.unseal; split=> n x Hx H k y ? Hxy.
   unshelve refine (H {| uPred_holds k _ :=
     ∃ x' : M, ✓{k} (x' ⋅ y) ∧ P k x' |} k y _ _ _).
   - intros n1 n2 x1 x2 (z&?&?) _ ?.
@@ -101,7 +102,8 @@ Lemma ownM_updateP {M : ucmra} x (Φ : M → Prop) (R : uPred M) :
   x ~~>: Φ →
   uPred_ownM x ∗ (∀ y, ⌜Φ y⌝ -∗ uPred_ownM y -∗ ■ R) ⊢ ■ R.
 Proof.
-  uPred.unseal=> Hup; split; intros n z Hv (?&z2&?&[z1 ?]&HR); ofe_subst.
+  intros Hup. rewrite /plainly. uPred.unseal.
+  split. intros n z Hv (?&z2&?&[z1 ?]&HR); ofe_subst.
   destruct (Hup n (Some (z1 â‹… z2))) as (y&?&?); simpl in *.
   { by rewrite assoc. }
   refine (HR y n z1 _ _ _ n y _ _ _); auto.
diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v
index 335bd5a534be02e894f32323f1c90b7e1e718078..a9d0c4117eadb2bf0194acb2163f3206f3da8177 100644
--- a/iris/base_logic/derived.v
+++ b/iris/base_logic/derived.v
@@ -20,12 +20,8 @@ Section derived.
 
   (** Propers *)
   Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
-  Global Instance cmra_valid_proper {A : cmra} :
-    Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
 
   (** Own and valid derived *)
-  Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢@{uPredI M} <pers> (✓ a).
-  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.
   Proof.
     rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
@@ -33,25 +29,11 @@ Section derived.
     by rewrite {1}persistently_ownM_core core_id_core.
   Qed.
   Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
-  Proof. intros. rewrite ownM_valid cmra_valid_elim. by apply pure_elim'. Qed.
+  Proof. intros. rewrite ownM_valid bi_cmra_valid_elim. by apply pure_elim'. Qed.
   Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
   Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
   Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
   Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
-  Lemma plainly_cmra_valid {A : cmra} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
-  Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
-  Lemma intuitionistically_cmra_valid {A : cmra} (a : A) : □ ✓ a ⊣⊢ ✓ a.
-  Proof.
-    rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
-      first by rewrite persistently_elim.
-    apply:persistently_cmra_valid_1.
-  Qed.
-  Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
-  Proof.
-    apply (anti_symm _).
-    - rewrite cmra_valid_elim. by apply pure_mono, cmra_discrete_valid.
-    - apply pure_elim'=> ?. by apply cmra_valid_intro.
-  Qed.
 
   Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y.
   Proof.
@@ -60,27 +42,16 @@ Section derived.
   Qed.
 
   (** Timeless instances *)
-  Global Instance valid_timeless {A : cmra} `{!CmraDiscrete A} (a : A) :
-    Timeless (✓ a : uPred M)%I.
-  Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
   Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
   Proof.
     intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
     rewrite (timeless (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
     apply except_0_mono. rewrite internal_eq_sym.
     apply (internal_eq_rewrite' b a (uPred_ownM) _);
-      auto using and_elim_l, and_elim_r.
+      [solve_proper|auto using and_elim_l, and_elim_r..].
   Qed.
 
-  (** Plainness *)
-  Global Instance cmra_valid_plain {A : cmra} (a : A) :
-    Plain (✓ a : uPred M)%I.
-  Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
-
   (** Persistence *)
-  Global Instance cmra_valid_persistent {A : cmra} (a : A) :
-    Persistent (✓ a : uPred M)%I.
-  Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
   Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
   Proof.
     intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
@@ -91,36 +62,6 @@ Section derived.
     MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
   Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
 
-  (** Derive [NonExpansive]/[Contractive] from an internal statement *)
-  Lemma ne_internal_eq {A B : ofe} (f : A → B) :
-    NonExpansive f ↔ ∀ x1 x2, x1 ≡ x2 ⊢ f x1 ≡ f x2.
-  Proof.
-    split; [apply f_equivI|].
-    intros Hf n x1 x2. by eapply internal_eq_entails.
-  Qed.
-
-  Lemma ne_2_internal_eq {A B C : ofe} (f : A → B → C) :
-    NonExpansive2 f ↔ ∀ x1 x2 y1 y2, x1 ≡ x2 ∧ y1 ≡ y2 ⊢ f x1 y1 ≡ f x2 y2.
-  Proof.
-    split.
-    - intros Hf x1 x2 y1 y2.
-      change ((x1,y1).1 ≡ (x2,y2).1 ∧ (x1,y1).2 ≡ (x2,y2).2
-        ⊢ uncurry f (x1,y1) ≡ uncurry f (x2,y2)).
-      rewrite -prod_equivI. apply ne_internal_eq. solve_proper.
-    - intros Hf n x1 x2 Hx y1 y2 Hy.
-      change (uncurry f (x1,y1) ≡{n}≡ uncurry f (x2,y2)).
-      apply ne_internal_eq; [|done].
-      intros [??] [??]. rewrite prod_equivI. apply Hf.
-  Qed.
-
-  Lemma contractive_internal_eq {A B : ofe} (f : A → B) :
-    Contractive f ↔ ∀ x1 x2, ▷ (x1 ≡ x2) ⊢ f x1 ≡ f x2.
-  Proof.
-    split; [apply f_equivI_contractive|].
-    intros Hf n x1 x2 Hx. specialize (Hf x1 x2).
-    rewrite -later_equivI internal_eq_entails in Hf. apply Hf. by f_contractive.
-  Qed.
-
   (** Soundness statement for our modalities: facts derived under modalities in
   the empty context also without the modalities.
   For basic updates, soundness only holds for plain propositions. *)
@@ -128,7 +69,10 @@ Section derived.
   Proof. rewrite bupd_elim. done. Qed.
 
   Lemma laterN_soundness P n : (⊢ ▷^n P) → ⊢ P.
-  Proof. induction n; eauto using later_soundness. Qed.
+  Proof.
+    induction n as [|n IH]; intros ?; simpl; [done|].
+    by apply IH, later_soundness.
+  Qed.
 
   (** As pure demonstration, we also show that this holds for an arbitrary nesting
   of modalities. We have to do a bit of work to be able to state this theorem
@@ -153,7 +97,7 @@ Section derived.
     move: H. apply bi_emp_valid_mono.
     induction ms as [|m ms IH]; first done; simpl.
     destruct m; simpl; rewrite IH.
-    - rewrite -later_intro. apply bupd_elim. apply _.
+    - rewrite -later_intro. apply: bupd_elim.
     - done.
     - rewrite -later_intro persistently_elim. done.
     - rewrite -later_intro plainly_elim. done.
@@ -163,6 +107,6 @@ Section derived.
   modalities. Again this is just for demonstration and probably not practically
   useful. *)
   Corollary consistency : ¬ ⊢@{uPredI M} False.
-  Proof. intros H. by eapply pure_soundness. Qed.
+  Proof. apply: pure_soundness. Qed.
 End derived.
 End uPred.
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index ec1163a1579a72465509d83a892ae2a23ffb8068..3c79d54ffc1fc4f4e2f33c56e51f76714e363288 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -94,7 +94,7 @@ Lemma box_own_agree γ Q1 Q2 :
   box_own_prop γ Q1 ∗ box_own_prop γ Q2 ⊢ ▷ (Q1 ≡ Q2).
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
-  by rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
+  by rewrite option_validI /= agree_op_invI agree_equivI later_equivI /=.
 Qed.
 
 Lemma box_alloc : ⊢ box N ∅ True.
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index e9df6b26d52aad304753036e35b16db6fd55f04a..29c2c283153b957dcac765944060d0af23ddceb8 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -47,7 +47,7 @@ Section proofs.
   Proof. split; [done|]. apply _. Qed.
 
   Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ⌜q1 + q2 ≤ 1⌝%Qp.
-  Proof. rewrite -frac_valid -uPred.discrete_valid. apply (own_valid_2 γ q1 q2). Qed.
+  Proof. rewrite -frac_valid -bi_cmra_discrete_valid. apply (own_valid_2 γ q1 q2). Qed.
 
   Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
   Proof.
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index d09d019eae03506411f41af240a3e70d640c6a14..8532446cc93f726c0bf17c7443612714267e612c 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -82,24 +82,24 @@ Proof. rewrite /BiBUpdFUpd uPred_fupd_unseal. by iIntros (E P) ">? [$ $] !> !>".
 
 (** The interaction laws with the plainly modality are only supported when
   we opt out of the support for later credits. *)
-Global Instance uPred_bi_fupd_plainly_no_lc `{!invGS_gen HasNoLc Σ} :
-  BiFUpdPlainly (uPredI (iResUR Σ)).
+Global Instance uPred_bi_fupd_sbi_no_lc `{!invGS_gen HasNoLc Σ} :
+  BiFUpdSbi (uPredI (iResUR Σ)).
 Proof.
   split; rewrite uPred_fupd_unseal /uPred_fupd_def.
-  - iIntros (E P) "H [Hw HE]".
-    iAssert (â—‡ â–  P)%I as "#>HP".
+  - iIntros (E Pi) "H [Hw HE]".
+    iAssert (â—‡ <si_pure> Pi)%I as "#>HP".
     { by iMod ("H" with "[$]") as "(_ & _ & HP)". }
     by iFrame.
-  - iIntros (E P Q) "[H HQ] [Hw HE]".
-    iAssert (â—‡ â–  P)%I as "#>HP".
+  - iIntros (E Pi Q) "[H HQ] [Hw HE]".
+    iAssert (â—‡ <si_pure> Pi)%I as "#>HP".
     { by iMod ("H" with "HQ [$]") as "(_ & _ & HP)". }
     by iFrame.
-  - iIntros (E P) "H [Hw HE]".
-    iAssert (â–· â—‡ â–  P)%I as "#HP".
+  - iIntros (E Pi) "H [Hw HE]".
+    iAssert (â–· â—‡ <si_pure> Pi)%I as "#HP".
     { iNext. by iMod ("H" with "[$]") as "(_ & _ & HP)". }
     iFrame. iIntros "!> !> !>". by iMod "HP".
-  - iIntros (E A Φ) "HΦ [Hw HE]".
-    iAssert (◇ ■ ∀ x : A, Φ x)%I as "#>HP".
+  - iIntros (E A Φi) "HΦ [Hw HE]".
+    iAssert (◇ ∀ x : A, <si_pure> Φi x)%I as "#>HP".
     { iIntros (x). by iMod ("HΦ" with "[$Hw $HE]") as "(_&_&?)". }
     by iFrame.
 Qed.
diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 6fa4c97a4f9af6d66697e9010cd23b8b3e0cc217..81ee3aca8cbcf49c152bd67311cd87a2dad3b1f4 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -105,11 +105,9 @@ Local Instance iRes_singleton_ne γ : NonExpansive (@iRes_singleton Σ A _ γ).
 Proof. by intros n a a' Ha; apply discrete_fun_singleton_ne; rewrite Ha. Qed.
 Local Lemma iRes_singleton_validI γ a : ✓ (iRes_singleton γ a) ⊢@{iPropI Σ} ✓ a.
 Proof.
-  rewrite /iRes_singleton.
-  rewrite discrete_fun_validI (forall_elim (inG_id i)) discrete_fun_lookup_singleton.
-  rewrite singleton_validI.
-  trans (✓ cmra_transport inG_prf a : iProp Σ)%I; last by destruct inG_prf.
-  apply valid_entails=> n. apply inG_unfold_validN.
+  sbi_unfold=> n. rewrite /iRes_singleton.
+  rewrite discrete_fun_singleton_validN singleton_validN inG_unfold_validN.
+  by destruct inG_prf.
 Qed.
 Local Lemma iRes_singleton_op γ a1 a2 :
   iRes_singleton γ (a1 ⋅ a2) ≡ iRes_singleton γ a1 ⋅ iRes_singleton γ a2.
@@ -204,7 +202,7 @@ Proof.
   rewrite and_exist_l. f_equiv=> b. rewrite and_exist_l. apply exist_elim=> r'.
   rewrite assoc. apply and_mono_l.
   etrans; [|apply ownM_mono, (cmra_included_l _ r')].
-  eapply (internal_eq_rewrite' _ _ uPred_ownM _); [apply and_elim_r|].
+  eapply (internal_eq_rewrite' _ _ uPred_ownM _ _); [apply and_elim_r|].
   apply and_elim_l.
 Qed.
 
diff --git a/iris/base_logic/proofmode.v b/iris/base_logic/proofmode.v
index 0c323e33132c164de3432ae6f98c58422ef14e74..72ec3e27920949edf6237b691a4c3907ce482320 100644
--- a/iris/base_logic/proofmode.v
+++ b/iris/base_logic/proofmode.v
@@ -9,17 +9,6 @@ Section class_instances.
   Context {M : ucmra}.
   Implicit Types P Q R : uPred M.
 
-  Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
-    @IntoPure (uPredI M) (✓ a) (✓ a).
-  Proof. rewrite /IntoPure. by rewrite uPred.discrete_valid. Qed.
-
-  Global Instance from_pure_cmra_valid {A : cmra} (a : A) :
-    @FromPure (uPredI M) false (✓ a) (✓ a).
-  Proof.
-    rewrite /FromPure /=. eapply bi.pure_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).
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 4b0c4486860227c8d0a33a6d153a95c744bd2af7..5b2434d1480b4d3f1d4b965664f5a109c224edbe 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -324,16 +324,6 @@ Global Arguments uPred_exist {M A}.
 Local Definition uPred_exist_unseal :
   @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).
 
-Local Program Definition uPred_internal_eq_def {M} {A : ofe} (a1 a2 : A) : uPred M :=
-  {| uPred_holds n x := a1 ≡{n}≡ a2 |}.
-Solve Obligations with naive_solver eauto 2 using dist_le.
-Local Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def).
-Proof. by eexists. Qed.
-Definition uPred_internal_eq := uPred_internal_eq_aux.(unseal).
-Global Arguments uPred_internal_eq {M A}.
-Local Definition uPred_internal_eq_unseal :
-  @uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
-
 Local 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.
@@ -361,18 +351,6 @@ Global Arguments uPred_wand {M}.
 Local Definition uPred_wand_unseal :
   @uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_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. *)
-Local 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.
-Local Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. by eexists. Qed.
-Definition uPred_plainly := uPred_plainly_aux.(unseal).
-Global Arguments uPred_plainly {M}.
-Local Definition uPred_plainly_unseal :
-  @uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
-
 Local Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
 Solve Obligations with naive_solver eauto using uPred_mono, cmra_core_monoN.
@@ -406,16 +384,6 @@ Global Arguments uPred_ownM {M}.
 Local Definition uPred_ownM_unseal :
   @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
 
-Local Program Definition uPred_cmra_valid_def {M} {A : cmra} (a : A) : uPred M :=
-  {| uPred_holds n x := ✓{n} a |}.
-Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
-Local Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def).
-Proof. by eexists. Qed.
-Definition uPred_cmra_valid := uPred_cmra_valid_aux.(unseal).
-Global Arguments uPred_cmra_valid {M A}.
-Local Definition uPred_cmra_valid_unseal :
-  @uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
-
 Local 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' |}.
@@ -432,9 +400,6 @@ Global Arguments uPred_bupd {M}.
 Local Definition uPred_bupd_unseal :
   @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.
-
 (** Primitive logical rules.
     These are not directly usable later because they do not refer to the BI
     connectives. *)
@@ -442,10 +407,10 @@ Module uPred_primitive.
 Local Definition uPred_unseal :=
   (uPred_si_pure_unseal, uPred_si_emp_valid_unseal,
   uPred_and_unseal, uPred_or_unseal, uPred_impl_unseal,
-  uPred_forall_unseal, uPred_exist_unseal, uPred_internal_eq_unseal,
-  uPred_sep_unseal, uPred_wand_unseal, uPred_plainly_unseal,
+  uPred_forall_unseal, uPred_exist_unseal,
+  uPred_sep_unseal, uPred_wand_unseal,
   uPred_persistently_unseal, uPred_later_unseal, uPred_ownM_unseal,
-  uPred_cmra_valid_unseal, @uPred_bupd_unseal).
+  @uPred_bupd_unseal).
 Ltac unseal :=
   rewrite !uPred_unseal /=.
 
@@ -480,8 +445,6 @@ Section primitive.
   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.
 
@@ -551,14 +514,6 @@ Section primitive.
       apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
   Qed.
 
-  Lemma internal_eq_ne (A : ofe) :
-    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.
@@ -578,12 +533,6 @@ Section primitive.
     eapply 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.
@@ -596,13 +545,6 @@ Section primitive.
     unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
   Qed.
 
-  Lemma cmra_valid_ne {A : cmra} :
-    NonExpansive (@uPred_cmra_valid M A).
-  Proof.
-    intros n a b Ha; unseal; split=> n' x ? /=.
-    by rewrite (dist_le _ _ _ _ Ha); last lia.
-  Qed.
-
   Lemma bupd_ne : NonExpansive (@uPred_bupd M).
   Proof.
     intros n P Q HPQ.
@@ -647,15 +589,6 @@ Section primitive.
     eapply uPred_mono with n ε; eauto using ucmra_unit_leastN.
   Qed.
 
-  (** FIXME: Rename once we delete the current [prop_ext]. *)
-  Lemma prop_ext_new P Q :
-    siProp_entails (<si_emp_valid> ((P -∗ Q) ∧ (Q -∗ P)))
-                   (siProp_internal_eq P Q).
-  Proof.
-    unseal; siProp_primitive.unseal.
-    split=> n /=. setoid_rewrite (left_id ε op). split; naive_solver.
-  Qed.
-
   Lemma persistently_impl_si_pure Pi Q :
     (<si_pure> Pi → □ Q) ⊢ □ (<si_pure> Pi → Q).
   Proof.
@@ -664,6 +597,14 @@ Section primitive.
     apply (HPQ n' x); eauto using cmra_validN_le.
   Qed.
 
+  Lemma prop_ext_2 P Q :
+    siProp_entails (<si_emp_valid> ((P -∗ Q) ∧ (Q -∗ P)))
+                   (siProp_internal_eq P Q).
+  Proof.
+    unseal; siProp_primitive.unseal.
+    split=> n /=. setoid_rewrite (left_id ε op). split; naive_solver.
+  Qed.
+
   (** Introduction and elimination rules *)
   Lemma and_elim_l P Q : P ∧ Q ⊢ P.
   Proof. by unseal; split=> n x ? [??]. Qed.
@@ -763,40 +704,6 @@ Section primitive.
     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_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
-  Proof.
-    unseal; split=> n x ? /=. setoid_rewrite (left_id ε op). split; 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.
@@ -838,54 +745,6 @@ Section primitive.
   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 : ofe} P (a : A) : P ⊢ (a ≡ a).
-  Proof. unseal; by split=> n x ??; simpl. Qed.
-  Lemma internal_eq_rewrite {A : ofe} 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 {A} {B : A → ofe} (g1 g2 : discrete_fun B) :
-    (∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
-  Proof. by unseal. Qed.
-  Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sigO P) :
-    proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
-  Proof. by unseal. Qed.
-
-  Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
-  Proof.
-    unseal. split. intros [|n]; simpl; [done|].
-    intros ?? Heq; apply Heq; auto.
-  Qed.
-  Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
-  Proof.
-    unseal. split. intros n ? ? Hn; split; intros m Hlt; simpl in *.
-    destruct n as [|n]; first lia.
-    eauto using dist_le with si_solver.
-  Qed.
-
-  Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
-  Proof.
-    unseal; siProp_primitive.unseal=> ?.
-    split=> n x ?. by apply (discrete_iff n).
-  Qed.
-
-  (** This is really just a special case of an entailment
-  between two [siProp], but we do not have the infrastructure
-  to express the more general case. This temporary proof rule will
-  be replaced by the proper one eventually. *)
-  Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
-    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
-  Proof.
-    split.
-    - unseal=> -[Hsi] n. apply (Hsi _ ε), ucmra_unit_validN.
-    - unseal=> Hsi. split=>n x ?. apply Hsi.
-  Qed.
 
   (** Basic update modality *)
   Lemma bupd_intro P : P ⊢ |==> P.
@@ -909,11 +768,10 @@ Section primitive.
     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.
+  Lemma bupd_si_pure Pi : (|==> <si_pure> Pi) ⊢ <si_pure> Pi.
   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 *)
@@ -935,9 +793,11 @@ Section primitive.
   Qed.
   Lemma ownM_unit P : P ⊢ (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).
+  Lemma later_ownM a :
+    ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ <si_pure> siProp_internal_eq a b.
   Proof.
-    unseal; split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
+    unseal; siProp_primitive.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.
@@ -953,51 +813,10 @@ Section primitive.
     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 : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
-  Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
-  Lemma cmra_valid_elim {A : cmra} (a : A) : ✓ a ⊢ ⌜ ✓{0} a ⌝.
+  Lemma ownM_valid (a : M) : uPred_ownM a ⊢ <si_pure> siProp_cmra_valid a.
   Proof.
     unseal; siProp_primitive.unseal.
-    split=> n x ??; apply cmra_validN_le with n; auto.
-  Qed.
-  Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
-  Proof. by unseal. Qed.
-  Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
-  Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
-
-  (** This is really just a special case of an entailment
-  between two [siProp], but we do not have the infrastructure
-  to express the more general case. This temporary proof rule will
-  be replaced by the proper one eventually. *)
-  Lemma valid_entails {A B : cmra} (a : A) (b : B) :
-    (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
-  Proof. unseal=> Hval. split=>n x ?. apply Hval. Qed.
-
-  (** Consistency/soundness statement *)
-  (** The lemmas [pure_soundness] and [internal_eq_soundness] should become an
-  instance of [siProp] soundness in the future. *)
-  Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
-  Proof.
-    unseal; siProp_primitive.unseal=> -[H].
-    by apply (H 0 ε); eauto using ucmra_unit_validN.
-  Qed.
-
-  Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
-  Proof.
-    unseal; siProp_primitive.unseal=> -[H]. apply equiv_dist=> n.
-    by apply (H n ε); eauto using ucmra_unit_validN.
-  Qed.
-
-  Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
-  Proof.
-    unseal; siProp_primitive.unseal=> -[HP]; split=> n x Hx _.
-    apply uPred_mono with n ε; eauto using ucmra_unit_leastN.
-    by apply (HP (S n)); eauto using ucmra_unit_validN.
+    split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
   Qed.
 End primitive.
 End uPred_primitive.
diff --git a/iris/base_logic/algebra.v b/iris/bi/algebra.v
similarity index 52%
rename from iris/base_logic/algebra.v
rename to iris/bi/algebra.v
index c33e5b8fd6f81c01cd54541ee506ae0801e6e8a9..4bc9c29ebebc2da1e6610fcdf9a6af95b3e5ca99 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/bi/algebra.v
@@ -1,27 +1,44 @@
 From iris.algebra Require Import cmra view auth agree csum list excl gmap.
 From iris.algebra.lib Require Import excl_auth gmap_view dfrac_agree.
-From iris.base_logic Require Import bi derived.
+From iris.bi Require Export sbi_unfold derived_laws.
 From iris.prelude Require Import options.
-
-(** Internalized properties of our CMRA constructions. *)
-Local Coercion uPred_holds : uPred >-> Funclass.
-
-Section upred.
-  Context {M : ucmra}.
-
-  (* Force implicit argument M *)
-  Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
-  Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
-  Notation "⊢ Q" := (bi_entails (PROP:=uPredI M) True Q).
+Local Set Default Proof Using "Type*".
+
+Section algebra.
+  Context `{!Sbi PROP}.
+
+  (* Force implicit argument [PROP] *)
+  Notation "P ⊢ Q" := (bi_entails (PROP:=PROP) P Q).
+  Notation "P ⊣⊢ Q" := (equiv (A:=PROP) P%I Q%I).
+  Notation "⊢ Q" := (bi_emp_valid (PROP:=PROP) Q).
+
+  Lemma ucmra_unit_validI {A : ucmra} : ⊢ ✓ (ε : A).
+  Proof. sbi_unfold. apply ucmra_unit_validN. Qed.
+  Lemma cmra_validI_op_r {A : cmra} (x y : A) : ✓ (x ⋅ y) ⊢ ✓ y.
+  Proof. sbi_unfold=> n. apply cmra_validN_op_r. Qed.
+  Lemma cmra_validI_op_l {A : cmra} (x y : A) : ✓ (x ⋅ y) ⊢ ✓ x.
+  Proof. sbi_unfold=> n. apply cmra_validN_op_l. Qed.
+  Lemma cmra_later_opI `{!CmraTotal A} (x y1 y2 : A) :
+    ▷ (✓ x ∧ x ≡ y1 ⋅ y2) ⊢ ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ ▷ (z1 ≡ y1) ∧ ▷ (z2 ≡ y2).
+  Proof.
+    sbi_unfold=> -[|n].
+    - intros _. exists x, (core x). by rewrite cmra_core_r.
+    - intros [??].
+      destruct (cmra_extend n x y1 y2) as (z1 & z2 & ? & ? & ?); [done..|].
+      exists z1, z2. auto using equiv_dist.
+  Qed.
+  Lemma cmra_morphism_validI {A B : cmra} (f : A → B) `{!CmraMorphism f} x :
+    ✓ x ⊢ ✓ (f x).
+  Proof. sbi_unfold=> n. by apply cmra_morphism_validN. Qed.
 
   Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
-  Proof. by uPred.unseal. Qed.
+  Proof. by sbi_unfold. Qed.
   Lemma option_validI {A : cmra} (mx : option A) :
-    ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
-  Proof. uPred.unseal. by destruct mx. Qed.
+    ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
+  Proof. destruct mx; by sbi_unfold. Qed.
   Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
     ✓ g ⊣⊢ ∀ i, ✓ g i.
-  Proof. by uPred.unseal. Qed.
+  Proof. by sbi_unfold. Qed.
 
   Section gmap_ofe.
     Context `{Countable K} {A : ofe}.
@@ -29,11 +46,11 @@ Section upred.
     Implicit Types i : K.
 
     Lemma gmap_equivI m1 m2 : m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
-    Proof. by uPred.unseal. Qed.
+    Proof. by sbi_unfold. Qed.
 
     Lemma gmap_union_equiv_eqI m m1 m2 :
       m ≡ m1 ∪ m2 ⊣⊢ ∃ m1' m2', ⌜ m = m1' ∪ m2' ⌝ ∧ m1' ≡ m1 ∧ m2' ≡ m2.
-    Proof. uPred.unseal; split=> n x _. apply gmap_union_dist_eq. Qed.
+    Proof. sbi_unfold=> n. apply gmap_union_dist_eq. Qed.
   End gmap_ofe.
 
   Section gmap_cmra.
@@ -41,16 +58,9 @@ Section upred.
     Implicit Types m : gmap K A.
 
     Lemma gmap_validI m : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
-    Proof. by uPred.unseal. Qed.
+    Proof. by sbi_unfold. Qed.
     Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢ ✓ x.
-    Proof.
-      rewrite gmap_validI. apply: anti_symm.
-      - rewrite (bi.forall_elim i) lookup_singleton option_validI. done.
-      - apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
-        + rewrite lookup_singleton option_validI. done.
-        + rewrite lookup_singleton_ne // option_validI.
-          apply bi.True_intro.
-    Qed.
+    Proof. sbi_unfold=> n. apply singleton_validN. Qed.
   End gmap_cmra.
 
   Section list_ofe.
@@ -58,16 +68,26 @@ Section upred.
     Implicit Types l : list A.
 
     Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
-    Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
+    Proof. sbi_unfold. intros n. apply list_dist_lookup. Qed.
   End list_ofe.
 
   Section excl.
     Context {A : ofe}.
     Implicit Types x : excl A.
 
+    Lemma excl_equivI x y :
+      x ≡ y ⊣⊢ match x, y with
+                          | Excl a, Excl b => a ≡ b
+                          | ExclBot, ExclBot => True
+                          | _, _ => False
+                          end.
+    Proof.
+      destruct x, y; sbi_unfold; (split; [by inversion 1|by try constructor]).
+    Qed.
+
     Lemma excl_validI x :
       ✓ x ⊣⊢ if x is ExclBot then False else True.
-    Proof. uPred.unseal. by destruct x. Qed.
+    Proof. destruct x; sbi_unfold; (split; [by inversion 1|by try constructor]). Qed.
   End excl.
 
   Section agree.
@@ -76,31 +96,17 @@ Section upred.
     Implicit Types x y : agree A.
 
     Lemma agree_equivI a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b).
-    Proof.
-      uPred.unseal. do 2 split.
-      - intros Hx. exact: (inj to_agree).
-      - intros Hx. exact: to_agree_ne.
-    Qed.
-    Lemma agree_validI x y : ✓ (x ⋅ y) ⊢ x ≡ y.
-    Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
+    Proof. sbi_unfold=> n. apply: inj_iff. Qed.
+    Lemma agree_op_invI x y : ✓ (x ⋅ y) ⊢ x ≡ y.
+    Proof. sbi_unfold=> n. apply agree_op_invN. Qed.
 
     Lemma to_agree_validI a : ⊢ ✓ to_agree a.
-    Proof. uPred.unseal; done. Qed.
+    Proof. by sbi_unfold. Qed.
     Lemma to_agree_op_validI a b : ✓ (to_agree a ⋅ to_agree b) ⊣⊢ a ≡ b.
-    Proof.
-      apply bi.entails_anti_sym.
-      - rewrite agree_validI. by rewrite agree_equivI.
-      - pose (Ψ := (λ x : A, ✓ (to_agree a ⋅ to_agree x) : uPred M)%I).
-        assert (NonExpansive Ψ) as ? by solve_proper.
-        rewrite (internal_eq_rewrite a b Ψ).
-        eapply bi.impl_elim; first reflexivity.
-        etrans; first apply bi.True_intro.
-        subst Ψ; simpl.
-        rewrite agree_idemp. apply to_agree_validI.
-    Qed.
+    Proof. sbi_unfold. apply to_agree_op_validN. Qed.
 
     Lemma to_agree_uninjI x : ✓ x ⊢ ∃ a, to_agree a ≡ x.
-    Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
+    Proof. sbi_unfold=> n. exact: to_agree_uninjN. Qed.
 
     (** Derived lemma: If two [x y : agree O] compose to some [to_agree a],
       they are internally equal, and also equal to the [to_agree a].
@@ -113,9 +119,10 @@ Section upred.
       x ⋅ y ≡ to_agree a ⊢ x ≡ y ∧ y ≡ to_agree a.
     Proof.
       assert (x ⋅ y ≡ to_agree a ⊢ x ≡ y) as Hxy_equiv.
-      { rewrite -(agree_validI x y) internal_eq_sym.
-        apply: (internal_eq_rewrite' _ _ (λ o, ✓ o)%I); first done.
-        rewrite -to_agree_validI. apply bi.True_intro. }
+      { rewrite -(agree_op_invI x y) internal_eq_sym.
+        apply: (internal_eq_rewrite' _ _ (λ o, ✓ o)%I); [solve_proper|done|].
+        rewrite -(bi.absorbing_absorbingly (✓ _)).
+        rewrite -to_agree_validI bi.absorbingly_emp_True. apply bi.True_intro. }
       apply bi.and_intro; first done.
       rewrite -{1}(idemp bi_and (_ ≡ _)%I) {1}Hxy_equiv. apply bi.impl_elim_l'.
       apply: (internal_eq_rewrite' _ _
@@ -124,6 +131,23 @@ Section upred.
     Qed.
   End agree.
 
+  Section csum_ofe.
+    Context {A B : ofe}.
+    Implicit Types a : A.
+    Implicit Types b : B.
+
+    Lemma csum_equivI (x y : csum A B) :
+      x ≡ y ⊣⊢ match x, y with
+                          | Cinl a, Cinl a' => a ≡ a'
+                          | Cinr b, Cinr b' => b ≡ b'
+                          | CsumBot, CsumBot => True
+                          | _, _ => False
+                          end.
+    Proof.
+      destruct x, y; sbi_unfold; (split; [by inversion 1|by try constructor]).
+    Qed.
+  End csum_ofe.
+
   Section csum_cmra.
     Context {A B : cmra}.
     Implicit Types a : A.
@@ -135,7 +159,7 @@ Section upred.
                         | Cinr b => ✓ b
                         | CsumBot => False
                         end.
-    Proof. uPred.unseal. by destruct x. Qed.
+    Proof. destruct x; by sbi_unfold. Qed.
   End csum_cmra.
 
   Section view.
@@ -145,62 +169,60 @@ Section upred.
     Implicit Types b : B.
     Implicit Types x y : view rel.
 
-    Lemma view_both_dfrac_validI_1 (relI : uPred M) dq a b :
-      (∀ n (x : M), rel n a b → relI n x) →
-      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ relI.
+    Lemma view_both_dfrac_validI_1 (relI : siProp) dq a b :
+      (∀ n, rel n a b → siProp_holds relI n) →
+      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
     Proof.
-      intros Hrel. uPred.unseal. split=> n x _ /=.
-      rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
+      intros. sbi_unfold=> n. rewrite view_both_dfrac_validN. naive_solver.
     Qed.
-    Lemma view_both_dfrac_validI_2 (relI : uPred M) dq a b :
-      (∀ n (x : M), relI n x → rel n a b) →
-      ⌜✓dq⌝ ∧ relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
+    Lemma view_both_dfrac_validI_2 (relI : siProp) dq a b :
+      (∀ n, siProp_holds relI n → rel n a b) →
+      ⌜✓dq⌝ ∧ <si_pure> relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
     Proof.
-      intros Hrel. uPred.unseal. split=> n x _ /=.
-      rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
+      intros. sbi_unfold=> n. rewrite view_both_dfrac_validN. naive_solver.
     Qed.
-    Lemma view_both_dfrac_validI (relI : uPred M) dq a b :
-      (∀ n (x : M), rel n a b ↔ relI n x) →
-      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
+    Lemma view_both_dfrac_validI (relI : siProp) dq a b :
+      (∀ n, rel n a b ↔ siProp_holds relI n) →
+      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
     Proof.
       intros. apply (anti_symm _);
         [apply view_both_dfrac_validI_1|apply view_both_dfrac_validI_2]; naive_solver.
     Qed.
 
-    Lemma view_both_validI_1 (relI : uPred M) a b :
-      (∀ n (x : M), rel n a b → relI n x) →
-      ✓ (●V a ⋅ ◯V b : view rel) ⊢ relI.
+    Lemma view_both_validI_1 (relI : siProp) a b :
+      (∀ n, rel n a b → siProp_holds relI n) →
+      ✓ (●V a ⋅ ◯V b : view rel) ⊢ <si_pure> relI.
     Proof. intros. by rewrite view_both_dfrac_validI_1 // bi.and_elim_r. Qed.
-    Lemma view_both_validI_2 (relI : uPred M) a b :
-      (∀ n (x : M), relI n x → rel n a b) →
-      relI ⊢ ✓ (●V a ⋅ ◯V b : view rel).
+    Lemma view_both_validI_2 (relI : siProp) a b :
+      (∀ n, siProp_holds relI n → rel n a b) →
+      <si_pure> relI ⊢ ✓ (●V a ⋅ ◯V b : view rel).
     Proof.
       intros. rewrite -view_both_dfrac_validI_2 //.
       apply bi.and_intro; [|done]. by apply bi.pure_intro.
     Qed.
-    Lemma view_both_validI (relI : uPred M) a b :
-      (∀ n (x : M), rel n a b ↔ relI n x) →
-      ✓ (●V a ⋅ ◯V b : view rel) ⊣⊢ relI.
+    Lemma view_both_validI (relI : siProp) a b :
+      (∀ n, rel n a b ↔ siProp_holds relI n) →
+      ✓ (●V a ⋅ ◯V b : view rel) ⊣⊢ <si_pure> relI.
     Proof.
       intros. apply (anti_symm _);
         [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
     Qed.
 
-    Lemma view_auth_dfrac_validI (relI : uPred M) dq a :
-      (∀ n (x : M), relI n x ↔ rel n a ε) →
-      ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
+    Lemma view_auth_dfrac_validI (relI : siProp) dq a :
+      (∀ n, siProp_holds relI n ↔ rel n a ε) →
+      ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
     Proof.
       intros. rewrite -(right_id ε op (●V{dq} a)). by apply view_both_dfrac_validI.
     Qed.
-    Lemma view_auth_validI (relI : uPred M) a :
-      (∀ n (x : M), relI n x ↔ rel n a ε) →
-      ✓ (●V a : view rel) ⊣⊢ relI.
+    Lemma view_auth_validI (relI : siProp) a :
+      (∀ n, siProp_holds relI n ↔ rel n a ε) →
+      ✓ (●V a : view rel) ⊣⊢ <si_pure> relI.
     Proof. intros. rewrite -(right_id ε op (●V a)). by apply view_both_validI. Qed.
 
-    Lemma view_frag_validI (relI : uPred M) b :
-      (∀ n (x : M), relI n x ↔ ∃ a, rel n a b) →
-      ✓ (◯V b : view rel) ⊣⊢ relI.
-    Proof. uPred.unseal=> Hrel. split=> n x _. by rewrite Hrel. Qed.
+    Lemma view_frag_validI (relI : siProp) b :
+      (∀ n, siProp_holds relI n ↔ ∃ a, rel n a b) →
+      ✓ (◯V b : view rel) ⊣⊢ <si_pure> relI.
+    Proof. intros Hrel. sbi_unfold=> n. by rewrite Hrel. Qed.
   End view.
 
   Section auth.
@@ -209,33 +231,22 @@ Section upred.
     Implicit Types x y : auth A.
 
     Lemma auth_auth_dfrac_validI dq a : ✓ (●{dq} a) ⊣⊢ ⌜✓dq⌝ ∧ ✓ a.
-    Proof.
-      apply view_auth_dfrac_validI=> n. uPred.unseal; split; [|by intros [??]].
-      split; [|done]. apply ucmra_unit_leastN.
-    Qed.
+    Proof. sbi_unfold=> n. apply auth_auth_dfrac_validN. Qed.
     Lemma auth_auth_validI a : ✓ (● a) ⊣⊢ ✓ a.
-    Proof.
-      by rewrite auth_auth_dfrac_validI bi.pure_True // left_id.
-    Qed.
+    Proof. sbi_unfold=> n. apply auth_auth_validN. Qed.
     Lemma auth_auth_dfrac_op_validI dq1 dq2 a1 a2 :
       ✓ (●{dq1} a1 ⋅ ●{dq2} a2) ⊣⊢ ✓ (dq1 ⋅ dq2) ∧ (a1 ≡ a2) ∧ ✓ a1.
-    Proof. uPred.unseal; split => n x _. apply auth_auth_dfrac_op_validN. Qed.
+    Proof. sbi_unfold=> n. apply auth_auth_dfrac_op_validN. Qed.
 
     Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢ ✓ a.
-    Proof.
-      apply view_frag_validI=> n x.
-      rewrite auth_view_rel_exists. by uPred.unseal.
-    Qed.
+    Proof. sbi_unfold=> n. apply auth_frag_validN. Qed.
 
     Lemma auth_both_dfrac_validI dq a b :
       ✓ (●{dq} a ⋅ ◯ b) ⊣⊢ ⌜✓dq⌝ ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
-    Proof. apply view_both_dfrac_validI=> n. by uPred.unseal. Qed.
+    Proof.  sbi_unfold=> n. apply auth_both_dfrac_validN. Qed.
     Lemma auth_both_validI a b :
       ✓ (● a ⋅ ◯ b) ⊣⊢ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
-    Proof.
-      by rewrite auth_both_dfrac_validI bi.pure_True // left_id.
-    Qed.
-
+    Proof. sbi_unfold=> n. apply auth_both_validN. Qed.
   End auth.
 
   Section excl_auth.
@@ -243,11 +254,7 @@ Section upred.
     Implicit Types a b : A.
 
     Lemma excl_auth_agreeI a b : ✓ (●E a ⋅ ◯E b) ⊢ (a ≡ b).
-    Proof.
-      rewrite auth_both_validI bi.and_elim_l.
-      apply bi.exist_elim=> -[[c|]|];
-        by rewrite option_equivI /= excl_equivI //= bi.False_elim.
-    Qed.
+    Proof. sbi_unfold=> n. apply excl_auth_agreeN. Qed.
   End excl_auth.
 
   Section dfrac_agree.
@@ -255,18 +262,11 @@ Section upred.
     Implicit Types a b : A.
 
     Lemma dfrac_agree_validI dq a : ✓ (to_dfrac_agree dq a) ⊣⊢ ⌜✓ dq⌝.
-    Proof.
-      rewrite prod_validI /= uPred.discrete_valid. apply bi.entails_anti_sym.
-      - by rewrite bi.and_elim_l.
-      - apply bi.and_intro; first done. etrans; last apply to_agree_validI.
-        apply bi.True_intro.
-    Qed.
+    Proof. sbi_unfold=> n. rewrite /to_dfrac_agree pair_validN. naive_solver. Qed.
 
     Lemma dfrac_agree_validI_2 dq1 dq2 a b :
       ✓ (to_dfrac_agree dq1 a ⋅ to_dfrac_agree dq2 b) ⊣⊢ ⌜✓ (dq1 ⋅ dq2)⌝ ∧ (a ≡ b).
-    Proof.
-      rewrite prod_validI /= uPred.discrete_valid to_agree_op_validI //.
-    Qed.
+    Proof. rewrite prod_validI /= bi_cmra_discrete_valid to_agree_op_validI //. Qed.
 
     Lemma frac_agree_validI q a : ✓ (to_frac_agree q a) ⊣⊢ ⌜(q ≤ 1)%Qp⌝.
     Proof.
@@ -287,19 +287,11 @@ Section upred.
     Lemma gmap_view_both_validI m k dq v :
       ✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ⊢
       ✓ dq ∧ m !! k ≡ Some v.
-    Proof.
-      rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
-      intros n a. uPred.unseal. apply gmap_view.gmap_view_rel_lookup.
-    Qed.
+    Proof. sbi_unfold=> n. apply gmap_view_both_validN. Qed.
 
     Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
       ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢
       ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
-    Proof.
-      rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI=> n x.
-      rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
-      rewrite -pair_op pair_validN to_agree_op_validN. by uPred.unseal.
-    Qed.
-
+    Proof. sbi_unfold=> n. apply gmap_view_frag_op_validN. Qed.
   End gmap_view.
-End upred.
+End algebra.
diff --git a/iris/bi/bi.v b/iris/bi/bi.v
index f44803e738cc08ed0a16d996b35df1be8f57f148..31d810444257bcae4da070e4fc0b3d2ed92f736a 100644
--- a/iris/bi/bi.v
+++ b/iris/bi/bi.v
@@ -1,5 +1,6 @@
 From iris.bi Require Export derived_laws derived_laws_later big_op.
-From iris.bi Require Export sbi updates internal_eq plainly embedding.
+From iris.bi Require Export updates embedding.
+From iris.bi Require Export sbi sbi_unfold internal_eq plainly cmra_valid algebra.
 From iris.prelude Require Import options.
 
 Module Import bi.
diff --git a/iris/bi/cmra_valid.v b/iris/bi/cmra_valid.v
new file mode 100644
index 0000000000000000000000000000000000000000..95e3f162ac658de54497680d0ad84b72a8333135
--- /dev/null
+++ b/iris/bi/cmra_valid.v
@@ -0,0 +1,80 @@
+From iris.algebra Require Export cmra.
+From iris.bi Require Export sbi plainly.
+From iris.bi Require Import derived_laws_later.
+From iris.prelude Require Import options.
+
+Definition bi_cmra_valid `{!Sbi PROP} {A : cmra} (a : A) : PROP :=
+  <si_pure> siProp_cmra_valid a.
+Global Arguments bi_cmra_valid : simpl never.
+Global Typeclasses Opaque bi_cmra_valid.
+Global Instance: Params (@bi_cmra_valid) 3 := {}.
+Notation "✓ a" := (bi_cmra_valid a) : bi_scope.
+
+Section cmra_valid.
+  Context `{!Sbi PROP}.
+  Implicit Types P Q : PROP.
+
+  (* Force implicit argument PROP *)
+  Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+  Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
+
+  Global Instance bi_cmra_valid_ne {A : cmra} :
+    NonExpansive (@bi_cmra_valid PROP _ A).
+  Proof.
+    intros n x x' ?. by apply si_pure_ne, siProp_primitive.cmra_valid_ne.
+  Qed.
+  Global Instance bi_cmra_valid_proper {A : cmra} :
+    Proper ((≡) ==> (⊣⊢)) (@bi_cmra_valid PROP _ A).
+  Proof. apply ne_proper, _. Qed.
+
+  Lemma bi_cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
+  Proof.
+    intros. rewrite (bi.True_intro P) -si_pure_pure.
+    by apply si_pure_mono, siProp_primitive.cmra_valid_intro.
+  Qed.
+  Lemma bi_cmra_valid_elim {A : cmra} (a : A) : ✓ a ⊢ ⌜ ✓{0} a ⌝.
+  Proof.
+    rewrite -si_pure_pure.
+    by apply si_pure_mono, siProp_primitive.cmra_valid_elim.
+  Qed.
+  (* FIXME: Remove in favor of cmra_validN_op_r *)
+  Lemma bi_cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+  Proof. by apply si_pure_mono, siProp_primitive.cmra_valid_weaken. Qed.
+  Lemma bi_cmra_valid_entails {A B : cmra} (a : A) (b : B) :
+    (✓ a ⊢ ✓ b) ↔ ∀ n, ✓{n} a → ✓{n} b.
+  Proof. rewrite si_pure_entails. apply siProp_primitive.valid_entails. Qed.
+
+  Lemma si_pure_cmra_valid {A : cmra} (a : A) : <si_pure> ✓ a ⊣⊢ ✓ a.
+  Proof. done. Qed.
+  Lemma persistently_cmra_valid {A : cmra} (a : A) : <pers> ✓ a ⊣⊢ ✓ a.
+  Proof. apply persistently_si_pure. Qed.
+  Lemma plainly_cmra_valid {A : cmra} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
+  Proof. apply plainly_si_pure. Qed.
+  Lemma intuitionistically_cmra_valid `{!BiAffine PROP} {A : cmra} (a : A) :
+    □ ✓ a ⊣⊢ ✓ a.
+  Proof.
+    by rewrite bi.intuitionistically_into_persistently persistently_cmra_valid.
+  Qed.
+  Lemma bi_cmra_discrete_valid `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+  Proof.
+    apply (anti_symm _).
+    - rewrite bi_cmra_valid_elim. by apply bi.pure_mono, cmra_discrete_valid.
+    - apply bi.pure_elim'=> ?. by apply bi_cmra_valid_intro.
+  Qed.
+
+  Global Instance bi_cmra_valid_timeless `{!CmraDiscrete A} (a : A) :
+    Timeless (PROP:=PROP) (✓ a).
+  Proof. rewrite /Timeless !bi_cmra_discrete_valid. apply (timeless _). Qed.
+
+  Global Instance bi_cmra_valid_plain {A : cmra} (a : A) :
+    Plain (PROP:=PROP) (✓ a).
+  Proof. rewrite -plainly_cmra_valid. apply _. Qed.
+
+  Global Instance bi_cmra_valid_absorbing {A : cmra} (a : A) :
+    Absorbing (PROP:=PROP) (✓ a).
+  Proof. rewrite -persistently_cmra_valid. apply _. Qed.
+
+  Global Instance bi_cmra_valid_persistent {A : cmra} (a : A) :
+    Persistent (PROP:=PROP) (✓ a).
+  Proof. rewrite -persistently_cmra_valid. apply _. Qed.
+End cmra_valid.
diff --git a/iris/bi/derived_laws_later.v b/iris/bi/derived_laws_later.v
index d89ef824376e443981197beb48803f79876a9b36..b7c682c1c2ddd57b4bff35858df131c02df78fc4 100644
--- a/iris/bi/derived_laws_later.v
+++ b/iris/bi/derived_laws_later.v
@@ -354,9 +354,10 @@ Global Instance impl_timeless `{!BiLöb PROP} P Q : Timeless Q → Timeless (P 
 Proof.
   rewrite /Timeless=> HQ. rewrite later_false_em.
   apply or_mono, impl_intro_l; first done.
+  rewrite impl_curry -(comm bi_and P) -impl_curry impl_elim_r.
   rewrite -{2}(löb Q). apply impl_intro_l.
   rewrite HQ /bi_except_0 !and_or_r. apply or_elim; last auto.
-  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
+  by rewrite impl_elim_r.
 Qed.
 Global Instance sep_timeless P Q: Timeless P → Timeless Q → Timeless (P ∗ Q).
 Proof.
diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index c2c3ad9abd067483b83602e15071ba534f4c6ea5..053551191741fa9e09f90d1c8e2df864b2ac29ad 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -3,9 +3,9 @@ From iris.bi Require Import interface derived_laws_later big_op.
 From iris.bi Require Import plainly updates internal_eq.
 From iris.prelude Require Import options.
 
-(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
-    primitive projections for the bi-records makes the proofmode faster.
-*)
+(* We enable primitive projections in this file to improve the performance of
+the Iris proofmode: primitive projections for the bi-records makes the proofmode
+faster. *)
 Local Set Primitive Projections.
 
 (* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
@@ -26,13 +26,6 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
   bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) (embed (A:=PROP1) (B:=PROP2));
   bi_embed_mixin_emp_valid_inj (P : PROP1) :
     (⊢@{PROP2} ⎡P⎤) → ⊢ P;
-  (** The following axiom expresses that the embedding is injective in the OFE
-  sense. Instead of this axiom being expressed in terms of [siProp] or
-  externally (i.e., as [Inj (dist n) (dist n) embed]), it is expressed using the
-  internal equality of _any other_ BI [PROP']. This is more general, as we do
-  not have any machinary to embed [siProp] into a BI with internal equality. *)
-  bi_embed_mixin_interal_inj {PROP' : bi} `{!BiInternalEq PROP'} (P Q : PROP1) :
-    ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q);
   bi_embed_mixin_emp_2 : emp ⊢@{PROP2} ⎡emp⎤;
   bi_embed_mixin_impl_2 (P Q : PROP1) :
     (⎡P⎤ → ⎡Q⎤) ⊢@{PROP2} ⎡P → Q⎤;
@@ -66,12 +59,6 @@ Class BiEmbedLater (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
 Global Hint Mode BiEmbedLater ! - - : typeclass_instances.
 Global Hint Mode BiEmbedLater - ! - : typeclass_instances.
 
-Class BiEmbedInternalEq (PROP1 PROP2 : bi)
-    `{!BiEmbed PROP1 PROP2, !BiInternalEq PROP1, !BiInternalEq PROP2} :=
-  embed_internal_eq_1 (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y.
-Global Hint Mode BiEmbedInternalEq ! - - - - : typeclass_instances.
-Global Hint Mode BiEmbedInternalEq - ! - - - : typeclass_instances.
-
 Class BiEmbedBUpd (PROP1 PROP2 : bi)
     `{!BiEmbed PROP1 PROP2, !BiBUpd PROP1, !BiBUpd PROP2} :=
   embed_bupd P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤.
@@ -84,11 +71,14 @@ Class BiEmbedFUpd (PROP1 PROP2 : bi)
 Global Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
 Global Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
 
-Class BiEmbedPlainly (PROP1 PROP2 : bi)
-    `{!BiEmbed PROP1 PROP2, !BiPlainly PROP1, !BiPlainly PROP2} :=
-  embed_plainly (P : PROP1) : ⎡■ P⎤ ⊣⊢@{PROP2} ■ ⎡P⎤.
-Global Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
-Global Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.
+Class BiEmbedSbi (PROP1 PROP2 : bi)
+    `{!BiEmbed PROP1 PROP2, !Sbi PROP1, !Sbi PROP2} := {
+  embed_si_emp_valid (P : PROP1) :
+    <si_emp_valid> ⎡ P ⎤ ⊣⊢@{siPropI} <si_emp_valid> P;
+  embed_si_pure_1 Pi : ⎡ <si_pure> Pi ⎤ ⊢@{PROP2} <si_pure> Pi;
+}.
+Global Hint Mode BiEmbedSbi - ! - - - : typeclass_instances.
+Global Hint Mode BiEmbedSbi ! - - - - : typeclass_instances.
 
 Section embed_laws.
   Context {PROP1 PROP2 : bi} `{!BiEmbed PROP1 PROP2}.
@@ -102,9 +92,6 @@ Section embed_laws.
   Proof. eapply bi_embed_mixin_mono, bi_embed_mixin. Qed.
   Lemma embed_emp_valid_inj P : (⊢@{PROP2} ⎡P⎤) → ⊢ P.
   Proof. eapply bi_embed_mixin_emp_valid_inj, bi_embed_mixin. Qed.
-  Lemma embed_interal_inj `{!BiInternalEq PROP'} (P Q : PROP1) :
-    ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q).
-  Proof. eapply bi_embed_mixin_interal_inj, bi_embed_mixin. Qed.
   Lemma embed_emp_2 : emp ⊢ ⎡emp⎤.
   Proof. eapply bi_embed_mixin_emp_2, bi_embed_mixin. Qed.
   Lemma embed_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤.
@@ -123,8 +110,8 @@ End embed_laws.
 
 Section embed.
   Context {PROP1 PROP2 : bi} `{!BiEmbed PROP1 PROP2}.
-  Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
-  Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
+  Notation embed := (embed (A:=bi_car PROP1) (B:=bi_car PROP2)).
+  Notation "⎡ P ⎤" := (embed P) : bi_scope.
   Implicit Types P Q R : PROP1.
 
   Global Instance embed_proper : Proper ((≡) ==> (≡)) embed.
@@ -293,27 +280,34 @@ Section embed.
     Qed.
   End later.
 
-  Section internal_eq.
-    Context `{!BiInternalEq PROP1, !BiInternalEq PROP2, !BiEmbedInternalEq PROP1 PROP2}.
+  Section sbi.
+    Context `{!Sbi PROP1, !Sbi PROP2, !BiEmbedSbi PROP1 PROP2}.
 
-    Lemma embed_internal_eq (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
+    Lemma embed_si_pure Pi : ⎡<si_pure> Pi⎤ ⊣⊢ <si_pure> Pi.
+    Proof.
+      apply (anti_symm _); [apply embed_si_pure_1|].
+      rewrite -(si_pure_si_emp_valid_elim ⎡ _ ⎤).
+      by rewrite embed_si_emp_valid si_emp_valid_si_pure.
+    Qed.
+
+    Lemma embed_interal_inj P Q : ⎡P⎤ ≡ ⎡Q⎤ ⊢@{siProp} P ≡ Q.
     Proof.
-      apply bi.equiv_entails; split; [apply embed_internal_eq_1|].
-      etrans; [apply (internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|].
-      rewrite -(internal_eq_refl True%I) embed_pure.
-      eapply bi.impl_elim; [done|]. apply bi.True_intro.
+      intros. rewrite !prop_ext. rewrite /bi_wand_iff !si_emp_valid_and.
+      by rewrite -!embed_wand !embed_si_emp_valid.
     Qed.
-  End internal_eq.
 
-  Section plainly.
-    Context `{!BiPlainly PROP1, !BiPlainly PROP2, !BiEmbedPlainly PROP1 PROP2}.
+    Lemma embed_internal_eq (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
+    Proof. apply embed_si_pure. Qed.
+
+    Lemma embed_plainly P : ⎡■ P⎤ ⊣⊢ ■ ⎡P⎤.
+    Proof. by rewrite /plainly embed_si_pure embed_si_emp_valid. Qed.
 
     Lemma embed_plainly_if p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
     Proof. destruct p; simpl; auto using embed_plainly. Qed.
 
     Lemma embed_plain (P : PROP1) : Plain P → Plain (PROP:=PROP2) ⎡P⎤.
     Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly. Qed.
-  End plainly.
+  End sbi.
 End embed.
 
 (* Not defined using an ordinary [Instance] because the default
@@ -339,7 +333,6 @@ Section embed_embed.
     - solve_proper.
     - solve_proper.
     - intros P. by rewrite !embed_emp_valid.
-    - intros PROP' ? P Q. by rewrite !embed_interal_inj.
     - by rewrite -!embed_emp_2.
     - intros P Q. by rewrite -!embed_impl.
     - intros A Φ. by rewrite -!embed_forall.
@@ -362,11 +355,14 @@ Section embed_embed.
     BiEmbedLater PROP1 PROP2 → BiEmbedLater PROP2 PROP3 →
     BiEmbedLater PROP1 PROP3.
   Proof. intros ?? P. by rewrite !embed_embed_alt !embed_later. Qed.
-  Lemma embed_embed_internal_eq
-      `{!BiInternalEq PROP1, !BiInternalEq PROP2, !BiInternalEq PROP3} :
-    BiEmbedInternalEq PROP1 PROP2 → BiEmbedInternalEq PROP2 PROP3 →
-    BiEmbedInternalEq PROP1 PROP3.
-  Proof. intros ?? A x y. by rewrite !embed_embed_alt !embed_internal_eq. Qed.
+  Lemma embed_embed_sbi `{!Sbi PROP1, !Sbi PROP2, !Sbi PROP3} :
+    BiEmbedSbi PROP1 PROP2 → BiEmbedSbi PROP2 PROP3 →
+    BiEmbedSbi PROP1 PROP3.
+  Proof.
+    intros ??; split.
+    - intros P. by rewrite embed_embed_alt !embed_si_emp_valid.
+    - intros Pi. by rewrite embed_embed_alt !embed_si_pure.
+  Qed.
   Lemma embed_embed_bupd `{!BiBUpd PROP1, !BiBUpd PROP2, !BiBUpd PROP3} :
     BiEmbedBUpd PROP1 PROP2 → BiEmbedBUpd PROP2 PROP3 →
     BiEmbedBUpd PROP1 PROP3.
@@ -375,9 +371,4 @@ Section embed_embed.
     BiEmbedFUpd PROP1 PROP2 → BiEmbedFUpd PROP2 PROP3 →
     BiEmbedFUpd PROP1 PROP3.
   Proof. intros ?? E1 E2 P. by rewrite !embed_embed_alt !embed_fupd. Qed.
-  Lemma embed_embed_plainly
-      `{!BiPlainly PROP1, !BiPlainly PROP2, !BiPlainly PROP3} :
-    BiEmbedPlainly PROP1 PROP2 → BiEmbedPlainly PROP2 PROP3 →
-    BiEmbedPlainly PROP1 PROP3.
-  Proof. intros ?? P. by rewrite !embed_embed_alt !embed_plainly. Qed.
 End embed_embed.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 6a7eca83d87be6eaeb683abc65814efb5a6cb835..a13a0793b851ff428ec563c0b35d4447f5b4eab7 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -1,131 +1,125 @@
-From iris.bi Require Import derived_laws_later big_op.
-From iris.prelude Require Import options.
 From iris.algebra Require Import excl csum.
-Import interface.bi derived_laws.bi derived_laws_later.bi.
-
-(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
-    primitive projections for the bi-records makes the proofmode faster.
-*)
-Local Set Primitive Projections.
-
-(** This file defines a type class for BIs with a notion of internal equality.
-Internal equality is not part of the [bi] canonical structure as [internal_eq]
-can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
-[▷ (x ≡ y) ⊢ Next x ≡ Next y] if the BI is step-indexed. *)
-Class InternalEq (PROP : Type) :=
-  internal_eq : ∀ {A : ofe}, A → A → PROP.
-Global Arguments internal_eq {_ _ _} _ _ : simpl never.
-Global Hint Mode InternalEq ! : typeclass_instances.
-Global Instance: Params (@internal_eq) 3 := {}.
+From iris.bi Require Export sbi.
+From iris.bi Require Import derived_laws_later.
+From iris.prelude Require Import options.
+
+Definition internal_eq `{!Sbi PROP} {A : ofe} (a b : A) : PROP :=
+  <si_pure> siProp_internal_eq a b.
+Global Arguments internal_eq : simpl never.
 Global Typeclasses Opaque internal_eq.
+Global Instance: Params (@internal_eq) 3 := {}.
 
 Infix "≡" := internal_eq : bi_scope.
 Infix "≡@{ A }" := (internal_eq (A := A)) (only parsing) : bi_scope.
-
 Notation "( X ≡.)" := (internal_eq X) (only parsing) : bi_scope.
 Notation "(.≡ X )" := (λ Y, Y ≡ X)%I (only parsing) : bi_scope.
 Notation "(≡@{ A } )" := (internal_eq (A:=A)) (only parsing) : bi_scope.
 
-(* Mixins allow us to create instances easily without having to use Program *)
-Record BiInternalEqMixin (PROP : bi) `(!InternalEq PROP) := {
-  bi_internal_eq_mixin_internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq PROP _ A);
-  bi_internal_eq_mixin_internal_eq_refl {A : ofe} (P : PROP) (a : A) : P ⊢ a ≡ a;
-  bi_internal_eq_mixin_internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
-    NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b;
-  bi_internal_eq_mixin_fun_extI {A} {B : A → ofe} (f g : discrete_fun B) :
-    (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g;
-  bi_internal_eq_mixin_sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sig P) :
-    `x ≡ `y ⊢@{PROP} x ≡ y;
-  bi_internal_eq_mixin_discrete_eq_1 {A : ofe} (a b : A) :
-    Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ b⌝;
-  bi_internal_eq_mixin_later_equivI_1 {A : ofe} (x y : A) :
-    Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y);
-  bi_internal_eq_mixin_later_equivI_2 {A : ofe} (x y : A) :
-    ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y;
-}.
-
-Class BiInternalEq (PROP : bi) := {
-  bi_internal_eq_internal_eq :> InternalEq PROP;
-  bi_internal_eq_mixin : BiInternalEqMixin PROP bi_internal_eq_internal_eq;
-}.
-Global Hint Mode BiInternalEq ! : typeclass_instances.
-Global Arguments bi_internal_eq_internal_eq : simpl never.
-
-Section internal_eq_laws.
-  Context {PROP : bi} `{!BiInternalEq PROP}.
-  Implicit Types P Q : PROP.
-
-  Global Instance internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq PROP _ A).
-  Proof. eapply bi_internal_eq_mixin_internal_eq_ne, (bi_internal_eq_mixin). Qed.
-
-  Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ a ≡ a.
-  Proof. eapply bi_internal_eq_mixin_internal_eq_refl, bi_internal_eq_mixin. Qed.
-  Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
-    NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
-  Proof. eapply bi_internal_eq_mixin_internal_eq_rewrite, bi_internal_eq_mixin. Qed.
-
-  Lemma fun_extI {A} {B : A → ofe} (f g : discrete_fun B) :
-    (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
-  Proof. eapply bi_internal_eq_mixin_fun_extI, bi_internal_eq_mixin. Qed.
-  Lemma sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sig P) :
-    `x ≡ `y ⊢@{PROP} x ≡ y.
-  Proof. eapply bi_internal_eq_mixin_sig_equivI_1, bi_internal_eq_mixin. Qed.
-  Lemma discrete_eq_1 {A : ofe} (a b : A) :
-    Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ b⌝.
-  Proof. eapply bi_internal_eq_mixin_discrete_eq_1, bi_internal_eq_mixin. Qed.
+(** A version of the constructor of [SbiPropExtMixin] stated using [≡@{siProp}]
+instead of [siProp_internal_eq]. *)
+Lemma sbi_prop_ext_mixin_make {PROP : bi} (empv : SiEmpValid PROP) :
+  (∀ P Q : PROP, <si_emp_valid> (P ∗-∗ Q) ⊢@{siPropI} P ≡ Q) →
+  SbiPropExtMixin PROP empv.
+Proof. done. Qed.
 
-  Lemma later_equivI_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
-  Proof. eapply bi_internal_eq_mixin_later_equivI_1, bi_internal_eq_mixin. Qed.
-  Lemma later_equivI_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
-  Proof. eapply bi_internal_eq_mixin_later_equivI_2, bi_internal_eq_mixin. Qed.
-End internal_eq_laws.
+Section internal_eq.
+  Context `{!Sbi PROP}.
+  Implicit Types P Q : PROP.
 
-(* Derived laws *)
-Section internal_eq_derived.
-  Context {PROP : bi} `{!BiInternalEq PROP}.
-  Implicit Types P : PROP.
+  Local Hint Resolve bi.or_elim bi.or_intro_l' bi.or_intro_r' : core.
+  Local Hint Resolve bi.True_intro bi.False_elim : core.
+  Local Hint Resolve bi.and_elim_l' bi.and_elim_r' bi.and_intro : core.
+  Local Hint Resolve bi.forall_intro : core.
+  Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
 
   (* Force implicit argument PROP *)
   Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
   Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
 
-  Global Instance internal_eq_proper (A : ofe) :
-    Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A) := ne_proper_2 _.
+  Lemma prop_ext_2 P Q : <si_emp_valid> (P ∗-∗ Q) ⊢@{siPropI} P ≡ Q.
+  Proof. apply sbi_mixin_prop_ext_2, sbi_sbi_prop_ext_mixin. Qed.
 
-  (* Equality *)
-  Local Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
-  Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
-  Local Hint Resolve internal_eq_refl : core.
-  Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
+  Global Instance internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq PROP _ A).
+  Proof.
+    intros n x x' ? y y' ?. by apply si_pure_ne, siProp_primitive.internal_eq_ne.
+  Qed.
+  Global Instance internal_eq_proper (A : ofe) :
+    Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A).
+  Proof. apply (ne_proper_2 _). Qed.
 
+  Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ a ≡ a.
+  Proof.
+    rewrite (bi.True_intro P) -si_pure_pure.
+    apply si_pure_mono, siProp_primitive.internal_eq_refl.
+  Qed.
   Lemma equiv_internal_eq {A : ofe} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
-  Proof. intros ->. auto. Qed.
-  Lemma internal_eq_rewrite' {A : ofe} a b (Ψ : A → PROP) P
-    {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+  Proof. intros ->. apply internal_eq_refl. Qed.
+  Lemma pure_internal_eq {A : ofe} (x y : A) : ⌜x ≡ y⌝ ⊢ x ≡ y.
+  Proof. apply bi.pure_elim'=> ->. apply internal_eq_refl. Qed.
+
+  Local Hint Resolve equiv_internal_eq : core.
+
+  Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
+    NonExpansive Ψ →
+    internal_eq a b ⊢ Ψ a → Ψ b.
+  Proof.
+    intros. (* [True -∗] makes [True -∗ Ψ a → Ψ a'] persistent, needed for
+    [si_pure_si_emp_valid_elim] *)
+    pose (Φ a' := (<si_emp_valid> (True -∗ Ψ a → Ψ a'))%I).
+    assert (⊢ Φ a) as HΦa.
+    { apply si_emp_valid_emp_valid, bi.wand_intro_l.
+      by rewrite right_id -bi.entails_impl_True. }
+    trans (<si_pure> (Φ a → Φ b) : PROP)%I.
+    - apply si_pure_mono. apply siProp_primitive.internal_eq_rewrite.
+      solve_proper.
+    - unfold bi_emp_valid in HΦa. rewrite -HΦa left_id.
+      rewrite /Φ si_pure_si_emp_valid_elim.
+      by rewrite -(bi.True_intro emp)%I left_id.
+  Qed.
+  Lemma internal_eq_rewrite' {A : ofe} a b (Ψ : A → PROP) P :
+    NonExpansive Ψ →
+    (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
   Proof.
-    intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
-    apply impl_elim_l'. by apply internal_eq_rewrite.
+    intros HΨ Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
+    apply bi.impl_elim_l'. by apply internal_eq_rewrite.
   Qed.
 
-  Lemma internal_eq_sym {A : ofe} (a b : A) : a ≡ b ⊢ b ≡ a.
+  Lemma internal_eq_sym {A : ofe} (a b : A) : a ≡ b ⊢@{PROP} b ≡ a.
   Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed.
-  Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
-  Proof. apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using iff_refl. Qed.
 
   Lemma f_equivI {A B : ofe} (f : A → B) `{!NonExpansive f} x y :
     x ≡ y ⊢ f x ≡ f y.
   Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed.
-  Lemma f_equivI_contractive {A B : ofe} (f : A → B) `{Hf : !Contractive f} x y :
-    ▷ (x ≡ y) ⊢ f x ≡ f y.
+
+  (** Equality of data types *)
+  Lemma discrete_eq_1 {A : ofe} (a b : A) :
+    TCOr (Discrete a) (Discrete b) → a ≡ b ⊢@{PROP} ⌜a ≡ b⌝.
   Proof.
-    rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]]. rewrite !Hfg.
-    by apply f_equivI.
+    intros. rewrite -si_pure_pure. destruct select (TCOr _ _).
+    - by apply si_pure_mono, siProp_primitive.discrete_eq_1.
+    - rewrite internal_eq_sym (symmetry_iff (≡)).
+      by apply si_pure_mono, siProp_primitive.discrete_eq_1.
   Qed.
+  Lemma discrete_eq {A : ofe} (a b : A) :
+    TCOr (Discrete a) (Discrete b) → a ≡ b ⊣⊢ ⌜a ≡ b⌝.
+  Proof.
+    intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
+  Qed.
+
+  Lemma fun_extI {A} {B : A → ofe} (f g : discrete_fun B) :
+    (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
+  Proof.
+    rewrite /internal_eq -si_pure_forall.
+    by apply si_pure_mono, siProp_primitive.fun_extI.
+  Qed.
+  Lemma sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sig P) :
+    `x ≡ `y ⊢@{PROP} x ≡ y.
+  Proof. by apply si_pure_mono, siProp_primitive.sig_equivI_1. Qed.
 
   Lemma prod_equivI {A B : ofe} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
   Proof.
     apply (anti_symm _).
-    - apply and_intro; apply f_equivI; apply _.
+    - apply bi.and_intro; apply f_equivI; apply _.
     - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y).
       apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto.
       apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto.
@@ -214,17 +208,18 @@ Section internal_eq_derived.
     Proof.
       apply (anti_symm _).
       - apply (internal_eq_rewrite' x y (λ y,
-                 ∃ eq : projT1 x = projT1 y,
-                   rew eq in projT2 x ≡ projT2 y))%I;
-            [| done | exact: (exist_intro' _ _ eq_refl) ].
-        move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
-        apply exist_ne => ?. by rewrite Hab.
-      - apply exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
-        apply f_equivI, _.
+                 ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y))%I.
+        + move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
+          apply bi.exist_ne => ?. by rewrite Hab.
+        + done.
+        + rewrite -(bi.exist_intro eq_refl) /=. auto.
+      - apply bi.exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
+        apply (f_equivI _).
     Qed.
   End sigT_equivI.
 
-  Lemma discrete_fun_equivI {A} {B : A → ofe} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+  Lemma discrete_fun_equivI {A} {B : A → ofe} (f g : discrete_fun B) :
+    f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
   Proof.
     apply (anti_symm _); auto using fun_extI.
     apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
@@ -243,26 +238,11 @@ Section internal_eq_derived.
       by rewrite -{2}[f]Hh -{2}[g]Hh -f_equivI -sig_equivI.
   Qed.
 
-  Lemma pure_internal_eq {A : ofe} (x y : A) : ⌜x ≡ y⌝ ⊢ x ≡ y.
-  Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
-  Lemma discrete_eq {A : ofe} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝.
-  Proof.
-    intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
-  Qed.
-
+  (** Modalities *)
   Lemma absorbingly_internal_eq {A : ofe} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
-  Proof.
-    apply (anti_symm _), absorbingly_intro.
-    apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto.
-    apply wand_intro_l, internal_eq_refl.
-  Qed.
+  Proof. apply absorbingly_si_pure. Qed.
   Lemma persistently_internal_eq {A : ofe} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
-  Proof.
-    apply (anti_symm (⊢)).
-    { by rewrite persistently_into_absorbingly absorbingly_internal_eq. }
-    apply (internal_eq_rewrite' a b (λ b, <pers> (a ≡ b))%I); auto.
-    rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
-  Qed.
+  Proof. apply persistently_si_pure. Qed.
 
   Global Instance internal_eq_absorbing {A : ofe} (x y : A) :
     Absorbing (PROP:=PROP) (x ≡ y).
@@ -271,26 +251,122 @@ Section internal_eq_derived.
     Persistent (PROP:=PROP) (a ≡ b).
   Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
 
-  (* Equality under a later. *)
-  Lemma internal_eq_rewrite_contractive {A : ofe} a b (Ψ : A → PROP)
-    {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
+  (** Equality under a later. *)
+  Lemma later_equivI_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
   Proof.
-    rewrite f_equivI_contractive. apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
+    rewrite /internal_eq -si_pure_later.
+    by apply si_pure_mono, siProp_primitive.later_equivI_1.
   Qed.
-  Lemma internal_eq_rewrite_contractive' {A : ofe} a b (Ψ : A → PROP) P
-    {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+  Lemma later_equivI_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
   Proof.
-    rewrite later_equivI_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
-    by apply internal_eq_rewrite'.
+    rewrite /internal_eq -si_pure_later.
+    by apply si_pure_mono, siProp_primitive.later_equivI_2.
   Qed.
-
   Lemma later_equivI {A : ofe} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
   Proof. apply (anti_symm _); auto using later_equivI_1, later_equivI_2. Qed.
-  Lemma later_equivI_prop_2 `{!Contractive (bi_later (PROP:=PROP))} P Q :
-    ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
-  Proof. apply (f_equivI_contractive _). Qed.
+
+  Lemma f_equivI_contractive {A B : ofe} (f : A → B) `{Hf : !Contractive f} x y :
+    ▷ (x ≡ y) ⊢ f x ≡ f y.
+  Proof.
+    rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]].
+    rewrite !Hfg. by apply f_equivI.
+  Qed.
+
+  Lemma internal_eq_rewrite_contractive {A : ofe} a b (Ψ : A → PROP) :
+    Contractive Ψ →
+    ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
+  Proof.
+    intros. rewrite f_equivI_contractive.
+    apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
+  Qed.
+  Lemma internal_eq_rewrite_contractive' {A : ofe} a b (Ψ : A → PROP) P :
+    Contractive Ψ →
+    (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+  Proof.
+    intros HΨ Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
+    apply bi.impl_elim_l'. by apply internal_eq_rewrite_contractive.
+  Qed.
 
   Global Instance eq_timeless {A : ofe} (a b : A) :
-    Discrete a → Timeless (PROP:=PROP) (a ≡ b).
+    TCOr (Discrete a) (Discrete b) → Timeless (PROP:=PROP) (a ≡ b).
   Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
-End internal_eq_derived.
+
+  (** Equality of propositions *)
+  Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
+  Proof.
+    apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using bi.iff_refl.
+  Qed.
+  Lemma affinely_internal_eq_wand_iff P Q : <affine> (P ≡ Q) ⊢ P ∗-∗ Q.
+  Proof.
+    apply (internal_eq_rewrite' P Q (λ Q, P ∗-∗ Q))%I; auto.
+    - by rewrite bi.affinely_elim.
+    - rewrite bi.affinely_elim_emp. apply bi.wand_iff_refl.
+  Qed.
+  Lemma internal_eq_wand_iff P Q : P ≡ Q ⊢ <absorb> (P ∗-∗ Q).
+  Proof.
+    rewrite -(bi.persistent_absorbingly_affinely (P ≡ Q)).
+    by rewrite affinely_internal_eq_wand_iff.
+  Qed.
+
+  Lemma si_pure_internal_eq {A : ofe} (x y : A) : <si_pure> (x ≡ y) ⊣⊢ x ≡ y.
+  Proof. done. Qed.
+
+  Lemma prop_ext P Q : P ≡ Q ⊣⊢@{siPropI} <si_emp_valid> (P ∗-∗ Q).
+  Proof.
+    apply (anti_symm _); [|apply prop_ext_2].
+    rewrite -(@si_pure_entails PROP) si_pure_internal_eq.
+    apply (internal_eq_rewrite' P Q
+      (λ Q, <si_pure> <si_emp_valid> (P ∗-∗ Q)))%I; auto.
+    rewrite -bi.wand_iff_refl si_emp_valid_emp si_pure_pure. auto.
+  Qed.
+
+  Lemma later_equivI_prop_2 P Q : ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
+  Proof.
+    rewrite -!si_pure_internal_eq -si_pure_later !prop_ext.
+    by rewrite -si_emp_valid_later bi.later_wand_iff.
+  Qed.
+
+  Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{PROP} x ≡ y) → x ≡ y.
+  Proof.
+    intros ?%si_pure_emp_valid. by apply siProp_primitive.internal_eq_soundness.
+  Qed.
+
+  (** Derive [NonExpansive]/[Contractive] from an internal statement *)
+  Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
+    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
+  Proof. rewrite si_pure_entails. apply siProp_primitive.internal_eq_entails. Qed.
+
+  Lemma ne_internal_eq {A B : ofe} (f : A → B) :
+    NonExpansive f ↔ ∀ x1 x2, x1 ≡ x2 ⊢ f x1 ≡ f x2.
+  Proof.
+    split; [apply f_equivI|]. intros Hf n x1 x2. by apply internal_eq_entails.
+  Qed.
+
+  Lemma ne_2_internal_eq {A B C : ofe} (f : A → B → C) :
+    NonExpansive2 f ↔ ∀ x1 x2 y1 y2, x1 ≡ x2 ∧ y1 ≡ y2 ⊢ f x1 y1 ≡ f x2 y2.
+  Proof.
+    split.
+    - intros Hf x1 x2 y1 y2.
+      change ((x1,y1).1 ≡ (x2,y2).1 ∧ (x1,y1).2 ≡ (x2,y2).2
+        ⊢ uncurry f (x1,y1) ≡ uncurry f (x2,y2)).
+      rewrite -prod_equivI. apply ne_internal_eq. solve_proper.
+    - intros Hf n x1 x2 Hx y1 y2 Hy.
+      change (uncurry f (x1,y1) ≡{n}≡ uncurry f (x2,y2)).
+      apply ne_internal_eq; [|done].
+      intros [??] [??]. rewrite prod_equivI. apply Hf.
+  Qed.
+
+  Lemma contractive_internal_eq {A B : ofe} (f : A → B) :
+    Contractive f ↔ ∀ x1 x2, ▷ (x1 ≡ x2) ⊢ f x1 ≡ f x2.
+  Proof.
+    split; [apply f_equivI_contractive|].
+    intros Hf n x1 x2 Hx. specialize (Hf x1 x2).
+    rewrite -later_equivI internal_eq_entails in Hf. apply Hf. by f_contractive.
+  Qed.
+
+  Global Instance sbi_later_contractive : BiLaterContractive PROP.
+  Proof using Type*.
+    rewrite /BiLaterContractive.
+    apply contractive_internal_eq, later_equivI_prop_2.
+  Qed.
+End internal_eq.
diff --git a/iris/bi/lib/cmra.v b/iris/bi/lib/cmra.v
index f3a8b9a20f46e2d9f19823c2242b48da1a74daed..cbab9ad5b62c36f32f4a1fc8bd1c9a640af4a682 100644
--- a/iris/bi/lib/cmra.v
+++ b/iris/bi/lib/cmra.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 (** Derived [≼] connective on [cmra] elements. This can be defined on
     any [bi] that has internal equality [≡]. It corresponds to the
     step-indexed [≼{n}] connective in the [uPred] model. *)
-Definition internal_included `{!BiInternalEq PROP} {A : cmra} (a b : A) : PROP :=
+Definition internal_included `{!Sbi PROP} {A : cmra} (a b : A) : PROP :=
   ∃ c, b ≡ a ⋅ c.
 Global Arguments internal_included {_ _ _} _ _ : simpl never.
 Global Instance: Params (@internal_included) 3 := {}.
@@ -15,7 +15,7 @@ Global Typeclasses Opaque internal_included.
 Infix "≼" := internal_included : bi_scope.
 
 Section internal_included_laws.
-  Context `{!BiInternalEq PROP}.
+  Context `{!Sbi PROP}.
   Implicit Type A B : cmra.
 
   (* Force implicit argument PROP *)
@@ -149,4 +149,4 @@ Section internal_included_laws.
     + iIntros "[%z Hz]". iRewrite "Hz". by rewrite assoc agree_idemp.
     + iIntros "H". by iExists _.
   Qed.
-End internal_included_laws.
\ No newline at end of file
+End internal_included_laws.
diff --git a/iris/bi/lib/core.v b/iris/bi/lib/core.v
index 8ff8e5fda4c2714dcda96a6d632388702b5aec86..63130d239ccd62eded48e738673b222dc4a1a0ad 100644
--- a/iris/bi/lib/core.v
+++ b/iris/bi/lib/core.v
@@ -6,7 +6,7 @@ Import bi.
 (** The "core" of an assertion is its maximal persistent part,
     i.e. the conjunction of all persistent assertions that are weaker
     than P (as in, implied by P). *)
-Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP :=
+Definition coreP `{!Sbi PROP} (P : PROP) : PROP :=
   (* TODO: Looks like we want notation for affinely-plainly; that lets us avoid
   using conjunction/implication here. *)
   ∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q.
@@ -14,7 +14,7 @@ Global Instance: Params (@coreP) 1 := {}.
 Global Typeclasses Opaque coreP.
 
 Section core.
-  Context {PROP : bi} `{!BiPlainly PROP}.
+  Context `{!Sbi PROP}.
   Implicit Types P Q : PROP.
 
   Lemma coreP_intro P : P -∗ coreP P.
@@ -27,7 +27,7 @@ Section core.
   Qed.
 
   Global Instance coreP_persistent
-      `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P :
+      `{!BiPersistentlyForall PROP, !BiPersistentlyImplSiPure PROP} P :
     Persistent (coreP P).
   Proof.
     rewrite /coreP /Persistent. iIntros "HC" (Q).
@@ -65,7 +65,7 @@ Section core.
     [<affine>] modality makes it stronger since it appears in the LHS of the
     [⊢] in the premise. As a user, you have to prove [<affine> coreP P ⊢ Q],
     which is weaker than [coreP P ⊢ Q]. *)
-  Lemma coreP_entails `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P Q :
+  Lemma coreP_entails `{!BiPersistentlyForall PROP, !BiPersistentlyImplSiPure PROP} P Q :
     (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q).
   Proof.
     split.
@@ -74,7 +74,7 @@ Section core.
     - iIntros (->) "HcQ". by iDestruct (coreP_elim with "HcQ") as "#HQ".
   Qed.
   (** A more convenient variant of the above lemma for affine [P]. *)
-  Lemma coreP_entails' `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP}
+  Lemma coreP_entails' `{!BiPersistentlyForall PROP, !BiPersistentlyImplSiPure PROP}
       P Q `{!Affine P} :
     (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
   Proof.
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index be4223c7271ebb1bcec801d8af91d9e378b7bac6..920ada33e7a11ee28f703481a5cea0cce19e7b07 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type*".
 
 (** * Definitions *)
 Section definitions.
-  Context {PROP : bi} `{!BiInternalEq PROP}.
+  Context `{!Sbi PROP}.
   Context {A : ofe}.
 
   Local Definition bi_rtc_pre (R : A → A → PROP)
@@ -42,7 +42,7 @@ Section definitions.
   Global Instance: Params (@bi_nsteps) 5 := {}.
 End definitions.
 
-Local Instance bi_rtc_pre_mono {PROP : bi} `{!BiInternalEq PROP}
+Local Instance bi_rtc_pre_mono {PROP : bi} `{!Sbi PROP}
     {A : ofe} (R : A → A → PROP) `{!NonExpansive2 R} (x : A) :
   BiMonoPred (bi_rtc_pre R x).
 Proof.
@@ -54,18 +54,18 @@ Proof.
   iDestruct ("H" with "Hrec") as "Hrec". eauto with iFrame.
 Qed.
 
-Global Instance bi_rtc_ne {PROP : bi} `{!BiInternalEq PROP} {A : ofe} (R : A → A → PROP) :
+Global Instance bi_rtc_ne {PROP : bi} `{!Sbi PROP} {A : ofe} (R : A → A → PROP) :
   NonExpansive2 (bi_rtc R).
 Proof.
   intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_rtc Hx. f_equiv=> rec z.
   solve_proper.
 Qed.
 
-Global Instance bi_rtc_proper {PROP : bi} `{!BiInternalEq PROP} {A : ofe} (R : A → A → PROP)
+Global Instance bi_rtc_proper {PROP : bi} `{!Sbi PROP} {A : ofe} (R : A → A → PROP)
   : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
 Proof. apply ne_proper_2. apply _. Qed.
 
-Local Instance bi_tc_pre_mono `{!BiInternalEq PROP}
+Local Instance bi_tc_pre_mono `{!Sbi PROP}
     {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
   BiMonoPred (bi_tc_pre R x).
 Proof.
@@ -77,7 +77,7 @@ Proof.
   iRight. iExists x'. iFrame "HR". by iApply "H".
 Qed.
 
-Global Instance bi_tc_ne `{!BiInternalEq PROP} {A : ofe}
+Global Instance bi_tc_ne `{!Sbi PROP} {A : ofe}
     (R : A → A → PROP) `{NonExpansive2 R} :
   NonExpansive2 (bi_tc R).
 Proof.
@@ -85,24 +85,24 @@ Proof.
   solve_proper.
 Qed.
 
-Global Instance bi_tc_proper `{!BiInternalEq PROP} {A : ofe}
+Global Instance bi_tc_proper `{!Sbi PROP} {A : ofe}
     (R : A → A → PROP) `{NonExpansive2 R}
   : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_tc R).
 Proof. apply ne_proper_2. apply _. Qed.
 
-Global Instance bi_nsteps_ne {PROP : bi} `{!BiInternalEq PROP}
+Global Instance bi_nsteps_ne {PROP : bi} `{!Sbi PROP}
     {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (n : nat) :
   NonExpansive2 (bi_nsteps R n).
 Proof. induction n; solve_proper. Qed.
 
-Global Instance bi_nsteps_proper {PROP : bi} `{!BiInternalEq PROP}
+Global Instance bi_nsteps_proper {PROP : bi} `{!Sbi PROP}
     {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (n : nat)
   : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_nsteps R n).
 Proof. apply ne_proper_2. apply _. Qed.
 
 (** * General theorems *)
 Section general.
-  Context {PROP : bi} `{!BiInternalEq PROP}.
+  Context `{!Sbi PROP}.
   Context {A : ofe}.
   Context (R : A → A → PROP) `{!NonExpansive2 R}.
 
@@ -396,7 +396,7 @@ Section general.
 End general.
 
 Section timeless.
-  Context {PROP : bi} `{!BiInternalEq PROP, !BiAffine PROP}.
+  Context `{!Sbi PROP, !Timeless (emp%I : PROP)}.
   Context `{!OfeDiscrete A}.
   Context (R : A → A → PROP) `{!NonExpansive2 R}.
 
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 956586906f448efea5aa41b32919c7ae371967cf..f029af9f75bd20a5bdf8f1a277c746f5d3a51786 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -250,16 +250,6 @@ Section monPred_defs.
   Local Definition monPred_later_unseal :
     monPred_later = _ := monPred_later_aux.(seal_eq).
 
-  Local Definition monPred_internal_eq_def `{!BiInternalEq PROP}
-    (A : ofe) (a b : A) : monPred := MonPred (λ _, a ≡ b)%I _.
-  Local Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def).
-  Proof. by eexists. Qed.
-  Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
-  Global Arguments monPred_internal_eq {_}.
-  Local Definition monPred_internal_eq_unseal `{!BiInternalEq PROP} :
-    @internal_eq _ monPred_internal_eq = monPred_internal_eq_def.
-  Proof. by rewrite -monPred_internal_eq_aux.(seal_eq). Qed.
-
   Local Program Definition monPred_bupd_def `{BiBUpd PROP}
     (P : monPred) : monPred := MonPred (λ i, |==> P i)%I _.
   Next Obligation. solve_proper. Qed.
@@ -282,15 +272,25 @@ Section monPred_defs.
     @fupd _ monPred_fupd = monPred_fupd_def.
   Proof. by rewrite -monPred_fupd_aux.(seal_eq). Qed.
 
-  Local Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
-    MonPred (λ _, ∀ i, ■ (P i))%I _.
-  Local Definition monPred_plainly_aux : seal (@monPred_plainly_def).
+  Local Definition monPred_si_pure_def `{Sbi PROP} (Pi : siProp) : monPred :=
+    MonPred (λ _, <si_pure> Pi)%I _.
+  Local Definition monPred_si_pure_aux : seal (@monPred_si_pure_def).
+  Proof. by eexists. Qed.
+  Definition monPred_si_pure := monPred_si_pure_aux.(unseal).
+  Global Arguments monPred_si_pure {_}.
+  Local Definition monPred_si_pure_unseal `{Sbi PROP} :
+    @si_pure _ monPred_si_pure = monPred_si_pure_def.
+  Proof. by rewrite -monPred_si_pure_aux.(seal_eq). Qed.
+
+  Local Definition monPred_si_emp_valid_def `{!Sbi PROP} P : siProp :=
+    <si_emp_valid> ∀ i, P i.
+  Local Definition monPred_si_emp_valid_aux : seal (@monPred_si_emp_valid_def).
   Proof. by eexists. Qed.
-  Definition monPred_plainly := monPred_plainly_aux.(unseal).
-  Global Arguments monPred_plainly {_}.
-  Local Definition monPred_plainly_unseal `{BiPlainly PROP} :
-    @plainly _ monPred_plainly = monPred_plainly_def.
-  Proof. by rewrite -monPred_plainly_aux.(seal_eq). Qed.
+  Definition monPred_si_emp_valid := monPred_si_emp_valid_aux.(unseal).
+  Global Arguments monPred_si_emp_valid {_}.
+  Local Definition monPred_si_emp_valid_unseal `{!Sbi PROP} :
+    @si_emp_valid _ monPred_si_emp_valid = monPred_si_emp_valid_def.
+  Proof. by rewrite -monPred_si_emp_valid_aux.(seal_eq). Qed.
 End monPred_defs.
 
 (** This is not the final collection of unsealing lemmas, below we redefine
@@ -450,10 +450,6 @@ Section instances.
     split; try apply _; rewrite /bi_emp_valid
       !(monPred_defs.monPred_embed_unseal, monPred_unseal_bi); try done.
     - move=> P /= [/(_ inhabitant) ?] //.
-    - intros PROP' ? P Q.
-      set (f P := @monPred_at I PROP P inhabitant).
-      assert (NonExpansive f) by solve_proper.
-      apply (f_equivI f).
     - intros P Q. split=> i /=.
       by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
     - intros P Q. split=> i /=.
@@ -462,25 +458,46 @@ Section instances.
   Global Instance monPred_bi_embed : BiEmbed PROP monPredI :=
     {| bi_embed_mixin := monPred_embedding_mixin |}.
 
-  Lemma monPred_internal_eq_mixin `{!BiInternalEq PROP} :
-    BiInternalEqMixin monPredI monPred_internal_eq.
+  Lemma monPred_sbi_mixin `{!Sbi PROP} :
+    SbiMixin monPredI monPred_si_pure monPred_si_emp_valid.
   Proof.
-    split;
-      rewrite !(monPred_defs.monPred_internal_eq_unseal, monPred_unseal_bi).
+    split; rewrite /Absorbing /bi_affinely /bi_absorbingly
+      !(monPred_defs.monPred_si_pure_unseal,
+        monPred_defs.monPred_si_emp_valid_unseal, monPred_unseal_bi)
+      /monPred_defs.monPred_si_emp_valid_def /=.
     - split=> i /=. solve_proper.
-    - intros A P a. split=> i /=. apply internal_eq_refl.
-    - intros A a b Ψ ?. split=> i /=.
-      setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro => ?.
-      erewrite (internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
-    - intros A1 A2 f g. split=> i /=. by apply fun_extI.
-    - intros A P x y. split=> i /=. by apply sig_equivI_1.
-    - intros A a b ?. split=> i /=. by apply discrete_eq_1.
-    - intros A x y. split=> i /=. by apply later_equivI_1.
-    - intros A x y. split=> i /=. by apply later_equivI_2.
+    - solve_proper.
+    - intros Pi Qi HPQ. split=> i /=. by rewrite HPQ.
+    - intros P Q [HPQ]. by setoid_rewrite HPQ.
+    - intros Pi Qi. split=> i /=. rewrite si_pure_impl.
+      by rewrite (bi.forall_elim i) bi.pure_True // left_id.
+    - intros A Φi. split=> i /=. apply si_pure_forall_2.
+    - intros Pi. split=> i /=. apply si_pure_later.
+    - intros Pi. split=> i /=. by rewrite bi.sep_elim_r.
+    - intros P. by rewrite -si_emp_valid_later_1 bi.later_forall.
+    - intros P. rewrite !si_emp_valid_forall. f_equiv=> i.
+      apply si_emp_valid_affinely_2.
+    - intros Pi. apply (anti_symm _).
+      + by rewrite (bi.forall_elim inhabitant) si_emp_valid_si_pure.
+      + rewrite si_emp_valid_forall. apply bi.forall_intro=> _.
+        by rewrite si_emp_valid_si_pure.
+    - intros P. split=> i /=. by rewrite si_pure_si_emp_valid (bi.forall_elim i).
+  Qed.
+  Lemma monPred_sbi_prop_ext_mixin `{!Sbi PROP} :
+    SbiPropExtMixin monPredI monPred_si_emp_valid.
+  Proof.
+    apply sbi_prop_ext_mixin_make=> P Q.
+    rewrite /bi_wand_iff
+      !(monPred_defs.monPred_si_emp_valid_unseal, monPred_unseal_bi)
+      /monPred_defs.monPred_si_emp_valid_def /=.
+    rewrite -{3}(sig_monPred_sig P) -{3}(sig_monPred_sig Q)
+      -f_equivI -sig_equivI !discrete_fun_equivI /=.
+    apply bi.forall_intro=> j. rewrite prop_ext.
+    by rewrite !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
   Qed.
-  Global Instance monPred_bi_internal_eq `{BiInternalEq PROP} :
-      BiInternalEq monPredI :=
-    {| bi_internal_eq_mixin := monPred_internal_eq_mixin |}.
+  Global Instance monPred_sbi `{!Sbi PROP} : Sbi monPredI :=
+    {| sbi_sbi_mixin := monPred_sbi_mixin;
+       sbi_sbi_prop_ext_mixin := monPred_sbi_prop_ext_mixin |}.
 
   Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
   Proof.
@@ -510,47 +527,21 @@ Section instances.
   Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredI :=
     {| bi_fupd_mixin := monPred_fupd_mixin |}.
 
-  Lemma monPred_plainly_mixin `{BiPlainly PROP} :
-    BiPlainlyMixin monPredI monPred_plainly.
-  Proof.
-    split; rewrite !(monPred_defs.monPred_plainly_unseal, monPred_unseal_bi).
-    - by (split=> ? /=; repeat f_equiv).
-    - intros P Q [?]. split=> i /=. by do 3 f_equiv.
-    - intros P. split=> i /=. by rewrite bi.forall_elim plainly_elim_persistently.
-    - intros P. split=> i /=. do 3 setoid_rewrite <-plainly_forall.
-      rewrite -plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
-    - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
-      rewrite plainly_forall. apply bi.forall_intro=> a. by rewrite !bi.forall_elim.
-    - intros P Q. split=> i /=.
-      setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
-      do 2 setoid_rewrite <-plainly_forall.
-      setoid_rewrite plainly_impl_plainly. f_equiv.
-      do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
-    - intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
-    - intros P Q. split=> i. apply bi.sep_elim_l, _.
-    - intros P. split=> i /=.
-      rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1.
-    - intros P. split=> i /=.
-      rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2.
-  Qed.
-  Global Instance monPred_bi_plainly `{BiPlainly PROP} : BiPlainly monPredI :=
-    {| bi_plainly_mixin := monPred_plainly_mixin |}.
-
   Local Lemma monPred_embed_unseal :
     embed = @monPred_defs.monPred_embed_def I PROP.
   Proof. by rewrite -monPred_defs.monPred_embed_unseal. Qed.
-  Local Lemma monPred_internal_eq_unseal `{!BiInternalEq PROP} :
-    @internal_eq _ _ = @monPred_defs.monPred_internal_eq_def I PROP _.
-  Proof. by rewrite -monPred_defs.monPred_internal_eq_unseal. Qed.
-  Local Lemma monPred_bupd_unseal `{BiBUpd PROP} :
+  Local Lemma monPred_bupd_unseal `{!BiBUpd PROP} :
     bupd = @monPred_defs.monPred_bupd_def I PROP _.
   Proof. by rewrite -monPred_defs.monPred_bupd_unseal. Qed.
-  Local Lemma monPred_fupd_unseal `{BiFUpd PROP} :
+  Local Lemma monPred_fupd_unseal `{!BiFUpd PROP} :
     fupd = @monPred_defs.monPred_fupd_def I PROP _.
   Proof. by rewrite -monPred_defs.monPred_fupd_unseal. Qed.
-  Local Lemma monPred_plainly_unseal `{BiPlainly PROP} :
-    plainly = @monPred_defs.monPred_plainly_def I PROP _.
-  Proof. by rewrite -monPred_defs.monPred_plainly_unseal. Qed.
+  Local Lemma monPred_si_pure_unseal `{!Sbi PROP} :
+    si_pure = @monPred_defs.monPred_si_pure_def I PROP _.
+  Proof. by rewrite -monPred_defs.monPred_si_pure_unseal. Qed.
+  Local Lemma monPred_si_emp_valid_unseal `{!Sbi PROP} :
+    si_emp_valid = @monPred_defs.monPred_si_emp_valid_def I PROP _.
+  Proof. by rewrite -monPred_defs.monPred_si_emp_valid_unseal. Qed.
 
   (** And finally the proper [unseal] tactic (which we also redefine outside
   of the section since Ltac definitions do not outlive a section). *)
@@ -558,8 +549,8 @@ Section instances.
     (monPred_unseal_bi,
     @monPred_defs.monPred_objectively_unseal,
     @monPred_defs.monPred_subjectively_unseal,
-    @monPred_embed_unseal, @monPred_internal_eq_unseal,
-    @monPred_bupd_unseal, @monPred_fupd_unseal, @monPred_plainly_unseal,
+    @monPred_embed_unseal, @monPred_bupd_unseal, @monPred_fupd_unseal,
+    @monPred_si_pure_unseal, @monPred_si_emp_valid_unseal,
     @monPred_defs.monPred_in_unseal).
   Ltac unseal := rewrite !monPred_unseal /=.
 
@@ -588,10 +579,6 @@ Section instances.
   Global Instance monPred_bi_embed_later : BiEmbedLater PROP monPredI.
   Proof. split; by unseal. Qed.
 
-  Global Instance monPred_bi_embed_internal_eq `{BiInternalEq PROP} :
-    BiEmbedInternalEq PROP monPredI.
-  Proof. split. by unseal. Qed.
-
   Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredI.
   Proof. intros E P. split=> i. unseal. apply bupd_fupd. Qed.
 
@@ -602,61 +589,38 @@ Section instances.
   Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
   Proof. split. by unseal. Qed.
 
-  Global Instance monPred_bi_persistently_impl_plainly
-       `{!BiPlainly PROP, !BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} :
-    BiPersistentlyImplPlainly monPredI.
+  Global Instance monPred_bi_persistently_impl_si_pure
+       `{!Sbi PROP, !@BiIndexBottom I bot,
+         !BiPersistentlyForall PROP, !BiPersistentlyImplSiPure PROP} :
+    BiPersistentlyImplSiPure monPredI.
   Proof.
     intros P Q. split=> i. unseal. setoid_rewrite bi.pure_impl_forall.
-    setoid_rewrite <-plainly_forall.
     do 2 setoid_rewrite bi.persistently_forall.
-    by setoid_rewrite persistently_impl_plainly.
+    by setoid_rewrite persistently_impl_si_pure.
   Qed.
 
-  Global Instance monPred_bi_prop_ext
-    `{!BiPlainly PROP, !BiInternalEq PROP, !BiPropExt PROP} : BiPropExt monPredI.
+  Global Instance monPred_bi_embed_sbi `{!Sbi PROP} : BiEmbedSbi PROP monPredI.
   Proof.
-    intros P Q. split=> i /=. rewrite /bi_wand_iff. unseal.
-    rewrite -{3}(sig_monPred_sig P) -{3}(sig_monPred_sig Q)
-      -f_equivI -sig_equivI !discrete_fun_equivI /=.
-    f_equiv=> j. rewrite prop_ext.
-    by rewrite !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
+    split; unseal; rewrite /monPred_defs.monPred_si_emp_valid_def /=; [|done].
+    intros P. apply (anti_symm _).
+    + by rewrite (bi.forall_elim inhabitant).
+    + rewrite si_emp_valid_forall. by apply bi.forall_intro.
   Qed.
 
-  Global Instance monPred_bi_plainly_exist `{!BiPlainly PROP, @BiIndexBottom I bot} :
-    BiPlainlyExist PROP → BiPlainlyExist monPredI.
-  Proof.
-    split=> ? /=. unseal. rewrite (bi.forall_elim bot) plainly_exist_1.
-    do 2 f_equiv. apply bi.forall_intro=> ?. by do 2 f_equiv.
-  Qed.
-
-  Global Instance monPred_bi_embed_plainly `{BiPlainly PROP} :
-    BiEmbedPlainly PROP monPredI.
-  Proof.
-    split=> i. unseal. apply (anti_symm _).
-    - by apply bi.forall_intro.
-    - by rewrite (bi.forall_elim inhabitant).
-  Qed.
-
-  Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} :
-    BiBUpdPlainly monPredI.
-  Proof.
-    intros P. split=> /= i. unseal. by rewrite bi.forall_elim bupd_plainly.
-  Qed.
+  Global Instance monPred_bi_bupd_sbi `{BiBUpdSbi PROP, !@BiIndexBottom I bot} :
+    BiBUpdSbi monPredI.
+  Proof. intros P. split=> /= i. unseal. apply bupd_si_pure. Qed.
 
-  Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} :
-    BiFUpdPlainly monPredI.
+  Global Instance monPred_bi_fupd_sbi `{BiFUpdSbi PROP, !@BiIndexBottom I bot} :
+    BiFUpdSbi monPredI.
   Proof.
     split; rewrite /bi_except_0; unseal.
-    - intros E P. split=>/= i.
-      by rewrite (bi.forall_elim i) fupd_plainly_mask_empty.
+    - intros E P. split=>/= i. apply fupd_si_pure_mask_empty.
     - intros E P R. split=>/= i.
       rewrite (bi.forall_elim i) bi.pure_True // bi.True_impl.
-      by rewrite (bi.forall_elim i) fupd_plainly_keep_l.
-    - intros E P. split=>/= i.
-      by rewrite (bi.forall_elim i) fupd_plainly_later.
-    - intros E A Φ. split=>/= i.
-      rewrite -fupd_plainly_forall_2. apply bi.forall_mono=> x.
-      by rewrite (bi.forall_elim i).
+      apply fupd_si_pure_keep_l.
+    - intros E P. split=>/= i. apply fupd_si_pure_later.
+    - intros E A Φ. split=>/= i. apply fupd_si_pure_forall_2.
   Qed.
 End instances.
 
@@ -1144,56 +1108,73 @@ Section bi_facts.
   Global Instance except0_objective P `{!Objective P} : Objective (â—‡ P).
   Proof. rewrite /bi_except_0. apply _. Qed.
 
-  (** Internal equality *)
-  Lemma monPred_internal_eq_unfold `{!BiInternalEq PROP} :
-    @internal_eq monPredI _ = λ A x y, ⎡ x ≡ y ⎤%I.
-  Proof. rewrite monPred_internal_eq_unseal. by unseal. Qed.
+  (** Sbi *)
+  Section sbi.
+    Context `{!Sbi PROP}.
 
-  Lemma monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofe} i (a b : A) :
-    @monPred_at (a ≡ b) i ⊣⊢ a ≡ b.
-  Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
+    Lemma monPred_si_pure_unfold :
+      @si_pure monPredI _ = λ Pi, ⎡ <si_pure> Pi ⎤%I.
+    Proof. by unseal. Qed.
+    Lemma monPred_si_emp_valid_unfold :
+      @si_emp_valid monPredI _ = λ P, (<si_emp_valid> ∀ i, P i)%I.
+    Proof. by unseal. Qed.
 
-  Lemma monPred_equivI `{!BiInternalEq PROP'} P Q :
-    P ≡ Q ⊣⊢@{PROP'} ∀ i, P i ≡ Q i.
-  Proof.
-    apply bi.equiv_entails. split.
-    - apply bi.forall_intro=> ?. apply (f_equivI (flip monPred_at _)).
-    - by rewrite -{2}(sig_monPred_sig P) -{2}(sig_monPred_sig Q)
-                 -f_equivI -sig_equivI !discrete_fun_equivI.
-  Qed.
+    Global Instance si_pure_objective Pi :
+      Objective (PROP:=PROP) (I:=I) (<si_pure> Pi).
+    Proof. rewrite monPred_si_pure_unfold. apply _. Qed.
 
-  Global Instance internal_eq_objective `{!BiInternalEq PROP} {A : ofe} (x y : A) :
-    @Objective I PROP (x ≡ y).
-  Proof. intros ??. rewrite monPred_internal_eq_unfold. by unseal. Qed.
+    (** Internal equality *)
+    Lemma monPred_internal_eq_unfold :
+      @internal_eq monPredI _ = λ A x y, ⎡ x ≡ y ⎤%I.
+    Proof. by rewrite /internal_eq monPred_si_pure_unfold. Qed.
 
-  (** FUpd  *)
-  Lemma monPred_at_fupd `{!BiFUpd PROP} i E1 E2 P :
-    (|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
-  Proof. by rewrite monPred_fupd_unseal. Qed.
+    Lemma monPred_at_internal_eq {A : ofe} i (a b : A) :
+      @monPred_at (a ≡ b) i ⊣⊢ a ≡ b.
+    Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
 
-  Global Instance fupd_objective E1 E2 P `{!Objective P} `{!BiFUpd PROP} :
-    Objective (|={E1,E2}=> P).
-  Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
+    Lemma monPred_equivI `{!Sbi PROP'} P Q :
+      P ≡ Q ⊣⊢@{PROP'} ∀ i, P i ≡ Q i.
+    Proof.
+      apply bi.equiv_entails. split.
+      - apply bi.forall_intro=> ?. apply (f_equivI (flip monPred_at _)).
+      - by rewrite -{2}(sig_monPred_sig P) -{2}(sig_monPred_sig Q)
+                   -f_equivI -sig_equivI !discrete_fun_equivI.
+    Qed.
 
-  (** Plainly *)
-  Lemma monPred_plainly_unfold `{!BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■ (P i) ⎤%I.
-  Proof. by rewrite monPred_plainly_unseal monPred_embed_unseal. Qed.
-  Lemma monPred_at_plainly `{!BiPlainly PROP} i P : (■ P) i ⊣⊢ ∀ j, ■ (P j).
-  Proof. by rewrite monPred_plainly_unseal. Qed.
+    Global Instance internal_eq_objective {A : ofe} (x y : A) :
+      @Objective I PROP (x ≡ y).
+    Proof. intros ??. rewrite monPred_internal_eq_unfold. by unseal. Qed.
 
-  Global Instance monPred_at_plain `{!BiPlainly PROP} P i : Plain P → Plain (P i).
-  Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Qed.
+    (** FUpd  *)
+    Lemma monPred_at_fupd `{!BiFUpd PROP} i E1 E2 P :
+      (|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
+    Proof. by rewrite monPred_fupd_unseal. Qed.
 
-  Global Instance plainly_objective `{!BiPlainly PROP} P : Objective (â–  P).
-  Proof. rewrite monPred_plainly_unfold. apply _. Qed.
-  Global Instance plainly_if_objective `{!BiPlainly PROP} P p `{!Objective P} :
-    Objective (â– ?p P).
-  Proof. rewrite /plainly_if. destruct p; apply _. Qed.
+    Global Instance fupd_objective E1 E2 P `{!Objective P} `{!BiFUpd PROP} :
+      Objective (|={E1,E2}=> P).
+    Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
 
-  Global Instance monPred_objectively_plain `{!BiPlainly PROP} P :
-    Plain P → Plain (<obj> P).
-  Proof. rewrite monPred_objectively_unfold. apply _. Qed.
-  Global Instance monPred_subjectively_plain `{!BiPlainly PROP} P :
-    Plain P → Plain (<subj> P).
-  Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
+    (** Plainly *)
+    Lemma monPred_at_plainly i P : (■ P) i ⊣⊢ ∀ j, ■ (P j).
+    Proof.
+      rewrite /plainly !monPred_si_pure_unfold monPred_si_emp_valid_unfold.
+      by rewrite monPred_at_embed -si_pure_forall -si_emp_valid_forall.
+    Qed.
+
+    Global Instance monPred_at_plain P i : Plain P → Plain (P i).
+    Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Qed.
+
+    Global Instance plainly_objective P : Objective (â–  P).
+    Proof. rewrite /plainly. apply _. Qed.
+    Global Instance plainly_if_objective P p `{!Objective P} :
+      Objective (â– ?p P).
+    Proof. rewrite /plainly_if. destruct p; apply _. Qed.
+
+    Global Instance monPred_objectively_plain P :
+      Plain P → Plain (<obj> P).
+    Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+    Global Instance monPred_subjectively_plain P :
+      Plain P → Plain (<subj> P).
+    Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
+  End sbi.
 End bi_facts.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index af0e93e30e70733e9b149091f3b17ddb7de18409..e6a7e080a06c09b1374fe923ee65db750060c0f2 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -1,114 +1,30 @@
 From iris.algebra Require Import monoid.
-From iris.bi Require Import derived_laws_later big_op internal_eq.
+From iris.bi Require Export internal_eq.
+From iris.bi Require Import derived_laws_later big_op.
 From iris.prelude Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
-(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
-    primitive projections for the bi-records makes the proofmode faster.
-*)
-Local Set Primitive Projections.
-
 (* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 
-Class Plainly (PROP : Type) := plainly : PROP → PROP.
-Global Arguments plainly {PROP}%type_scope {_} _%I.
-Global Hint Mode Plainly ! : typeclass_instances.
+Definition plainly `{!Sbi PROP} (P : PROP) : PROP :=
+  <si_pure> <si_emp_valid> P.
+Global Arguments plainly : simpl never.
 Global Instance: Params (@plainly) 2 := {}.
 Global Typeclasses Opaque plainly.
 
 Notation "â–  P" := (plainly P) : bi_scope.
 
-(* Mixins allow us to create instances easily without having to use Program *)
-Record BiPlainlyMixin (PROP : bi) `(Plainly PROP) := {
-  bi_plainly_mixin_plainly_ne : NonExpansive (plainly (PROP:=PROP));
-
-  bi_plainly_mixin_plainly_mono (P Q : PROP) : (P ⊢ Q) → ■ P ⊢ ■ Q;
-  bi_plainly_mixin_plainly_elim_persistently (P : PROP) : ■ P ⊢ <pers> P;
-  bi_plainly_mixin_plainly_idemp_2 (P : PROP) : ■ P ⊢ ■ ■ P;
-
-  bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A → PROP) :
-    (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a);
-
-  (* The following law and [persistently_impl_plainly] below are very similar,
-     and indeed they hold not just for persistently and plainly, but for any
-     modality defined as [M P n x := ∀ y, R x y → P n y]. *)
-  bi_plainly_mixin_plainly_impl_plainly (P Q : PROP) :
-    (■ P → ■ Q) ⊢ ■ (■ P → Q);
-
-  bi_plainly_mixin_plainly_emp_intro (P : PROP) : P ⊢ ■ emp;
-  bi_plainly_mixin_plainly_absorb (P Q : PROP) : ■ P ∗ Q ⊢ ■ P;
-
-  bi_plainly_mixin_later_plainly_1 (P : PROP) : ▷ ■ P ⊢ ■ ▷ P;
-  bi_plainly_mixin_later_plainly_2 (P : PROP) : ■ ▷ P ⊢ ▷ ■ P;
-}.
-
-Class BiPlainly (PROP : bi) := {
-  bi_plainly_plainly :> Plainly PROP;
-  bi_plainly_mixin : BiPlainlyMixin PROP bi_plainly_plainly;
-}.
-Global Hint Mode BiPlainly ! : typeclass_instances.
-Global Arguments bi_plainly_plainly : simpl never.
-
-Class BiPersistentlyImplPlainly `{!BiPlainly PROP} :=
-  persistently_impl_plainly (P Q : PROP) :
-    (■ P → <pers> Q) ⊢ <pers> (■ P → Q).
-Global Arguments BiPersistentlyImplPlainly : clear implicits.
-Global Arguments BiPersistentlyImplPlainly _ {_}.
-Global Arguments persistently_impl_plainly _ {_ _} _.
-Global Hint Mode BiPersistentlyImplPlainly ! - : typeclass_instances.
-
-Class BiPlainlyExist {PROP: bi} `{!BiPlainly PROP} :=
-  plainly_exist_1 A (Ψ : A → PROP) :
-    ■ (∃ a, Ψ a) ⊢ ∃ a, ■ (Ψ a).
-Global Arguments BiPlainlyExist : clear implicits.
-Global Arguments BiPlainlyExist _ {_}.
-Global Arguments plainly_exist_1 _ {_ _} _.
-Global Hint Mode BiPlainlyExist ! - : typeclass_instances.
-
-Class BiPropExt {PROP: bi} `{!BiPlainly PROP, !BiInternalEq PROP} :=
-  prop_ext_2 (P Q : PROP) : ■ (P ∗-∗ Q) ⊢ P ≡ Q.
-Global Arguments BiPropExt : clear implicits.
-Global Arguments BiPropExt _ {_ _}.
-Global Arguments prop_ext_2 _ {_ _ _} _.
-Global Hint Mode BiPropExt ! - - : typeclass_instances.
-
-Section plainly_laws.
-  Context {PROP: bi} `{!BiPlainly PROP}.
-  Implicit Types P Q : PROP.
-
-  Global Instance plainly_ne : NonExpansive (@plainly PROP _).
-  Proof. eapply bi_plainly_mixin_plainly_ne, bi_plainly_mixin. Qed.
-
-  Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
-  Proof. eapply bi_plainly_mixin_plainly_mono, bi_plainly_mixin. Qed.
-  Lemma plainly_elim_persistently P : ■ P ⊢ <pers> P.
-  Proof. eapply bi_plainly_mixin_plainly_elim_persistently, bi_plainly_mixin. Qed.
-  Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
-  Proof. eapply bi_plainly_mixin_plainly_idemp_2, bi_plainly_mixin. Qed.
-  Lemma plainly_forall_2 {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a).
-  Proof. eapply bi_plainly_mixin_plainly_forall_2, bi_plainly_mixin. Qed.
-  Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
-  Proof. eapply bi_plainly_mixin_plainly_impl_plainly, bi_plainly_mixin. Qed.
-  Lemma plainly_absorb P Q : ■ P ∗ Q ⊢ ■ P.
-  Proof. eapply bi_plainly_mixin_plainly_absorb, bi_plainly_mixin. Qed.
-  Lemma plainly_emp_intro P : P ⊢ ■ emp.
-  Proof. eapply bi_plainly_mixin_plainly_emp_intro, bi_plainly_mixin. Qed.
-
-  Lemma later_plainly_1 P : ▷ ■ P ⊢ ■ (▷ P).
-  Proof. eapply bi_plainly_mixin_later_plainly_1, bi_plainly_mixin. Qed.
-  Lemma later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P.
-  Proof. eapply bi_plainly_mixin_later_plainly_2, bi_plainly_mixin. Qed.
-End plainly_laws.
-
-(* Derived properties and connectives *)
-Class Plain {PROP: bi} `{!BiPlainly PROP} (P : PROP) := plain : P ⊢ ■ P.
+Class Plain `{!Sbi PROP} (P : PROP) := plain : P ⊢ ■ P.
 Global Arguments Plain {_ _} _%I : simpl never.
 Global Arguments plain {_ _} _%I {_}.
 Global Hint Mode Plain + - ! : typeclass_instances.
 Global Instance: Params (@Plain) 1 := {}.
 
-Definition plainly_if {PROP: bi} `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
+Global Instance siProp_plain (P : siProp) : Plain P | 0.
+Proof. done. Qed.
+
+Definition plainly_if `{!Sbi PROP} (p : bool) (P : PROP) : PROP :=
   (if p then â–  P else P)%I.
 Global Arguments plainly_if {_ _} !_ _%I /.
 Global Instance: Params (@plainly_if) 2 := {}.
@@ -116,26 +32,53 @@ Global Typeclasses Opaque plainly_if.
 
 Notation "â– ? p P" := (plainly_if p P) : bi_scope.
 
-(* Derived laws *)
-Section plainly_derived.
-  Context {PROP: bi} `{!BiPlainly PROP}.
-  Implicit Types P : PROP.
+Section plainly.
+  Context `{!Sbi PROP}.
+  Implicit Types P Q : PROP.
 
   Local Hint Resolve pure_intro forall_intro : core.
   Local Hint Resolve or_elim or_intro_l' or_intro_r' : core.
   Local Hint Resolve and_intro and_elim_l' and_elim_r' : core.
 
-  Global Instance plainly_proper :
-    Proper ((⊣⊢) ==> (⊣⊢)) (@plainly PROP _) := ne_proper _.
+  Global Instance plainly_ne : NonExpansive (plainly (PROP:=PROP)).
+  Proof. solve_proper. Qed.
+  Global Instance plainly_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@plainly PROP _).
+  Proof. apply ne_proper, _. Qed.
 
+  Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
+  Proof. intros. by apply si_pure_mono, si_emp_valid_mono. Qed.
   Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@plainly PROP _).
   Proof. intros P Q; apply plainly_mono. Qed.
   Global Instance plainly_flip_mono' :
     Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _).
   Proof. intros P Q; apply plainly_mono. Qed.
 
+  Lemma plainly_elim_persistently P : ■ P ⊢ <pers> P.
+  Proof. apply si_pure_si_emp_valid. Qed.
+  Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
+  Proof. by rewrite /plainly si_emp_valid_si_pure. Qed.
+  Lemma plainly_forall_2 {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a).
+  Proof. by rewrite /plainly si_emp_valid_forall si_pure_forall. Qed.
+  Lemma plainly_exist_1 `{!SbiEmpValidExist PROP} {A} (Ψ : A → PROP) :
+    ■ (∃ a, Ψ a) ⊢ ∃ a, ■ (Ψ a).
+  Proof. by rewrite /plainly si_emp_valid_exist si_pure_exist. Qed.
+  Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
+  Proof. by rewrite /plainly si_pure_impl_2 -si_emp_valid_impl_si_pure. Qed.
+  Lemma plainly_emp_intro P : P ⊢ ■ emp.
+  Proof. rewrite /plainly si_emp_valid_emp si_pure_pure. apply True_intro. Qed.
+  Lemma plainly_absorb P Q : ■ P ∗ Q ⊢ ■ P.
+  Proof. by rewrite /plainly sep_elim_l. Qed.
+  Lemma later_plainly P : ▷ ■ P ⊣⊢ ■ ▷ P.
+  Proof. by rewrite /plainly -si_pure_later -si_emp_valid_later. Qed.
+  Lemma later_plainly_1 P : ▷ ■ P ⊢ ■ (▷ P).
+  Proof. by rewrite later_plainly. Qed.
+  Lemma later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P.
+  Proof. by rewrite later_plainly. Qed.
+
   Lemma affinely_plainly_elim P : <affine> ■ P ⊢ P.
-  Proof. by rewrite plainly_elim_persistently /bi_affinely persistently_and_emp_elim. Qed.
+  Proof.
+    by rewrite plainly_elim_persistently /bi_affinely persistently_and_emp_elim.
+  Qed.
 
   Lemma persistently_elim_plainly P : <pers> ■ P ⊣⊢ ■ P.
   Proof.
@@ -156,7 +99,9 @@ Section plainly_derived.
   Qed.
 
   Lemma absorbingly_elim_plainly P : <absorb> ■ P ⊣⊢ ■ P.
-  Proof. by rewrite -(persistently_elim_plainly P) absorbingly_elim_persistently. Qed.
+  Proof.
+    by rewrite -(persistently_elim_plainly P) absorbingly_elim_persistently.
+  Qed.
 
   Lemma plainly_and_sep_elim P Q : ■ P ∧ Q ⊢ (emp ∧ P) ∗ Q.
   Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim_emp. Qed.
@@ -178,28 +123,21 @@ Section plainly_derived.
   Proof. intros <-. apply plainly_idemp_2. Qed.
 
   Lemma plainly_pure φ : ■ ⌜φ⌝ ⊣⊢@{PROP} ⌜φ⌝.
-  Proof.
-    apply (anti_symm _); auto.
-    - 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 φ).
-  Qed.
+  Proof. by rewrite /plainly si_emp_valid_pure si_pure_pure. Qed.
+  Lemma plainly_si_pure Pi : ■ <si_pure> Pi ⊣⊢@{PROP} <si_pure> Pi.
+  Proof. by rewrite /plainly si_emp_valid_si_pure. Qed.
   Lemma plainly_forall {A} (Ψ : A → PROP) : ■ (∀ a, Ψ a) ⊣⊢ ∀ a, ■ (Ψ a).
-  Proof.
-    apply (anti_symm _); auto using plainly_forall_2.
-    apply forall_intro=> x. by rewrite (forall_elim x).
-  Qed.
+  Proof. by rewrite /plainly si_emp_valid_forall si_pure_forall. Qed.
   Lemma plainly_exist_2 {A} (Ψ : A → PROP) : (∃ a, ■ (Ψ a)) ⊢ ■ (∃ a, Ψ a).
   Proof. apply exist_elim=> x. by rewrite (exist_intro x). Qed.
-  Lemma plainly_exist `{!BiPlainlyExist PROP} {A} (Ψ : A → PROP) :
+  Lemma plainly_exist `{!SbiEmpValidExist PROP} {A} (Ψ : A → PROP) :
     ■ (∃ a, Ψ a) ⊣⊢ ∃ a, ■ (Ψ a).
   Proof. apply (anti_symm _); auto using plainly_exist_1, plainly_exist_2. Qed.
   Lemma plainly_and P Q : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q.
   Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
   Lemma plainly_or_2 P Q : ■ P ∨ ■ Q ⊢ ■ (P ∨ Q).
   Proof. rewrite !or_alt -plainly_exist_2. by apply exist_mono=> -[]. Qed.
-  Lemma plainly_or `{!BiPlainlyExist PROP} P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
+  Lemma plainly_or `{!SbiEmpValidExist PROP} P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
   Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed.
   Lemma plainly_impl P Q : ■ (P → Q) ⊢ ■ P → ■ Q.
   Proof.
@@ -233,7 +171,9 @@ Section plainly_derived.
   Qed.
 
   Lemma plainly_affinely_elim P : ■ <affine> P ⊣⊢ ■ P.
-  Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
+  Proof.
+   by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id.
+  Qed.
 
   Lemma intuitionistically_plainly_elim P : □ ■ P ⊢ □ P.
   Proof. rewrite intuitionistically_affinely plainly_elim_persistently //. Qed.
@@ -255,7 +195,8 @@ Section plainly_derived.
   Lemma plainly_sep `{!BiPositive PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
   Proof.
     apply (anti_symm _); auto using plainly_sep_2.
-    rewrite -(plainly_affinely_elim (_ ∗ _)) affinely_sep -and_sep_plainly. apply and_intro.
+    rewrite -(plainly_affinely_elim (_ ∗ _)).
+    rewrite affinely_sep -and_sep_plainly. apply and_intro.
     - by rewrite (affinely_elim_emp Q) right_id affinely_elim.
     - by rewrite (affinely_elim_emp P) left_id affinely_elim.
   Qed.
@@ -281,9 +222,14 @@ Section plainly_derived.
   Lemma impl_wand_affinely_plainly P Q : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ Q).
   Proof. by rewrite -(persistently_elim_plainly P) impl_wand_intuitionistically. Qed.
 
-  Lemma persistently_wand_affinely_plainly `{!BiPersistentlyImplPlainly PROP} P Q :
+  Lemma persistently_impl_plainly `{!BiPersistentlyImplSiPure PROP} P Q :
+    (■ P → <pers> Q) ⊢ <pers> (■ P → Q).
+  Proof. by apply persistently_impl_si_pure. Qed.
+  Lemma persistently_wand_affinely_plainly `{!BiPersistentlyImplSiPure PROP} P Q :
     (<affine> ■ P -∗ <pers> Q) ⊢ <pers> (<affine> ■ P -∗ Q).
-  Proof. rewrite -!impl_wand_affinely_plainly. apply: persistently_impl_plainly. Qed.
+  Proof. 
+    rewrite -!impl_wand_affinely_plainly. apply: persistently_impl_plainly.
+  Qed.
 
   Lemma plainly_wand_affinely_plainly P Q :
     (<affine> ■ P -∗ ■ Q) ⊢ ■ (<affine> ■ P -∗ Q).
@@ -338,11 +284,12 @@ Section plainly_derived.
   Proof. destruct p; simpl; auto using plainly_and. Qed.
   Lemma plainly_if_or_2 p P Q : ■?p P ∨ ■?p Q ⊢ ■?p (P ∨ Q).
   Proof. destruct p; simpl; auto using plainly_or_2. Qed.
-  Lemma plainly_if_or `{!BiPlainlyExist PROP} p P Q : ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
+  Lemma plainly_if_or `{!SbiEmpValidExist PROP} p P Q :
+    ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
   Proof. destruct p; simpl; auto using plainly_or. Qed.
   Lemma plainly_if_exist_2 {A} p (Ψ : A → PROP) : (∃ a, ■?p (Ψ a)) ⊢ ■?p (∃ a, Ψ a).
   Proof. destruct p; simpl; auto using plainly_exist_2. Qed.
-  Lemma plainly_if_exist `{!BiPlainlyExist PROP} {A} p (Ψ : A → PROP) :
+  Lemma plainly_if_exist `{!SbiEmpValidExist PROP} {A} p (Ψ : A → PROP) :
     ■?p (∃ a, Ψ a) ⊣⊢ ∃ a, ■?p (Ψ a).
   Proof. destruct p; simpl; auto using plainly_exist. Qed.
   Lemma plainly_if_sep_2 `{!BiPositive PROP} p P Q : ■?p P ∗ ■?p Q  ⊢ ■?p (P ∗ Q).
@@ -373,7 +320,7 @@ Section plainly_derived.
   Lemma plain_persistent P : Plain P → Persistent P.
   Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
 
-  Global Instance impl_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
+  Global Instance impl_persistent `{!BiPersistentlyImplSiPure PROP} P Q :
     Absorbing P → Plain P → Persistent Q → Persistent (P → Q).
   Proof.
     intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly
@@ -383,7 +330,7 @@ Section plainly_derived.
   Global Instance plainly_persistent P : Persistent (â–  P).
   Proof. by rewrite /Persistent persistently_elim_plainly. Qed.
 
-  Global Instance wand_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
+  Global Instance wand_persistent `{!BiPersistentlyImplSiPure PROP} P Q :
     Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q).
   Proof.
     intros. rewrite /Persistent {2}(plain P). trans (<pers> (■ P → Q))%I.
@@ -392,12 +339,13 @@ Section plainly_derived.
     - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
   Qed.
 
-  Global Instance limit_preserving_Plain {A : ofe} `{!Cofe A} (Φ : A → PROP) :
+  Global Instance limit_preserving_Plain `{!Cofe A} (Φ : A → PROP) :
     NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
   Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
   (* Instances for big operators *)
-  Global Instance plainly_sep_weak_homomorphism `{!BiPositive PROP, !BiAffine PROP} :
+  Global Instance plainly_sep_weak_homomorphism
+      `{!BiPositive PROP, !BiAffine PROP} :
     WeakMonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
   Proof. split; try apply _. apply plainly_sep. Qed.
   Global Instance plainly_sep_entails_weak_homomorphism :
@@ -413,7 +361,7 @@ Section plainly_derived.
   Global Instance plainly_and_homomorphism :
     MonoidHomomorphism bi_and bi_and (≡) (@plainly PROP _).
   Proof. split; [split|]; try apply _; [apply plainly_and | apply plainly_pure]. Qed.
-  Global Instance plainly_or_homomorphism `{!BiPlainlyExist PROP} :
+  Global Instance plainly_or_homomorphism `{!SbiEmpValidExist PROP} :
     MonoidHomomorphism bi_or bi_or (≡) (@plainly PROP _).
   Proof. split; [split|]; try apply _; [apply plainly_or | apply plainly_pure]. Qed.
 
@@ -423,7 +371,7 @@ Section plainly_derived.
   Lemma big_andL_plainly {A} (Φ : nat → A → PROP) l :
     ■ ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, ■ (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
-  Lemma big_orL_plainly `{!BiPlainlyExist PROP} {A} (Φ : nat → A → PROP) l :
+  Lemma big_orL_plainly `{!SbiEmpValidExist PROP} {A} (Φ : nat → A → PROP) l :
     ■ ([∨ list] k↦x ∈ l, Φ k x) ⊣⊢ [∨ list] k↦x ∈ l, ■ (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
@@ -436,7 +384,8 @@ Section plainly_derived.
     ■ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, ■ (Φ k x).
   Proof. apply (big_opM_commute _). Qed.
 
-  Lemma big_sepM2_plainly `{!BiAffine PROP, Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
+  Lemma big_sepM2_plainly `{!BiAffine PROP, Countable K} {A B}
+      (Φ : K → A → B → PROP) m1 m2 :
     ■ ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢ [∗ map] k↦x1;x2 ∈ m1;m2, ■ (Φ k x1 x2).
   Proof. by rewrite !big_sepM2_alt plainly_and plainly_pure big_sepM_plainly. Qed.
 
@@ -488,7 +437,8 @@ Section plainly_derived.
   Proof. by rewrite /Plain plainly_idemp. Qed.
   Global Instance persistently_plain P : Plain P → Plain (<pers> P).
   Proof.
-    rewrite /Plain=> HP. rewrite {1}HP plainly_persistently_elim persistently_elim_plainly //.
+    rewrite /Plain=> HP.
+    rewrite {1}HP plainly_persistently_elim persistently_elim_plainly //.
   Qed.
   Global Instance affinely_plain P : Plain P → Plain (<affine> P).
   Proof. rewrite /bi_affinely. apply _. Qed.
@@ -500,6 +450,11 @@ Section plainly_derived.
     (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
   Proof. destruct mx; apply _. Qed.
 
+  Global Instance si_pure_plain Pi : Plain (PROP:=PROP) (<si_pure> Pi).
+  Proof. by rewrite /Plain plainly_si_pure. Qed.
+  Global Instance si_emp_valid_plain P : Plain (<si_emp_valid> P).
+  Proof. by rewrite /Plain. Qed.
+
   Global Instance big_sepL_nil_plain {A} (Φ : nat → A → PROP) :
     Plain ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
@@ -567,81 +522,61 @@ Section plainly_derived.
       [rewrite big_opMS_empty|rewrite big_opMS_insert]; apply _.
   Qed.
 
-  Global Instance plainly_timeless P  `{!BiPlainlyExist PROP} :
-    Timeless P → Timeless (■ P).
-  Proof.
-    intros. rewrite /Timeless /bi_except_0 later_plainly_1.
-    by rewrite (timeless P) /bi_except_0 plainly_or {1}plainly_elim.
-  Qed.
+  Global Instance plainly_timeless P : Timeless P → Timeless (■ P).
+  Proof. rewrite /plainly. apply _. Qed.
 
   (* Interaction with equality *)
-  Section internal_eq.
-    Context `{!BiInternalEq PROP}.
-
-    Lemma plainly_internal_eq {A:ofe} (a b : A) : ■ (a ≡ b) ⊣⊢@{PROP} a ≡ b.
-    Proof.
-      apply (anti_symm (⊢)).
-      { by rewrite plainly_elim. }
-      apply (internal_eq_rewrite' a b (λ  b, ■ (a ≡ b))%I); [solve_proper|done|].
-      rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
-    Qed.
-
-    Global Instance internal_eq_plain {A : ofe} (a b : A) :
-      Plain (PROP:=PROP) (a ≡ b).
-    Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
-  End internal_eq.
+  Lemma plainly_internal_eq {A:ofe} (a b : A) : ■ (a ≡ b) ⊣⊢@{PROP} a ≡ b.
+  Proof.
+    apply (anti_symm (⊢)).
+    { by rewrite plainly_elim. }
+    apply (internal_eq_rewrite' a b (λ  b, ■ (a ≡ b))%I); [solve_proper|done|].
+    rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
+  Qed.
 
-  Section prop_ext.
-    Context `{!BiInternalEq PROP, !BiPropExt PROP}.
+  Global Instance internal_eq_plain {A : ofe} (a b : A) :
+    Plain (PROP:=PROP) (a ≡ b).
+  Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
 
-    Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■ (P ∗-∗ Q).
-    Proof.
-      apply (anti_symm (⊢)); last exact: prop_ext_2.
-      apply (internal_eq_rewrite' P Q (λ Q, ■ (P ∗-∗ Q))%I);
-        [ solve_proper | done | ].
-      rewrite (plainly_emp_intro (P ≡ Q)).
-      apply plainly_mono, wand_iff_refl.
-    Qed.
+  (* FIMXE: Rename, conflict with the si_pure version *)
+  Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■ (P ∗-∗ Q).
+  Proof. by rewrite /plainly -prop_ext si_pure_internal_eq. Qed.
+  Lemma prop_ext_2 P Q : ■ (P ∗-∗ Q) ⊢ P ≡ Q.
+  Proof. by rewrite prop_ext. Qed.
 
-    Lemma plainly_alt P : ■ P ⊣⊢ <affine> P ≡ emp.
-    Proof.
-      rewrite -plainly_affinely_elim. apply (anti_symm (⊢)).
-      - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
-        + by rewrite affinely_elim_emp left_id.
-        + by rewrite left_id.
-      - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
-        by rewrite -plainly_True_emp plainly_pure True_impl.
-    Qed.
+  Lemma plainly_alt P : ■ P ⊣⊢ <affine> P ≡ emp.
+  Proof.
+    rewrite -plainly_affinely_elim. apply (anti_symm (⊢)).
+    - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
+      + by rewrite affinely_elim_emp left_id.
+      + by rewrite left_id.
+    - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
+      by rewrite -plainly_True_emp plainly_pure True_impl.
+  Qed.
 
-    Lemma plainly_alt_absorbing P `{!Absorbing P} : ■ P ⊣⊢ P ≡ True.
-    Proof.
-      apply (anti_symm (⊢)).
-      - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
-      - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
-        by rewrite plainly_pure True_impl.
-    Qed.
+  Lemma plainly_alt_absorbing P `{!Absorbing P} : ■ P ⊣⊢ P ≡ True.
+  Proof.
+    apply (anti_symm (⊢)).
+    - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+    - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
+      by rewrite plainly_pure True_impl.
+  Qed.
 
-    Lemma plainly_True_alt P : ■ (True -∗ P) ⊣⊢ P ≡ True.
-    Proof.
-      apply (anti_symm (⊢)).
-      - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
-        by rewrite wand_elim_r.
-      - rewrite internal_eq_sym (internal_eq_rewrite _ _
-          (λ Q, ■ (True -∗ Q))%I ltac:(shelve)); last solve_proper.
-        by rewrite -entails_wand // -(plainly_emp_intro True) True_impl.
-    Qed.
+  Lemma plainly_True_alt P : ■ (True -∗ P) ⊣⊢ P ≡ True.
+  Proof.
+    apply (anti_symm (⊢)).
+    - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+      by rewrite wand_elim_r.
+    - rewrite internal_eq_sym (internal_eq_rewrite _ _
+        (λ Q, ■ (True -∗ Q))%I ltac:(shelve)); last solve_proper.
+      by rewrite -entails_wand // -(plainly_emp_intro True) True_impl.
+  Qed.
 
-    (* This proof uses [BiPlainlyExist] and [BiLöb] via [plainly_timeless] and
-    [wand_timeless]. *)
-    Global Instance internal_eq_timeless `{!BiPlainlyExist PROP, !BiLöb PROP}
-        `{!Timeless P} `{!Timeless Q} :
-      Timeless (PROP := PROP) (P ≡ Q).
-    Proof. rewrite prop_ext. apply _. Qed.
-  End prop_ext.
+  Global Instance internal_eq_timeless P Q :
+    Timeless P → Timeless Q → Timeless (PROP := PROP) (P ≡ Q).
+  Proof. rewrite prop_ext. apply _. Qed.
 
   (* Interaction with â–· *)
-  Lemma later_plainly P : ▷ ■ P ⊣⊢ ■ ▷ P.
-  Proof. apply (anti_symm _); auto using later_plainly_1, later_plainly_2. Qed.
   Lemma laterN_plainly n P : ▷^n ■ P ⊣⊢ ■ ▷^n P.
   Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_plainly. Qed.
 
@@ -652,9 +587,8 @@ Section plainly_derived.
 
   Lemma except_0_plainly_1 P : ◇ ■ P ⊢ ■ ◇ P.
   Proof. by rewrite /bi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed.
-  Lemma except_0_plainly `{!BiPlainlyExist PROP} P : ◇ ■ P ⊣⊢ ■ ◇ P.
-  Proof. by rewrite /bi_except_0 plainly_or -later_plainly plainly_pure. Qed.
-
+  Lemma except_0_plainly P : ◇ ■ P ⊣⊢ ■ ◇ P.
+  Proof. by rewrite /plainly si_emp_valid_except_0 si_pure_except_0. Qed.
   Global Instance later_plain P : Plain P → Plain (▷ P).
   Proof. intros. by rewrite /Plain -later_plainly {1}(plain P). Qed.
   Global Instance laterN_plain n P : Plain P → Plain (▷^n P).
@@ -662,7 +596,7 @@ Section plainly_derived.
   Global Instance except_0_plain P : Plain P → Plain (◇ P).
   Proof. rewrite /bi_except_0; apply _. Qed.
 
-End plainly_derived.
+End plainly.
 
 (* When declared as an actual instance, [plain_persistent] will cause
 failing proof searches to take exponential time, as Coq will try to
diff --git a/iris/bi/sbi.v b/iris/bi/sbi.v
index 2defe23e9670cc5697c8abf810d08d47eb96b4b0..ee7cb746de6972fdcdf53ba80c8f4101b1be9a6c 100644
--- a/iris/bi/sbi.v
+++ b/iris/bi/sbi.v
@@ -11,12 +11,14 @@ Local Set Primitive Projections.
 Class SiPure (PROP : Type) : Type := si_pure : siProp → PROP.
 Global Instance : Params (@si_pure) 2 := {}.
 Global Hint Mode SiPure ! : typeclass_instances.
+Global Typeclasses Opaque si_pure.
 Global Arguments si_pure {_}%type_scope {_} _%bi_scope.
 Notation "<si_pure> Pi" := (si_pure Pi) : bi_scope.
 
 Class SiEmpValid (PROP : Type) : Type := si_emp_valid : PROP → siProp.
 Global Instance : Params (@si_emp_valid) 2 := {}.
 Global Hint Mode SiEmpValid ! : typeclass_instances.
+Global Typeclasses Opaque si_emp_valid.
 Global Arguments si_emp_valid {_}%type_scope {_} _%bi_scope.
 Notation "<si_emp_valid> P" := (si_emp_valid P) : bi_scope.
 
@@ -37,8 +39,6 @@ Record SbiMixin (PROP : bi) `(!SiPure PROP, SiEmpValid PROP) := {
   sbi_mixin_si_pure_absorbing Pi :
     Absorbing (PROP:=PROP) (<si_pure> Pi);
 
-  sbi_mixin_si_emp_valid_exist_1 {A} (Φ : A → PROP) :
-    <si_emp_valid> (∃ x, Φ x) ⊢@{siPropI} (∃ x, <si_emp_valid> Φ x);
   sbi_mixin_si_emp_valid_later_1 (P : PROP) :
     <si_emp_valid> ▷ P ⊢@{siPropI} ▷ <si_emp_valid> P;
   sbi_mixin_si_emp_valid_affinely_2 (P : PROP) :
@@ -50,23 +50,54 @@ Record SbiMixin (PROP : bi) `(!SiPure PROP, SiEmpValid PROP) := {
     <si_pure> <si_emp_valid> P ⊢ <pers> P
 }.
 
+Record SbiPropExtMixin (PROP : bi) `(!SiEmpValid PROP) := {
+  sbi_mixin_prop_ext_2 (P Q : PROP) :
+    <si_emp_valid> (P ∗-∗ Q) ⊢@{siPropI} siProp_internal_eq P Q;
+}.
+
 Class Sbi (PROP : bi) := {
   sbi_si_pure :> SiPure PROP;
   sbi_si_emp_valid :> SiEmpValid PROP;
   sbi_sbi_mixin : SbiMixin PROP sbi_si_pure sbi_si_emp_valid;
+  sbi_sbi_prop_ext_mixin : SbiPropExtMixin PROP sbi_si_emp_valid;
 }.
 Global Hint Mode Sbi ! : typeclass_instances.
 Global Arguments sbi_si_pure : simpl never.
 Global Arguments sbi_si_emp_valid : simpl never.
 
-Class BiPersistentlyImplSiPure `{!Sbi PROP} :=
+Class SbiEmpValidExist PROP `{!Sbi PROP} :=
+  si_emp_valid_exist_1 : ∀ {A} (Φ : A → PROP),
+    <si_emp_valid> (∃ x, Φ x) ⊢@{siPropI} (∃ x, <si_emp_valid> Φ x).
+Global Arguments SbiEmpValidExist _ {_}.
+Global Arguments si_emp_valid_exist_1 _ {_ _} _.
+Global Hint Mode SbiEmpValidExist ! - : typeclass_instances.
+
+Class BiPersistentlyImplSiPure PROP `{!Sbi PROP} :=
   persistently_impl_si_pure Pi (Q : PROP) :
     (<si_pure> Pi → <pers> Q) ⊢ <pers> (<si_pure> Pi → Q).
-Global Arguments BiPersistentlyImplSiPure : clear implicits.
 Global Arguments BiPersistentlyImplSiPure _ {_}.
 Global Arguments persistently_impl_si_pure _ {_ _} _.
 Global Hint Mode BiPersistentlyImplSiPure ! - : typeclass_instances.
 
+(** [siProp] itself is an SBI by taking [<si_pure>] and [<si_emp_valid>] to be
+the identity. *)
+Lemma siprop_sbi_mixin : SbiMixin siProp id id.
+Proof.
+  split; rewrite /si_pure /si_emp_valid; try (done || apply _).
+  intros P. by rewrite bi.affine_affinely.
+Qed.
+Lemma siprop_sbi_prop_ext_mixin : SbiPropExtMixin siProp id.
+Proof. split; intros P Q. apply siProp_primitive.prop_ext_2. Qed.
+
+Global Instance siprop_sbi : Sbi siPropI :=
+  {| sbi_sbi_mixin := siprop_sbi_mixin;
+     sbi_sbi_prop_ext_mixin := siprop_sbi_prop_ext_mixin |}.
+Global Instance siprop_sbi_emp_valid_exist : SbiEmpValidExist siPropI.
+Proof. done. Qed.
+Global Instance siprop_bi_persistently_impl_si_pure :
+  BiPersistentlyImplSiPure siPropI.
+Proof. done. Qed.
+
 Section sbi_laws.
   Context `{!Sbi PROP}.
   Implicit Types Pi Qi Ri : siProp.
@@ -102,10 +133,6 @@ Section sbi_laws.
   Lemma si_emp_valid_later_1 (P : PROP) :
     <si_emp_valid> ▷ P ⊢@{siPropI} ▷ <si_emp_valid> P.
   Proof. eapply sbi_mixin_si_emp_valid_later_1, sbi_sbi_mixin. Qed.
-  Lemma si_emp_valid_exist_1 {A} (Φ : A → PROP) :
-    <si_emp_valid> (∃ x, Φ x) ⊢@{siPropI} (∃ x, <si_emp_valid> Φ x).
-  Proof. eapply sbi_mixin_si_emp_valid_exist_1, sbi_sbi_mixin. Qed.
-
   Lemma si_emp_valid_si_pure Pi :
     <si_emp_valid> (<si_pure> Pi : PROP) ⊣⊢@{siPropI} Pi.
   Proof. eapply sbi_mixin_si_emp_valid_si_pure, sbi_sbi_mixin. Qed.
@@ -276,16 +303,21 @@ Section sbi_derived.
       rewrite si_pure_forall -si_emp_valid_affinely bi.affinely_forall.
       by setoid_rewrite affinely_si_pure_si_emp_valid.
   Qed.
-  Lemma si_emp_valid_exist {A} (Φ : A → PROP) :
+  Lemma si_emp_valid_exist_2 {A} (Φ : A → PROP) :
+    (∃ x, <si_emp_valid> Φ x) ⊢@{siPropI} <si_emp_valid> (∃ x, Φ x).
+  Proof. apply bi.exist_elim=> x. by rewrite -(bi.exist_intro x). Qed.
+  Lemma si_emp_valid_exist `{!SbiEmpValidExist PROP} {A} (Φ : A → PROP) :
     <si_emp_valid> (∃ x, Φ x) ⊣⊢@{siPropI} ∃ x, <si_emp_valid> Φ x.
   Proof.
-    apply (anti_symm _); [apply si_emp_valid_exist_1|].
-    apply bi.exist_elim=> x. by rewrite -(bi.exist_intro x).
+    apply (anti_symm _); [apply: si_emp_valid_exist_1|apply si_emp_valid_exist_2].
   Qed.
   Lemma si_emp_valid_and P Q :
     <si_emp_valid> (P ∧ Q) ⊣⊢@{siPropI} <si_emp_valid> P ∧ <si_emp_valid> Q.
   Proof. rewrite !bi.and_alt si_emp_valid_forall. by f_equiv=> -[]. Qed.
-  Lemma si_emp_valid_or P Q :
+  Lemma si_emp_valid_or_2 P Q :
+    <si_emp_valid> P ∨ <si_emp_valid> Q ⊢@{siPropI} <si_emp_valid> (P ∨ Q).
+  Proof. rewrite !bi.or_alt -si_emp_valid_exist_2. by f_equiv=> -[]. Qed.
+  Lemma si_emp_valid_or `{!SbiEmpValidExist PROP} P Q :
     <si_emp_valid> (P ∨ Q) ⊣⊢@{siPropI} <si_emp_valid> P ∨ <si_emp_valid> Q.
   Proof. rewrite !bi.or_alt si_emp_valid_exist. by f_equiv=> -[]. Qed.
   Lemma si_emp_valid_impl_si_pure Pi Q :
@@ -312,7 +344,17 @@ Section sbi_derived.
   Lemma si_emp_valid_except_0 P :
     <si_emp_valid> ◇ P ⊣⊢@{siPropI} ◇ <si_emp_valid> P.
   Proof.
-    by rewrite /bi_except_0 si_emp_valid_or si_emp_valid_later si_emp_valid_pure.
+    apply (anti_symm _).
+    - trans (▷ <si_emp_valid> P ∧ <si_emp_valid> ◇ P)%I.
+      { apply bi.and_intro, reflexivity.
+        by rewrite -si_emp_valid_later bi.except_0_into_later. }
+      rewrite bi.later_false_em bi.and_or_r. apply bi.or_elim.
+      { rewrite bi.and_elim_l. apply bi.or_intro_l. }
+      apply bi.or_intro_r'. rewrite si_emp_valid_impl_si_pure -si_emp_valid_and.
+      f_equiv. rewrite si_pure_later si_pure_pure.
+      by rewrite bi.and_or_l bi.impl_elim_l bi.and_elim_r idemp.
+    - rewrite /bi_except_0 -si_emp_valid_or_2.
+      by rewrite si_emp_valid_later si_emp_valid_pure.
   Qed.
 
   Global Instance si_emp_valid_timeless P :
@@ -348,12 +390,13 @@ Section sbi_derived.
   (** Soundness lemmas *)
   Lemma pure_soundness φ : (⊢@{PROP} ⌜ φ ⌝) → φ.
   Proof.
-    rewrite -si_pure_pure si_pure_emp_valid. apply siProp.pure_soundness.
+    rewrite -si_pure_pure si_pure_emp_valid.
+    apply siProp_primitive.pure_soundness.
   Qed.
 
   Lemma later_soundness (P : PROP) : (⊢ ▷ P) → ⊢ P.
   Proof.
     rewrite -!si_emp_valid_emp_valid si_emp_valid_later.
-    apply siProp.later_soundness.
+    apply siProp_primitive.later_soundness.
   Qed.
 End sbi_derived.
diff --git a/iris/bi/sbi_unfold.v b/iris/bi/sbi_unfold.v
new file mode 100644
index 0000000000000000000000000000000000000000..0b5f517ff1aef22cc227a676bd83c41cf8ca8519
--- /dev/null
+++ b/iris/bi/sbi_unfold.v
@@ -0,0 +1,136 @@
+From iris.bi Require Export cmra_valid internal_eq.
+From iris.prelude Require Import options.
+Local Set Default Proof Using "Type*".
+
+(* For the ∀/∃ instances we need this record to live in [Type], i.e., we need
+strong elimination of the witness [sbi_unfold_car]. *)
+Class UnfoldSbi `{!Sbi PROP} (P : PROP) (Pi : nat → Prop) := {
+  sbi_unfold_car : siProp;
+  sbi_unfold_as_si_pure : P ⊣⊢ <si_pure> sbi_unfold_car;
+  sbi_unfold_siProp_holds n : siProp_holds sbi_unfold_car n ↔ Pi n;
+}.
+Global Hint Mode UnfoldSbi + + ! - : typeclass_instances.
+Global Arguments sbi_unfold_car {_ _} _ {_ _}.
+
+Section sbi_unfold.
+  Context `{Sbi PROP}.
+  Implicit Types P Q : PROP.
+  Local Arguments siProp_holds !_.
+  Local Notation UnfoldSbi := (UnfoldSbi (PROP:=PROP)).
+
+  Lemma sbi_unfold_entails `{!UnfoldSbi P Pi, !UnfoldSbi Q Qi} :
+    (P ⊢ Q) ↔ ∀ n, Pi n → Qi n.
+  Proof.
+    rewrite [P]sbi_unfold_as_si_pure [Q]sbi_unfold_as_si_pure.
+    rewrite si_pure_entails. split.
+    - intros HPQ n. rewrite -(sbi_unfold_siProp_holds (P:=P)). intros.
+      (* FIXME: if we remove the [intros] we trigger a Coq anomaly. *)
+      rewrite -(sbi_unfold_siProp_holds (P:=Q)).
+      by apply HPQ.
+    - intros HPQ. split=> n. rewrite !sbi_unfold_siProp_holds. auto.
+  Qed.
+
+  Lemma sbi_unfold_equiv `{!UnfoldSbi P Pi, !UnfoldSbi Q Qi} :
+    (∀ n, Pi n ↔ Qi n) → P ⊣⊢ Q.
+  Proof. rewrite bi.equiv_entails !sbi_unfold_entails. naive_solver. Qed.
+
+  Lemma sbi_unfold_emp_valid `{!UnfoldSbi Q Qi} :
+    (∀ n, Qi n) ↔ ⊢ Q.
+  Proof.
+    rewrite [Q]sbi_unfold_as_si_pure si_pure_emp_valid. split.
+    - intros HQ. split=> n. rewrite !sbi_unfold_siProp_holds. auto.
+    - intros HQ n. rewrite -(sbi_unfold_siProp_holds (P:=Q)). apply HQ.
+      by siProp.unseal.
+  Qed.
+
+  Global Instance sbi_unfold_pure φ : UnfoldSbi ⌜ φ ⌝ (λ _, φ).
+  Proof. exists ⌜ φ ⌝%I; [|by siProp.unseal]. by rewrite si_pure_pure. Qed.
+
+  Global Instance sbi_unfold_internal_eq {A : ofe} (x y : A) :
+    UnfoldSbi (x ≡ y) (λ n, x ≡{n}≡ y).
+  Proof. exists (x ≡ y)%I; [done |rewrite /internal_eq; by siProp.unseal]. Qed.
+
+  Global Instance sbi_unfold_cmra_valid {A : cmra} (x : A) :
+    UnfoldSbi (✓ x) (λ n, ✓{n} x).
+  Proof. exists (✓ x)%I; [done|rewrite /bi_cmra_valid; by siProp.unseal]. Qed.
+
+  Global Instance sbi_unfold_si_pure Pi :
+    UnfoldSbi (<si_pure> Pi) (siProp_holds Pi).
+  Proof. by exists Pi. Qed.
+
+  Global Instance sbi_unfold_and P Q Pi Qi :
+    UnfoldSbi P Pi →
+    UnfoldSbi Q Qi →
+    UnfoldSbi (P ∧ Q) (λ n, Pi n ∧ Qi n).
+  Proof.
+    intros [Pii ??] [Qii ??]. exists (Pii ∧ Qii)%I.
+    - rewrite si_pure_and. by f_equiv.
+    - siProp.unseal. naive_solver.
+  Qed.
+
+  Global Instance sbi_unfold_or P Q Pi Qi :
+    UnfoldSbi P Pi →
+    UnfoldSbi Q Qi →
+    UnfoldSbi (P ∨ Q) (λ n, Pi n ∨ Qi n).
+  Proof.
+    intros [Pii ??] [Qii ??]. exists (Pii ∨ Qii)%I.
+    - rewrite si_pure_or. by f_equiv.
+    - siProp.unseal. naive_solver.
+  Qed.
+
+  Global Instance sbi_unfold_impl P Q Pi Qi :
+    UnfoldSbi P Pi →
+    UnfoldSbi Q Qi →
+    UnfoldSbi (P → Q) (λ n, ∀ n', n' ≤ n → Pi n' → Qi n').
+  Proof.
+    intros [Pii ??] [Qii ??]. exists (Pii → Qii)%I.
+    - rewrite si_pure_impl. by f_equiv.
+    - siProp.unseal. naive_solver.
+  Qed.
+
+  Global Instance sbi_unfold_iff P Q Pi Qi :
+    UnfoldSbi P Pi →
+    UnfoldSbi Q Qi →
+    UnfoldSbi (P ↔ Q) (λ n, ∀ n', n' ≤ n → Pi n' ↔ Qi n').
+  Proof.
+    intros [Pii ??] [Qii ??]. exists (Pii ↔ Qii)%I.
+    - rewrite si_pure_iff. by f_equiv.
+    - rewrite /bi_iff. siProp.unseal. naive_solver.
+  Qed.
+
+  Global Instance sbi_unfold_forall {A} (Φ : A → PROP) Φi :
+    (∀ x, UnfoldSbi (Φ x)  (Φi x)) →
+    UnfoldSbi (∀ x, Φ x) (λ n, ∀ x, Φi x n).
+  Proof.
+    intros HP. exists (∀ x, sbi_unfold_car (Φ x))%I.
+    - rewrite si_pure_forall. f_equiv=> x. apply HP.
+    - intros n. siProp.unseal. apply forall_proper=> x. apply HP.
+  Qed.
+
+  Global Instance sbi_unfold_exist {A} (Φ : A → PROP) Φi :
+    (∀ x, UnfoldSbi (Φ x)  (Φi x)) →
+    UnfoldSbi (∃ x, Φ x) (λ n, ∃ x, Φi x n).
+  Proof.
+    intros HP. exists (∃ x, sbi_unfold_car (Φ x))%I.
+    - rewrite si_pure_exist. f_equiv=> x. apply HP.
+    - intros n. siProp.unseal. f_equiv=> x. apply HP.
+  Qed.
+
+  Global Instance sbi_unfold_later P Pi :
+    UnfoldSbi P Pi →
+    UnfoldSbi (▷ P) (λ n, match n with 0 => True | S n' => Pi n' end).
+  Proof.
+    intros [Pii ??]. exists (â–· Pii)%I.
+    - rewrite si_pure_later. by f_equiv.
+    - siProp.unseal. by intros [].
+  Qed.
+End sbi_unfold.
+
+(** FIXME: better error reporting if unfolding fails *)
+Ltac sbi_unfold :=
+  lazymatch goal with
+  | |- ⊢ _ => apply sbi_unfold_emp_valid
+  | |- _ ⊣⊢ _ => apply sbi_unfold_equiv
+  | |- _ ⊢ _ => apply sbi_unfold_entails
+  | |- _ => fail "sbi_unfold: not a BI entailment"
+  end.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 964b4567a7d8b3e865252e171927da89aa1a6504..6af3878d3e3a52091b8e9e84dce7093d1882abbc 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -109,32 +109,31 @@ Class BiBUpdFUpd (PROP : bi) `{BiBUpd PROP, BiFUpd PROP} :=
   bupd_fupd E (P : PROP) : (|==> P) ⊢ |={E}=> P.
 Global Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
 
-Class BiBUpdPlainly (PROP : bi) `{!BiBUpd PROP, !BiPlainly PROP} :=
-  bupd_plainly (P : PROP) : (|==> ■ P) ⊢ P.
-Global Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
-
-(** These rules for the interaction between the [â– ] and [|={E1,E2=>] modalities
-only make sense for affine logics. From the axioms below, one could derive
-[■ P ={E}=∗ P] (see the lemma [fupd_plainly_elim]), which in turn gives
-[True ={E}=∗ emp]. *)
-Class BiFUpdPlainly (PROP : bi) `{!BiFUpd PROP, !BiPlainly PROP} := {
+Class BiBUpdSbi (PROP : bi) `{!BiBUpd PROP, !Sbi PROP} :=
+  bupd_si_pure Pi : (|==> <si_pure> Pi) ⊢@{PROP} <si_pure> Pi.
+Global Hint Mode BiBUpdSbi ! - - : typeclass_instances.
+
+(** These rules for the interaction between [<si_pure>] and the [|={E1,E2=>]
+modality only make sense for affine logics. For general BIs we do not know the
+canonical set of rules and linear models in which they might hold. *)
+Class BiFUpdSbi (PROP : bi) `{!BiFUpd PROP, !Sbi PROP} := {
   (** When proving a fancy update of a plain proposition, you can also prove it
   while being allowed to open all invariants. *)
-  fupd_plainly_mask_empty E (P : PROP) :
-    (|={E,∅}=> ■ P) ⊢ |={E}=> P;
+  fupd_si_pure_mask_empty E Pi :
+    (|={E,∅}=> <si_pure> Pi) ⊢@{PROP} |={E}=> <si_pure> Pi;
   (** A strong eliminator (a la modus ponens) for the wand-fancy-update with a
   plain conclusion: We eliminate [R ={E}=∗ ■ P] by supplying an [R], but we get
   to keep the [R]. *)
-  fupd_plainly_keep_l E (P R : PROP) :
-    (R ={E}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R;
+  fupd_si_pure_keep_l E Pi (R : PROP) :
+    (R ={E}=∗ <si_pure> Pi) ∗ R ⊢ |={E}=> <si_pure> Pi ∗ R;
   (** Later "almost" commutes with fancy updates over plain propositions. It
   commutes "almost" because of the â—‡ modality, which is needed in the definition
   of fancy updates so one can remove laters of timeless propositions. *)
-  fupd_plainly_later E (P : PROP) :
-    (▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P;
+  fupd_si_pure_later E Pi :
+    (▷ |={E}=> <si_pure> Pi) ⊢@{PROP} |={E}=> ▷ ◇ <si_pure> Pi;
   (** Forall quantifiers commute with fancy updates over plain propositions. *)
-  fupd_plainly_forall_2 E {A} (Φ : A → PROP) :
-    (∀ x, |={E}=> ■ Φ x) ⊢ |={E}=> ∀ x, Φ x
+  fupd_si_pure_forall_2 E {A} (Φi : A → siProp) :
+    (∀ x, |={E}=> <si_pure> Φi x) ⊢@{PROP} |={E}=> ∀ x, <si_pure> Φi x
 }.
 Global Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
 
@@ -251,12 +250,21 @@ Section bupd_derived.
   Proof. rewrite /Absorbing /bi_absorbingly bupd_frame_l =>-> //. Qed.
 
   Section bupd_plainly.
-    Context `{!BiPlainly PROP, !BiBUpdPlainly PROP}.
+    Context `{!Sbi PROP, !BiBUpdSbi PROP}.
 
-    Lemma bupd_elim P `{!Plain P} : (|==> P) ⊢ P.
-    Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
+    Lemma bupd_plainly P : (|==> ■ P) ⊢ ■ P.
+    Proof. apply bupd_si_pure. Qed.
 
-    Lemma bupd_plain_forall {A} (Φ : A → PROP) `{∀ x, Plain (Φ x)} :
+    Lemma bupd_plainly_elim P `{!Absorbing P} : (|==> ■ P) ⊢ P.
+    Proof. by rewrite bupd_plainly plainly_elim. Qed.
+
+    Lemma bupd_elim P `{!Plain P, !Absorbing P} : (|==> P) ⊢ P.
+    Proof.
+      by rewrite {1}(plain P) /plainly bupd_si_pure si_pure_si_emp_valid_elim.
+    Qed.
+
+    Lemma bupd_plain_forall {A} (Φ : A → PROP)
+        `{!∀ x, Plain (Φ x), !∀ x, Absorbing (Φ x)} :
       (|==> ∀ x, Φ x) ⊣⊢ (∀ x, |==> Φ x).
     Proof.
       apply (anti_symm _).
@@ -564,7 +572,26 @@ Section fupd_derived.
   Qed.
 
   Section fupd_plainly_derived.
-    Context `{!BiPlainly PROP, !BiFUpdPlainly PROP}.
+    Context `{!Sbi PROP, !BiFUpdSbi PROP, !BiAffine PROP}.
+
+    Lemma fupd_plainly_mask_empty E P : (|={E,∅}=> ■ P) ⊢ |={E}=> P.
+    Proof.
+      by rewrite /plainly fupd_si_pure_mask_empty si_pure_si_emp_valid_elim.
+    Qed.
+    Lemma fupd_plainly_keep_l E P R : (R ={E}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R.
+    Proof.
+      by rewrite /plainly fupd_si_pure_keep_l si_pure_si_emp_valid_elim.
+    Qed.
+    Lemma fupd_plainly_later E P : (▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P.
+    Proof.
+      by rewrite /plainly fupd_si_pure_later si_pure_si_emp_valid_elim.
+    Qed.
+    Lemma fupd_plainly_forall_2 E {A} (Φ : A → PROP) :
+      (∀ x, |={E}=> ■ Φ x) ⊢ |={E}=> ∀ x, Φ x.
+    Proof.
+      rewrite /plainly fupd_si_pure_forall_2.
+      by setoid_rewrite si_pure_si_emp_valid_elim; last apply _.
+    Qed.
 
     Lemma fupd_plainly_mask E E' P : (|={E,E'}=> ■ P) ⊢ |={E}=> P.
     Proof.
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 16d66473e3de0ce772ed5d67827fd3da712894b6..19927f313bb555d98a365e9d9661b6c6d10a0c09 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -175,7 +175,7 @@ Local Lemma wp_progress_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} es σ1 n κs t2
   not_stuck e2 σ2.
 Proof.
   intros Hwp ??.
-  eapply pure_soundness.
+  apply (pure_soundness (PROP:=iPropI Σ)).
   eapply (step_fupdN_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
     (steps_sum num_laters_per_step 0 n)).
   iIntros (Hinv) "Hcred".
@@ -233,7 +233,7 @@ Lemma wp_strong_adequacy_gen (hlc : has_lc) Σ Λ `{!invGpreS Σ} s es σ1 n κs
   φ.
 Proof.
   intros Hwp ?.
-  eapply pure_soundness.
+  apply (pure_soundness (PROP:=iPropI Σ)).
   eapply (step_fupdN_soundness_gen _ hlc (steps_sum num_laters_per_step 0 n)
     (steps_sum num_laters_per_step 0 n)).
   iIntros (Hinv) "Hcred".
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 1328984b2eeee93a3e95fd84564c36e99887d92c..2af658ae2a77588a3f62c1f51d7e5389b0f5b18c 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -133,7 +133,9 @@ Theorem twp_total Σ Λ `{!invGpreS Σ} s e σ Φ n :
        stateI σ n [] 0 ∗ WP e @ s; ⊤ [{ Φ }]) →
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
-  intros Hwp. eapply pure_soundness. apply (laterN_soundness _  1); simpl.
+  intros Hwp.
+  eapply (pure_soundness (PROP:=iPropI Σ)).
+  apply (laterN_soundness _ 1); simpl.
   apply (fupd_soundness_no_lc ⊤ ⊤ _ 0)=> Hinv. iIntros "_".
   iMod (Hwp) as (stateI num_laters_per_step fork_post stateI_mono) "[Hσ H]".
   set (iG := IrisG Hinv stateI fork_post num_laters_per_step stateI_mono).
diff --git a/iris/proofmode/class_instances_cmra_valid.v b/iris/proofmode/class_instances_cmra_valid.v
new file mode 100644
index 0000000000000000000000000000000000000000..f53d59ae3b2d36917cca6871ee8e06c9cf82b11f
--- /dev/null
+++ b/iris/proofmode/class_instances_cmra_valid.v
@@ -0,0 +1,18 @@
+From iris.proofmode Require Import modality_instances classes.
+From iris.prelude Require Import options.
+Import bi.
+
+Section class_instances_cmra_valid.
+  Context `{!Sbi PROP}.
+
+  Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
+    @IntoPure PROP (✓ a) (✓ a).
+  Proof. by rewrite /IntoPure bi_cmra_discrete_valid. Qed.
+
+  Global Instance from_pure_cmra_valid {A : cmra} (a : A) :
+    @FromPure PROP false (✓ a) (✓ a).
+  Proof.
+    rewrite /FromPure /=. eapply bi.pure_elim=> // ?.
+    rewrite -bi_cmra_valid_intro //.
+  Qed.
+End class_instances_cmra_valid.
diff --git a/iris/proofmode/class_instances_embedding.v b/iris/proofmode/class_instances_embedding.v
index ee84ce46d843193eae6fa032d404a8e68c91b6a2..a0f2df4a7027622f4c918a4667bd7a92ea28ef34 100644
--- a/iris/proofmode/class_instances_embedding.v
+++ b/iris/proofmode/class_instances_embedding.v
@@ -155,13 +155,13 @@ Global Instance from_modal_later_embed `{!BiEmbedLater PROP PROP'} φ `(sel : A)
 Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_laterN. Qed.
 
 Global Instance from_modal_plainly_embed
-    `{!BiPlainly PROP, !BiPlainly PROP', !BiEmbedPlainly PROP PROP'} φ `(sel : A) P Q :
+    `{!Sbi PROP, !Sbi PROP', !BiEmbedSbi PROP PROP'} φ `(sel : A) P Q :
   FromModal φ modality_plainly sel P Q →
   FromModal φ (PROP2:=PROP') modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
 Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_plainly. Qed.
 
 Global Instance into_internal_eq_embed
-    `{!BiInternalEq PROP, !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
+    `{!Sbi PROP, !Sbi PROP', !BiEmbedSbi PROP PROP'}
     {A : ofe} (x y : A) (P : PROP) :
   IntoInternalEq P x y → IntoInternalEq (⎡P⎤ : PROP')%I x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index c391c5bc55ce4a082af7485c942b88049de5cc0f..b34c7011801e19c51d7a773e0d258601701fad89 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -220,8 +220,8 @@ Proof.
   rewrite persistently_elim impl_elim_r //.
 Qed.
 
-Global Instance frame_eq_embed `{!BiEmbed PROP PROP', !BiInternalEq PROP,
-    !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
+Global Instance frame_eq_embed `{!BiEmbed PROP PROP', !Sbi PROP,
+    !Sbi PROP', !BiEmbedSbi PROP PROP'}
     p P Q (Q' : PROP') {A : ofe} (a b : A) :
   Frame p (a ≡ b) P Q → MakeEmbed Q Q' →
   Frame p (a ≡ b) ⎡P⎤ Q'. (* Default cost > 1 *)
diff --git a/iris/proofmode/class_instances_internal_eq.v b/iris/proofmode/class_instances_internal_eq.v
index b44a78702792432e1c5bc2cf470bc710b754de9f..9b8af6a068ca48b61e62358c355c2d220ee1a7dd 100644
--- a/iris/proofmode/class_instances_internal_eq.v
+++ b/iris/proofmode/class_instances_internal_eq.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
 Import bi.
 
 Section class_instances_internal_eq.
-Context `{!BiInternalEq PROP}.
+Context `{!Sbi PROP}.
 Implicit Types P Q R : PROP.
 
 (* When a user calls [iPureIntro] on [⊢ a ≡ b], the following instance turns
@@ -25,7 +25,7 @@ Proof. by rewrite /FromPure pure_internal_eq. Qed.
   The following instance implements above logic, while avoiding a double search
   for [Discrete a]. *)
 Global Instance into_pure_eq {A : ofe} (a b : A) (P : Prop) :
-  Discrete a →
+  TCOr (Discrete a) (Discrete b) →
   TCOr (TCAnd (LeibnizEquiv A) (TCEq P (a = b)))
        (TCEq P (a ≡ b)) →
   @IntoPure PROP (a ≡ b) P.
diff --git a/iris/proofmode/class_instances_plainly.v b/iris/proofmode/class_instances_plainly.v
index 0971f80cd2681716ba5cd883c0631061efb0010f..2861365041b0211033080effc16e69ebc403ae5b 100644
--- a/iris/proofmode/class_instances_plainly.v
+++ b/iris/proofmode/class_instances_plainly.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
 Import bi.
 
 Section class_instances_plainly.
-Context {PROP} `{!BiPlainly PROP}.
+Context `{!Sbi PROP}.
 Implicit Types P Q R : PROP.
 
 Global Instance from_assumption_plainly_l_true P Q :
@@ -67,7 +67,7 @@ Global Instance from_or_plainly P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (■ P) (■ Q1) (■ Q2).
 Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed.
 
-Global Instance into_or_plainly `{!BiPlainlyExist PROP} P Q1 Q2 :
+Global Instance into_or_plainly `{!SbiEmpValidExist PROP} P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (■ P) (■ Q1) (■ Q2).
 Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
 
@@ -75,7 +75,8 @@ Global Instance from_exist_plainly {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (■ P) (λ a, ■ (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
 
-Global Instance into_exist_plainly `{!BiPlainlyExist PROP} {A} P (Φ : A → PROP) name :
+Global Instance into_exist_plainly `{!SbiEmpValidExist PROP}
+    {A} P (Φ : A → PROP) name :
   IntoExist P Φ name → IntoExist (■ P) (λ a, ■ (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
 
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index d182711d91999aa8314a2699f30ddf0ea7db2ccc..8933f8b35c968bd552ff33327460b065d1b8f76c 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -100,7 +100,8 @@ Global Instance into_forall_fupd `{!BiFUpd PROP} {A} E1 E2 P (Φ : A → PROP) :
 Proof. rewrite /IntoForall=>->. apply fupd_forall. Qed.
 
 Global Instance from_forall_fupd
-    `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) name :
+    `{!BiFUpd PROP, !Sbi PROP, !BiFUpdSbi PROP, !BiAffine PROP}
+    E1 E2 {A} P (Φ : A → PROP) name :
   (* Some cases in which [E2 ⊆ E1] holds *)
   TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
   FromForall P Φ name → (∀ x, Plain (Φ x)) →
@@ -109,7 +110,8 @@ Proof.
   rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite fupd_plain_forall; set_solver.
 Qed.
 Global Instance from_forall_step_fupd
-    `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) name :
+    `{!BiFUpd PROP, !Sbi PROP, !BiFUpdSbi PROP, !BiAffine PROP}
+    E1 E2 {A} P (Φ : A → PROP) name :
   (* Some cases in which [E2 ⊆ E1] holds *)
   TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
   FromForall P Φ name → (∀ x, Plain (Φ x)) →
@@ -148,14 +150,14 @@ Proof.
 Qed.
 
 Global Instance elim_modal_bupd_plain_goal
-    `{!BiBUpd PROP, !BiPlainly PROP, !BiBUpdPlainly PROP} p P Q :
+    `{!BiBUpd PROP, !Sbi PROP, !BiBUpdSbi PROP, !BiAffine PROP} p P Q :
   Plain Q → ElimModal True p false (|==> P) P Q Q.
 Proof.
   intros. by rewrite /ElimModal intuitionistically_if_elim
     bupd_frame_r wand_elim_r bupd_elim.
 Qed.
 Global Instance elim_modal_bupd_plain
-    `{!BiBUpd PROP, !BiPlainly PROP, !BiBUpdPlainly PROP} p P Q :
+    `{!BiBUpd PROP, !Sbi PROP, !BiBUpdSbi PROP, !BiAffine PROP} p P Q :
   Plain P → ElimModal True p p (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_elim wand_elim_r. Qed.
 Global Instance elim_modal_bupd_fupd
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 94558ae4ba5fdd0b3cecc1663a689c1f8297de01..bffad6cf02843c1602d2185f100aacfd85f837dd 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -84,7 +84,7 @@ Proof. by exists φ. Qed.
 Global Hint Extern 0 (FromPureT _ _ _) =>
   notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
 
-Class IntoInternalEq `{BiInternalEq PROP} {A : ofe} (P : PROP) (x y : A) :=
+Class IntoInternalEq `{!Sbi PROP} {A : ofe} (P : PROP) (x y : A) :=
   into_internal_eq : P ⊢ x ≡ y.
 Global Arguments IntoInternalEq {_ _ _} _%I _%type_scope _%type_scope : simpl never.
 Global Arguments into_internal_eq {_ _ _} _%I _%type_scope _%type_scope {_}.
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index a7047a8e165ae492d86fb5ee0d70090c4592cb04..b55df9b94881178befa9ebe505da4d450d2d70ba 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -978,7 +978,7 @@ Proof.
 Qed.
 
 (** * Rewriting *)
-Lemma tac_rewrite `{!BiInternalEq PROP} Δ i p Pxy d Q :
+Lemma tac_rewrite `{!Sbi PROP} Δ i p Pxy d Q :
   envs_lookup i Δ = Some (p, Pxy) →
   ∀ {A : ofe} (x y : A) (Φ : A → PROP),
     IntoInternalEq Pxy x y →
@@ -992,7 +992,7 @@ Proof.
   destruct d; auto using internal_eq_sym.
 Qed.
 
-Lemma tac_rewrite_in `{!BiInternalEq PROP} Δ i p Pxy j q P d Q :
+Lemma tac_rewrite_in `{!Sbi PROP} Δ i p Pxy j q P d Q :
   envs_lookup i Δ = Some (p, Pxy) →
   envs_lookup j Δ = Some (q, P) →
   ∀ {A : ofe} (x y : A) (Φ : A → PROP),
diff --git a/iris/proofmode/modality_instances.v b/iris/proofmode/modality_instances.v
index 9206cd26d6adc76477a4205fd114ff785b397918..960b14655841446d4358a24528dd8caf29fc7335 100644
--- a/iris/proofmode/modality_instances.v
+++ b/iris/proofmode/modality_instances.v
@@ -46,13 +46,13 @@ Section modalities.
   Definition modality_embed `{!BiEmbed PROP PROP'} :=
     Modality _ modality_embed_mixin.
 
-  Lemma modality_plainly_mixin `{!BiPlainly PROP} :
+  Lemma modality_plainly_mixin `{!Sbi PROP} :
     modality_mixin (@plainly PROP _) (MIEnvForall Plain) MIEnvClear.
   Proof.
     split; simpl; split_and?; eauto using equiv_entails_1_2, plainly_intro,
       plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
   Qed.
-  Definition modality_plainly `{!BiPlainly PROP} :=
+  Definition modality_plainly `{!Sbi PROP} :=
     Modality _ modality_plainly_mixin.
 
   Lemma modality_laterN_mixin n :
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 8f61cdb17c5e6b949fb4b1efb797eff61bf27ce2..ec4aef597d739a43afd4d5da843b5f1be9237bd5 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -462,14 +462,14 @@ Global Instance add_modal_at_bupd_goal `{!BiBUpd PROP} φ 𝓟 𝓟' Q i :
   AddModal 𝓟 𝓟' (|==> Q i)%I → AddModal 𝓟 𝓟' ((|==> Q) i).
 Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
 
-Global Instance from_forall_monPred_at_plainly `{!BiPlainly PROP} i P Φ :
+Global Instance from_forall_monPred_at_plainly `{!Sbi PROP} i P Φ :
   (∀ i, MakeMonPredAt i P (Φ i)) →
   FromForall ((■ P) i) (λ j, ■ (Φ j))%I (to_ident_name idx).
 Proof.
   rewrite /FromForall /MakeMonPredAt=>HPΦ. rewrite monPred_at_plainly.
   by setoid_rewrite HPΦ.
 Qed.
-Global Instance into_forall_monPred_at_plainly `{!BiPlainly PROP} i P Φ :
+Global Instance into_forall_monPred_at_plainly `{!Sbi PROP} i P Φ :
   (∀ i, MakeMonPredAt i P (Φ i)) →
   IntoForall ((■ P) i) (λ j, ■ (Φ j))%I.
 Proof.
@@ -481,7 +481,7 @@ Global Instance is_except_0_monPred_at i P :
   IsExcept0 P → IsExcept0 (P i).
 Proof. rewrite /IsExcept0=>- [/(_ i)]. by rewrite monPred_at_except_0. Qed.
 
-Global Instance make_monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofe} (x y : A) i :
+Global Instance make_monPred_at_internal_eq `{!Sbi PROP} {A : ofe} (x y : A) i :
   MakeMonPredAt i (x ≡ y) (x ≡ y).
 Proof. by rewrite /MakeMonPredAt monPred_at_internal_eq. Qed.
 Global Instance make_monPred_at_except_0 i P 𝓠 :
@@ -497,7 +497,7 @@ Global Instance make_monPred_at_fupd `{!BiFUpd PROP} i E1 E2 P 𝓟 :
   MakeMonPredAt i P 𝓟 → MakeMonPredAt i (|={E1,E2}=> P) (|={E1,E2}=> 𝓟).
 Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
 
-Global Instance into_internal_eq_monPred_at `{!BiInternalEq PROP}
+Global Instance into_internal_eq_monPred_at `{!Sbi PROP}
     {A : ofe} (x y : A) P i :
   IntoInternalEq P x y → IntoInternalEq (P i) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite monPred_at_internal_eq. Qed.
diff --git a/iris/proofmode/proofmode.v b/iris/proofmode/proofmode.v
index 87ea29a1489e511721837715f21d1eaef0f09bff..cd984b96184822993135fb3e1d6b554247677ef4 100644
--- a/iris/proofmode/proofmode.v
+++ b/iris/proofmode/proofmode.v
@@ -1,4 +1,4 @@
-(** The main proofmode file that everyone should import.
+(** The main proofmode file thaet everyone should import.
 Unless you are working with the guts of the proofmode, do not import any other
 file from this folder! *)
 From iris.proofmode Require Export ltac_tactics.
@@ -6,7 +6,7 @@ From iris.proofmode Require Export ltac_tactics.
 these files. *)
 From iris.proofmode Require Import class_instances class_instances_later
   class_instances_updates class_instances_embedding
-  class_instances_plainly class_instances_internal_eq.
+  class_instances_plainly class_instances_internal_eq class_instances_cmra_valid.
 From iris.proofmode Require Import class_instances_frame class_instances_make.
 From iris.proofmode Require Import modality_instances.
 From iris.prelude Require Import options.
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index e86a2c1b04f2264609e11d90fa250a0212fff537..5d93c95df4bf065bca934927f919f3339383897f 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export interface extensions internal_eq plainly.
+From iris.bi Require Export interface extensions.
 From iris.si_logic Require Export siprop.
 From iris.prelude Require Import options.
 Import siProp_primitive.
@@ -136,36 +136,6 @@ Proof. exact: @pure_forall_2. Qed.
 Global Instance siProp_later_contractive : BiLaterContractive siPropI.
 Proof. exact: @later_contractive. Qed.
 
-Lemma siProp_internal_eq_mixin : BiInternalEqMixin siPropI (@siProp_internal_eq).
-Proof.
-  split.
-  - 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.
-Qed.
-Global Instance siProp_internal_eq : BiInternalEq siPropI :=
-  {| bi_internal_eq_mixin := siProp_internal_eq_mixin |}.
-
-Lemma siProp_plainly_mixin : BiPlainlyMixin siPropI siProp_plainly.
-Proof.
-  split; try done.
-  - solve_proper.
-  - (* P ⊢ ■ emp *)
-    intros P. by apply pure_intro.
-  - (* ■ P ∗ Q ⊢ ■ P *)
-    intros P Q. apply and_elim_l.
-Qed.
-Global Instance siProp_plainlyC : BiPlainly siPropI :=
-  {| bi_plainly_mixin := siProp_plainly_mixin |}.
-
-Global Instance siProp_prop_ext : BiPropExt siPropI.
-Proof. exact: prop_ext_2. Qed.
-
 (** extra BI instances *)
 
 Global Instance siProp_affine : BiAffine siPropI | 0.
@@ -174,42 +144,15 @@ Proof. intros P. exact: pure_intro. Qed.
 many lemmas that have [BiAffine] as a premise. *)
 Global Hint Immediate siProp_affine : core.
 
-Global Instance siProp_plain (P : siProp) : Plain P | 0.
-Proof. done. Qed.
 Global Instance siProp_persistent (P : siProp) : Persistent P.
 Proof. done. Qed.
 
-Global Instance siProp_plainly_exist_1 : BiPlainlyExist siPropI.
-Proof. done. Qed.
-
 (** Re-state/export soundness lemmas *)
 
 Module siProp.
 Section restate.
-  (** Equality *)
-  Global Instance internal_eq_ne (A : ofe) : NonExpansive2 (@siProp_internal_eq A).
-  Proof. apply internal_eq_ne. Qed.
-  Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ siProp_internal_eq a a.
-  Proof. apply internal_eq_refl. Qed.
-  Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → siProp) :
-    NonExpansive Ψ → siProp_internal_eq a b ⊢ Ψ a → Ψ b.
-  Proof. apply internal_eq_rewrite. Qed.
-  Lemma prop_ext_2 P Q : ((P → Q) ∧ (Q → P)) ⊢ siProp_internal_eq P Q.
-  Proof. apply prop_ext_2. Qed.
-
-  (** Validity *)
-  Global Instance cmra_valid_ne (A : cmra) : NonExpansive (@siProp_cmra_valid A).
-  Proof. apply cmra_valid_ne. Qed.
-
-  (** Consistency/soundness statements *)
-  Lemma pure_soundness φ : (⊢@{siPropI} ⌜ φ ⌝) → φ.
-  Proof. apply pure_soundness. Qed.
-
-  Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{siPropI} x ≡ y) → x ≡ y.
-  Proof. apply internal_eq_soundness. Qed.
-
-  Lemma later_soundness (P : siProp) : (⊢ ▷ P) → ⊢ P.
-  Proof. apply later_soundness. Qed.
+  (** The equality, validity, cmra valid, and soundness lemmas are restated for
+  any BI with equality in [bi.internal_eq] and TODO. *)
 
   (** We restate the unsealing lemmas so that they also unfold the BI layer. The
   sealing lemmas are partially applied so that they also work under binders. *)
@@ -231,22 +174,23 @@ Section restate.
   Proof. by rewrite -siprop.siProp_and_unseal. Qed.
   Local Lemma siProp_wand_unseal : bi_wand = @siprop.siProp_impl_def.
   Proof. by rewrite -siprop.siProp_impl_unseal. Qed.
-  Local Lemma siProp_plainly_unseal : plainly = @id siProp.
-  Proof. done. Qed.
   Local Lemma siProp_persistently_unseal : bi_persistently = @id siProp.
   Proof. done. Qed.
   Local Lemma siProp_later_unseal : bi_later = @siprop.siProp_later_def.
   Proof. by rewrite -siprop.siProp_later_unseal. Qed.
   Local Lemma siProp_internal_eq_unseal :
-    @internal_eq _ _ = @siprop.siProp_internal_eq_def.
-  Proof. by rewrite -siprop.siProp_internal_eq_unseal. Qed.
+    @siProp_internal_eq = @siprop.siProp_internal_eq_def.
+  Proof. apply siprop.siProp_internal_eq_unseal. Qed.
+  Local Lemma siProp_cmra_valid_unseal :
+    @siProp_cmra_valid = @siprop.siProp_cmra_valid_def.
+  Proof. apply siprop.siProp_cmra_valid_unseal. Qed.
 
   Local Definition siProp_unseal :=
     (siProp_emp_unseal, siProp_pure_unseal, siProp_and_unseal, siProp_or_unseal,
     siProp_impl_unseal, siProp_forall_unseal, siProp_exist_unseal,
     siProp_sep_unseal, siProp_wand_unseal,
-    siProp_plainly_unseal, siProp_persistently_unseal, siProp_later_unseal,
-    siProp_internal_eq_unseal).
+    siProp_persistently_unseal, siProp_later_unseal,
+    siProp_internal_eq_unseal, siProp_cmra_valid_unseal).
 End restate.
 
 (** The final unseal tactic that also unfolds the BI layer. *)
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index 5cd4b782873a33cffe4016282f7e2cf3a3b65ed4..43aad20af7e5765dfe3c777f42e2073316dd5756 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -274,17 +274,6 @@ Section primitive.
   Proof. unseal; intros HΨ; split=> n [a ?]; by apply HΨ with a. Qed.
 
   (** Later *)
-  Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
-  Proof.
-    unseal. split. intros [|n]; simpl; [done|].
-    intros Heq; apply Heq; auto.
-  Qed.
-  Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
-  Proof.
-    unseal. split. intros n Hn; split; intros m Hlt; simpl in *.
-    destruct n as [|n]; eauto using dist_le with si_solver.
-  Qed.
-
   Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
   Proof. unseal=> HP; split=>-[|n]; [done|apply HP; eauto using cmra_validN_S]. Qed.
   Lemma later_intro P : P ⊢ ▷ P.
@@ -310,24 +299,48 @@ Section primitive.
     intros Hnonexp. unseal; split=> n Hab n' ? HΨ. eapply Hnonexp with n a; auto.
   Qed.
 
-  Lemma fun_ext {A} {B : A → ofe} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g.
-  Proof. by unseal. Qed.
-  Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y.
-  Proof. by unseal. Qed.
-  Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
-  Proof. unseal=> ?. split=> n. by apply (discrete_iff n). Qed.
-
   Lemma prop_ext_2 P Q : ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
   Proof.
     unseal; split=> n /= HPQ. split=> n' ?.
     move: HPQ=> [] /(_ n') ? /(_ n'). naive_solver.
   Qed.
 
+  Lemma fun_extI {A} {B : A → ofe} (g1 g2 : discrete_fun B) :
+    (∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
+  Proof. by unseal. Qed.
+  Lemma sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sigO P) :
+    proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
+  Proof. by unseal. Qed.
+
+  Lemma later_equivI_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
+  Proof.
+    unseal. split. intros [|n]; simpl; [done|].
+    intros Heq; apply Heq; auto.
+  Qed.
+  Lemma later_equivI_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
+  Proof.
+    unseal. split. intros n ?; split; intros m Hlt; simpl in *.
+    destruct n as [|n]; first lia.
+    eauto using dist_le with si_solver.
+  Qed.
+
+  Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
+  Proof. unseal=> ?. split=> n. by apply (discrete_iff n). Qed.
+
+  Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
+    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
+  Proof. unseal. split; [by intros []|done]. Qed.
+
   (** Validity *)
   Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
   Proof. unseal=> ?; split=> n ? /=; by apply cmra_valid_validN. Qed.
+  Lemma cmra_valid_elim {A : cmra} (a : A) : ✓ a ⊢ ⌜ ✓{0} a ⌝.
+  Proof. unseal; split=> n ?; apply cmra_validN_le with n; auto with lia. Qed.
   Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
   Proof. unseal; split=> n; apply cmra_validN_op_l. Qed.
+  Lemma valid_entails {A B : cmra} (a : A) (b : B) :
+    (✓ a ⊢ ✓ b) ↔ ∀ n, ✓{n} a → ✓{n} b.
+  Proof. unseal. split; [by intros []|done]. Qed.
 
   (** Consistency/soundness statements *)
   Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index b06b4f1cbe3f40bad6e92b8a84aac74f30061949..80d71dd68adcdb7f664e68e8dad3ae539989d01f 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -62,7 +62,7 @@ Global Hint Extern 0 (lockG _) => progress simpl : typeclass_instances.
 Global Instance is_lock_contractive `{!heapGS_gen hlc Σ, !lock, !lockG Σ} γ lk :
   Contractive (is_lock γ lk).
 Proof.
-  apply (uPred.contractive_internal_eq (M:=iResUR Σ)).
+  apply (contractive_internal_eq (PROP:=iPropI Σ)).
   iIntros (P Q) "#HPQ". iApply prop_ext. iIntros "!>".
   iSplit; iIntros "H"; iApply (is_lock_iff with "H");
     iNext; iRewrite "HPQ"; auto.
diff --git a/iris_heap_lang/lib/rw_lock.v b/iris_heap_lang/lib/rw_lock.v
index 57060fd9814e4bde566e6519d7c2c0a4c3c0c8ec..100c271790203c08484f093034a68f13747352ff 100644
--- a/iris_heap_lang/lib/rw_lock.v
+++ b/iris_heap_lang/lib/rw_lock.v
@@ -89,7 +89,7 @@ Global Instance is_rw_lock_contractive `{!heapGS_gen hlc Σ, !rwlock, !rwlockG 
   Proper (pointwise_relation _ (dist_later n) ==> dist n) (is_rw_lock γ lk).
 Proof.
   assert (Contractive (is_rw_lock γ lk : (Qp -d> iPropO Σ) → _)) as Hcontr.
-  { apply (uPred.contractive_internal_eq (M:=iResUR Σ)); iIntros (Φ1 Φ2) "#HΦ".
+  { apply (contractive_internal_eq (PROP:=iPropI Σ)); iIntros (Φ1 Φ2) "#HΦ".
     rewrite discrete_fun_equivI.
     iApply plainly.prop_ext_2; iIntros "!>"; iSplit; iIntros "H";
       iApply (is_rw_lock_iff with "H");
diff --git a/iris_unstable/base_logic/algebra.v b/iris_unstable/base_logic/algebra.v
deleted file mode 100644
index 4e4cc8d590f0b9d9961995d9a3cda31b38b15a48..0000000000000000000000000000000000000000
--- a/iris_unstable/base_logic/algebra.v
+++ /dev/null
@@ -1,22 +0,0 @@
-(** This is just an integration file for [iris_staging.algebra.list];
-both should be stabilized together. *)
-From iris.algebra Require Import cmra.
-From iris.unstable.algebra Require Import list.
-From iris.base_logic Require Import bi derived.
-From iris.prelude Require Import options.
-
-Section upred.
-Context {M : ucmra}.
-
-(* 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).
-
-Section list_cmra.
-  Context {A : ucmra}.
-  Implicit Types l : list A.
-
-  Lemma list_validI l : ✓ l ⊣⊢ ∀ i, ✓ (l !! i).
-  Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
-End list_cmra.
-End upred.
diff --git a/iris_unstable/bi/algebra.v b/iris_unstable/bi/algebra.v
new file mode 100644
index 0000000000000000000000000000000000000000..a9bd6951d7580e84d49d26c861133aaeabe85967
--- /dev/null
+++ b/iris_unstable/bi/algebra.v
@@ -0,0 +1,22 @@
+(** This is just an integration file for [iris_staging.algebra.list];
+both should be stabilized together. *)
+From iris.algebra Require Import cmra.
+From iris.unstable.algebra Require Import list.
+From iris.bi Require Import algebra.
+From iris.prelude Require Import options.
+
+Section algebra.
+  Context `{!Sbi PROP}.
+
+  (* Force implicit argument [PROP] *)
+  Notation "P ⊢ Q" := (bi_entails (PROP:=PROP) P Q).
+  Notation "P ⊣⊢ Q" := (equiv (A:=PROP) P%I Q%I).
+
+  Section list_cmra.
+    Context {A : ucmra}.
+    Implicit Types l : list A.
+
+    Lemma list_validI l : ✓ l ⊣⊢ ∀ i, ✓ (l !! i).
+    Proof. sbi_unfold=> n. apply list_lookup_validN. Qed.
+  End list_cmra.
+End algebra.
diff --git a/tests/bi.ref b/tests/bi.ref
index 27b5cb7da314682827854e7c3ab45e03ea45a9bb..90f35a324108a07de684ff886ba150d8fdd8ce8e 100644
--- a/tests/bi.ref
+++ b/tests/bi.ref
@@ -12,11 +12,3 @@ P : PROP
 
 ?p : "Persistent (|==> P)"
 
-The command has indeed failed with message:
-Unable to satisfy the following constraints:
-In environment:
-PROP : bi
-P : PROP
-
-?p : "Persistent (â–  P)"
-
diff --git a/tests/bi.v b/tests/bi.v
index 3e38ccce0141b0fe4696c2d13840e7c2170ea205..a5c983dc2fd898419f2fc1b57041c8661f44fdbc 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -3,10 +3,10 @@ From iris.bi Require Import bi plainly big_op.
 Unset Mangle Names.
 
 (** See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/610 *)
-Lemma test_impl_persistent_1 `{!BiPlainly PROP, !BiPersistentlyImplPlainly PROP} :
+Lemma test_impl_persistent_1 `{!Sbi PROP, !BiPersistentlyImplSiPure PROP} :
   Persistent (PROP:=PROP) (True → True).
 Proof. apply _. Qed.
-Lemma test_impl_persistent_2 `{!BiPlainly PROP, !BiPersistentlyImplPlainly PROP} :
+Lemma test_impl_persistent_2 `{!Sbi PROP, !BiPersistentlyImplSiPure PROP} :
   Persistent (PROP:=PROP) (True → True → True).
 Proof. apply _. Qed.
 
@@ -66,7 +66,8 @@ Coq would unify [bupd_instance] with [persistently]. *)
 Goal ∀ {PROP : bi} (P : PROP),
   ∃ bupd_instance, Persistent (@bupd PROP bupd_instance P).
 Proof. intros. eexists _. Fail apply _. Abort.
-(* Similarly for [plainly]. *)
+(* Similarly for [plainly], but here it should leave the [Sbi] instance that
+was introduced by [eexists _] unshelved. *)
 Goal ∀ {PROP : bi} (P : PROP),
-  ∃ plainly_instance, Persistent (@plainly PROP plainly_instance P).
-Proof. intros. eexists _. Fail apply _. Abort.
+  ∃ sbi_instance, Persistent (@plainly PROP sbi_instance P).
+Proof. intros. eexists _. apply _. Unshelve. Abort.
diff --git a/tests/fixpoint.v b/tests/fixpoint.v
index b9e3c606fccd3026fbfdb45f9127c8726b2b965a..3f702078f786b308934d928207d60fbca9e60dbd 100644
--- a/tests/fixpoint.v
+++ b/tests/fixpoint.v
@@ -3,8 +3,7 @@ From iris.proofmode Require Import proofmode.
 From iris.prelude Require Import options.
 
 Section fixpoint.
-  Context {PROP : bi} `{!BiInternalEq PROP}
-    {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+  Context `{!Sbi PROP} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
 
   Definition L := bi_least_fixpoint F.
   Definition G := bi_greatest_fixpoint F.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e9f7005e0db6e44cce68360668dd5f0532003135..6176c58581c99cf074b58803c3c628b7b4119431 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -73,7 +73,7 @@ Check "test_iStopProof".
 Lemma test_iStopProof Q : emp -∗ Q -∗ Q.
 Proof. iIntros "#H1 H2". Show. iStopProof. Show. by rewrite bi.sep_elim_r. Qed.
 
-Lemma test_iRewrite `{!BiInternalEq PROP} {A : ofe} (x y : A) P :
+Lemma test_iRewrite `{!Sbi PROP} {A : ofe} (x y : A) P :
   □ (∀ z, P -∗ <affine> (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
 Proof.
   iIntros "#H1 H2".
@@ -82,7 +82,7 @@ Proof.
   auto.
 Qed.
 
-Lemma test_iRewrite_dom `{!BiInternalEq PROP} {A : ofe} (m1 m2 : gmap nat A) :
+Lemma test_iRewrite_dom `{!Sbi PROP} {A : ofe} (m1 m2 : gmap nat A) :
   m1 ≡ m2 ⊢@{PROP} ⌜ dom m1 = dom m2 ⌝.
 Proof. iIntros "H". by iRewrite "H". Qed.
 
@@ -297,7 +297,7 @@ Qed.
 Lemma test_iIntros_pure_not `{!BiPureForall PROP} : ⊢@{PROP} ⌜ ¬False ⌝.
 Proof. by iIntros (?). Qed.
 
-Lemma test_fast_iIntros `{!BiInternalEq PROP} P Q :
+Lemma test_fast_iIntros `{!Sbi PROP} P Q :
   ⊢ ∀ x y z : nat,
     ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x).
 Proof.
@@ -641,7 +641,7 @@ Proof.
   unshelve iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅); try apply _. done.
 Qed.
 
-Lemma test_iFrame_pure `{!BiInternalEq PROP} {A : ofe} (φ : Prop) (y z : A) :
+Lemma test_iFrame_pure `{!Sbi PROP} {A : ofe} (φ : Prop) (y z : A) :
   φ → <affine> ⌜y ≡ z⌝ -∗ (⌜ φ ⌝ ∧ ⌜ φ ⌝ ∧ y ≡ z : PROP).
 Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
 
@@ -848,7 +848,7 @@ Lemma test_iNext_quantifier {A} (Φ : A → A → PROP) :
   (∀ y, ∃ x, ▷ Φ x y) -∗ ▷ (∀ y, ∃ x, Φ x y).
 Proof. iIntros "H". iNext. done. Qed.
 
-Lemma text_iNext_Next `{!BiInternalEq PROP} {A B : ofe} (f : A -n> A) x y :
+Lemma text_iNext_Next `{!Sbi PROP} {A B : ofe} (f : A -n> A) x y :
   Next x ≡ Next y -∗ (Next (f x) ≡ Next (f y) : PROP).
 Proof. iIntros "H". iNext. by iRewrite "H". Qed.
 
@@ -985,7 +985,7 @@ Lemma test_apply_wand_below_let (Φ : nat → PROP) :
   Φ 5 -∗ Φ 5.
 Proof. iIntros "?". iApply lemma_for_test_apply_wand_below_let. done. Qed.
 
-Lemma test_iNext_iRewrite `{!BiInternalEq PROP} P Q :
+Lemma test_iNext_iRewrite `{!Sbi PROP} P Q :
   <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
 Proof.
   iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ".
@@ -1003,7 +1003,7 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
   x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P.
 Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
 
-Lemma test_iIntros_leibniz_equiv `{!BiInternalEq PROP} {A : ofe} (x y : A) :
+Lemma test_iIntros_leibniz_equiv `{!Sbi PROP} {A : ofe} (x y : A) :
   Discrete x → LeibnizEquiv A →
   x ≡ y ⊢@{PROP} ⌜x = y⌝.
 Proof.
@@ -1012,7 +1012,7 @@ Proof.
   done.
 Qed.
 
-Lemma test_iIntros_leibniz_equiv_prod `{!BiInternalEq PROP}
+Lemma test_iIntros_leibniz_equiv_prod `{!Sbi PROP}
     {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
   Discrete a1 → Discrete b1 → LeibnizEquiv A → LeibnizEquiv B →
   (a1, b1) ≡ (a2, b2) ⊢@{PROP} ⌜a1 = a2⌝.
@@ -1024,7 +1024,7 @@ Proof.
   done.
 Qed.
 
-Lemma test_iPureIntro_leibniz_equiv `{!BiInternalEq PROP}
+Lemma test_iPureIntro_leibniz_equiv `{!Sbi PROP}
     {A : ofe} `{!LeibnizEquiv A} (x y : A) :
   (x ≡ y) → ⊢@{PROP} x ≡ y.
 Proof.
@@ -1042,7 +1042,7 @@ Proof.
   otherwise. *)
 Qed.
 
-Lemma test_iNext_affine `{!BiInternalEq PROP} P Q :
+Lemma test_iNext_affine `{!Sbi PROP} P Q :
   <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
 Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
 
@@ -1306,11 +1306,11 @@ Proof.
   iExFalso. iExact "H".
 Qed.
 
-Lemma test_apply_affine_impl `{!BiPlainly PROP} (P : PROP) :
+Lemma test_apply_affine_impl `{!Sbi PROP} (P : PROP) :
   P -∗ (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q).
 Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
 
-Lemma test_apply_affine_wand `{!BiPlainly PROP} (P : PROP) :
+Lemma test_apply_affine_wand `{!Sbi PROP} (P : PROP) :
   P -∗ (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q).
 Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
 
@@ -1568,7 +1568,7 @@ Lemma test_entails_annot_sections_space_close P :
   (P ⊣⊢@{PROP} P ) ∧ (⊣⊢@{PROP} ) P P ∧ (.⊣⊢ P ) P.
 Proof. naive_solver. Qed.
 
-Lemma test_bi_internal_eq_annot_sections `{!BiInternalEq PROP} P :
+Lemma test_bi_internal_eq_annot_sections `{!Sbi PROP} P :
   ⊢@{PROP}
     P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P ∧
     ((P ≡@{PROP} P)) ∧ ((≡@{PROP})) P P ∧ ((P ≡.)) P ∧ ((.≡ P)) P ∧
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 9a9785e5768afcc21aeb646bef7029ad00283072..9a3dce8c79ac27b26fb2e1bbfd62585cf9f5120b 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -28,7 +28,7 @@ Section tests.
   Proof. iStartProof PROP. iIntros (i) "$". Qed.
   Lemma test_iStartProof_6 P : P ⊣⊢ P.
   Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
-  Lemma test_iStartProof_7 `{!BiInternalEq PROP} P : ⊢@{monPredI} P ≡ P.
+  Lemma test_iStartProof_7 `{!Sbi PROP} P : ⊢@{monPredI} P ≡ P.
   Proof. iStartProof PROP. done. Qed.
 
   Lemma test_intowand_1 P Q : (P -∗ Q) -∗ P -∗ Q.