diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 10f0a3b448d1cee136cd7316daaa3d7444bbb9bf..ca5a5ce2b6e1393220ab640c8c0dd93b04dd52ff 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -1,8 +1,7 @@
 From iris.base_logic.lib Require Export own.
 From stdpp Require Export coPset.
 From iris.base_logic.lib Require Import wsat.
-From iris.algebra Require Import gmap.
-From iris.proofmode Require Import tactics classes.
+From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Export invG.
 Import uPred.
@@ -10,18 +9,17 @@ Import uPred.
 Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   (wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I.
 Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
-Instance uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux.
-Definition uPred_fupd_eq `{invG Σ} : fupd = uPred_fupd_def := seal_eq uPred_fupd_aux.
+Definition uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux.
+Definition uPred_fupd_eq `{invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
+  seal_eq uPred_fupd_aux.
 
-Instance fupd_facts `{invG Σ} : FUpdFacts (uPredSI (iResUR Σ)).
+Lemma uPred_fupd_mixin `{invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd.
 Proof.
   split.
-  - apply _.
   - rewrite uPred_fupd_eq. solve_proper.
   - intros E1 E2 P (E1''&->&?)%subseteq_disjoint_union_L.
     rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
-      by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
-  - rewrite uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>".
+    by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
   - rewrite uPred_fupd_eq. iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
   - rewrite uPred_fupd_eq. iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
   - rewrite uPred_fupd_eq. iIntros (E1 E2 E3 P) "HP HwE".
@@ -42,3 +40,8 @@ Proof.
     iAssert (â–· â—‡ P)%I with "[-]" as "#$"; last by iFrame.
     iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
 Qed.
+Instance uPred_bi_fupd `{invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
+  {| bi_fupd_mixin := uPred_fupd_mixin |}.
+
+Instance uPred_bi_bupd_fupd `{invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
+Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index b7a6e372142ab0c2457de7b47a8fe8c31eeac952..6feffe22fcd7f48eae06b3d8bc490ad73390064f 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -336,7 +336,7 @@ Next Obligation.
   eauto using uPred_mono, cmra_includedN_l.
 Qed.
 Definition uPred_bupd_aux {M} : seal (@uPred_bupd_def M). by eexists. Qed.
-Instance uPred_bupd {M} : BUpd (uPred M) := unseal uPred_bupd_aux.
+Definition uPred_bupd {M} : BUpd (uPred M) := unseal uPred_bupd_aux.
 Definition uPred_bupd_eq {M} :
   @bupd _ uPred_bupd = @uPred_bupd_def M := seal_eq uPred_bupd_aux.
 
@@ -575,6 +575,30 @@ Coercion uPred_valid {M} : uPred M → Prop := bi_valid.
 (* Latest notation *)
 Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
 
+Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
+Proof.
+  split.
+  - intros n P Q HPQ.
+    unseal; split=> n' x; split; intros HP k yf ??;
+    destruct (HP k yf) as (x'&?&?); auto;
+    exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
+  - unseal. split=> n x ? HP k yf ?; exists x; split; first done.
+    apply uPred_mono with n x; eauto using cmra_validN_op_l.
+  - unseal. intros HPQ; split=> n x ? HP k yf ??.
+    destruct (HP k yf) as (x'&?&?); eauto.
+    exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
+  - unseal; split; naive_solver.
+  - unseal. split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
+    destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto.
+    { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
+    exists (x' â‹… x2); split; first by rewrite -assoc.
+    exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
+  - 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.
+Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
+
 Module uPred.
 Include uPred_unseal.
 Section uPred.
@@ -675,30 +699,6 @@ Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) :
   (✓ g : uPred M) ⊣⊢ ∀ i, ✓ g i.
 Proof. by uPred.unseal. Qed.
 
-(* Basic update modality *)
-Global Instance bupd_facts : BUpdFacts (uPredSI M).
-Proof.
-  split.
-  - intros n P Q HPQ.
-    unseal; split=> n' x; split; intros HP k yf ??;
-    destruct (HP k yf) as (x'&?&?); auto;
-    exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
-  - unseal. split=> n x ? HP k yf ?; exists x; split; first done.
-    apply uPred_mono with n x; eauto using cmra_validN_op_l.
-  - unseal. intros HPQ; split=> n x ? HP k yf ??.
-    destruct (HP k yf) as (x'&?&?); eauto.
-    exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
-  - unseal; split; naive_solver.
-  - unseal. split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
-    destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto.
-    { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
-    exists (x' â‹… x2); split; first by rewrite -assoc.
-    exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
-  - 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.
-
 Lemma bupd_ownM_updateP x (Φ : M → Prop) :
   x ~~>: Φ → uPred_ownM x ==∗ ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
 Proof.
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 74eeec2015722fd87c0a1d60c970699ee52ef1f5..59792e0f078dd27789103ede34947e5b74b4471e 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -3,7 +3,7 @@ From stdpp Require Import coPset.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition atomic_shift {PROP: sbi} `{!FUpd PROP} {A B : Type}
+Definition atomic_shift `{BiFUpd PROP} {A B : Type}
   (α : A → PROP) (* atomic pre-condition *)
   (β : A → B → PROP) (* atomic post-condition *)
   (Eo Em : coPset) (* outside/module masks *)
@@ -14,7 +14,7 @@ Definition atomic_shift {PROP: sbi} `{!FUpd PROP} {A B : Type}
           ((α x ={E∖Em, E}=∗ P) ∧ (∀ y, β x y ={E∖Em, E}=∗ Q x y)))
     )%I.
 
-Definition atomic_update {PROP: sbi} `{!FUpd PROP} {A B : Type}
+Definition atomic_update `{BiFUpd PROP} {A B : Type}
   (α : A → PROP) (* atomic pre-condition *)
   (β : A → B → PROP) (* atomic post-condition *)
   (Eo Em : coPset) (* outside/module masks *)
@@ -25,7 +25,7 @@ Definition atomic_update {PROP: sbi} `{!FUpd PROP} {A B : Type}
     )%I.
 
 Section lemmas.
-  Context {PROP: sbi} `{FUpdFacts PROP} {A B : Type}.
+  Context `{BiFUpd PROP} {A B : Type}.
   Implicit Types (α : A → PROP) (β: A → B → PROP) (P : PROP) (Q : A → B → PROP).
 
   Lemma aupd_acc α β Eo Em Q E :
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 36dcb9f0e560aa7b1c40ad81a830887d44a49796..aea516612d3538b7f06ad407ac76592bafe67091 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -205,8 +205,8 @@ Definition monPred_bupd_def `{BUpd PROP} (P : monPred) : monPred :=
      terms in logical terms. *)
   monPred_upclosed (λ i, |==> P i)%I.
 Definition monPred_bupd_aux `{BUpd PROP} : seal monPred_bupd_def. by eexists. Qed.
-Global Instance monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux.
-Definition monPred_bupd_eq `{BUpd PROP} : @bupd monPred _ = _ := seal_eq _.
+Definition monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux.
+Definition monPred_bupd_eq `{BUpd PROP} : @bupd _ monPred_bupd = _ := seal_eq _.
 End Bi.
 
 Arguments monPred_absolutely {_ _} _%I.
@@ -237,8 +237,8 @@ Definition monPred_fupd_def `{FUpd PROP} (E1 E2 : coPset) (P : monPred) : monPre
      terms in logical terms. *)
   monPred_upclosed (λ i, |={E1,E2}=> P i)%I.
 Definition monPred_fupd_aux `{FUpd PROP} : seal monPred_fupd_def. by eexists. Qed.
-Global Instance monPred_fupd `{FUpd PROP} : FUpd _ := unseal monPred_fupd_aux.
-Definition monPred_fupd_eq `{FUpd PROP} : @fupd monPred _ = _ := seal_eq _.
+Definition monPred_fupd `{FUpd PROP} : FUpd _ := unseal monPred_fupd_aux.
+Definition monPred_fupd_eq `{FUpd PROP} : @fupd _ monPred_fupd = _ := seal_eq _.
 End Sbi.
 
 Module MonPred.
@@ -411,7 +411,6 @@ Implicit Types i : I.
 Implicit Types P Q : monPred.
 
 (** Instances *)
-
 Global Instance monPred_at_mono :
   Proper ((⊢) ==> (⊑) ==> (⊢)) monPred_at.
 Proof. by move=> ?? [?] ?? ->. Qed.
@@ -802,17 +801,8 @@ Global Instance big_sepMS_absolute `{Countable A} (Φ : A → monPred)
   Absolute ([∗ mset] y ∈ X, Φ y)%I.
 Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply absolute_at. Qed.
 
-End bi_facts.
-
-Section sbi_facts.
-Context {I : biIndex} {PROP : sbi}.
-Local Notation monPred := (monPred I PROP).
-Local Notation monPredSI := (monPredSI I PROP).
-Implicit Types i : I.
-Implicit Types P Q : monPred.
-
 (** bupd *)
-Global Instance monPred_bupd_facts `{BUpdFacts PROP} : BUpdFacts monPredSI.
+Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
 Proof.
   split; unseal; unfold monPred_bupd_def, monPred_upclosed.
   (* Note: Notation is somewhat broken here. *)
@@ -828,24 +818,34 @@ Proof.
   - intros P. split=> /= i. rewrite bi.forall_elim bi.pure_impl_forall
       bi.forall_elim // -bi.plainly_forall bupd_plainly bi.forall_elim //.
 Qed.
+Global Instance monPred_bi_bupd `{BiBUpd PROP} : BiBUpd monPredI :=
+  {| bi_bupd_mixin := monPred_bupd_mixin |}.
 
-Lemma monPred_at_bupd `{BUpdFacts PROP} i P : (|==> P) i ⊣⊢ |==> P i.
+Lemma monPred_at_bupd `{BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i.
 Proof.
   unseal. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
   - rewrite !bi.forall_elim //.
   - do 2 apply bi.forall_intro=>?. by do 2 f_equiv.
 Qed.
-Global Instance bupd_absolute `{BUpdFacts PROP} P `{!Absolute P} :
+Global Instance bupd_absolute `{BiBUpd PROP} P `{!Absolute P} :
   Absolute (|==> P)%I.
 Proof. intros ??. by rewrite !monPred_at_bupd absolute_at. Qed.
 
-Lemma monPred_bupd_embed `{BUpdFacts PROP} (P : PROP) :
-  ⎡|==> P⎤ ⊣⊢ bupd (PROP:=monPredSI) ⎡P⎤.
+Lemma monPred_bupd_embed `{BiBUpd PROP} (P : PROP) :
+  ⎡|==> P⎤ ⊣⊢ bupd (PROP:=monPredI) ⎡P⎤.
 Proof.
   unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
   - by do 2 apply bi.forall_intro=>?.
   - rewrite !bi.forall_elim //.
 Qed.
+End bi_facts.
+
+Section sbi_facts.
+Context {I : biIndex} {PROP : sbi}.
+Local Notation monPred := (monPred I PROP).
+Local Notation monPredSI := (monPredSI I PROP).
+Implicit Types i : I.
+Implicit Types P Q : monPred.
 
 Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
 Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
@@ -865,16 +865,15 @@ Qed.
 Global Instance monPred_sbi_embedding : SbiEmbedding PROP monPredSI.
 Proof. split; try apply _; by unseal. Qed.
 
-Global Instance monPred_fupd_facts `{FUpdFacts PROP} : FUpdFacts monPredSI.
+Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredSI monPred_fupd.
 Proof.
-  split; first apply _; unseal; unfold monPred_fupd_def, monPred_upclosed.
+  split; unseal; unfold monPred_fupd_def, monPred_upclosed.
   (* Note: Notation is somewhat broken here. *)
   - intros E1 E2 n P Q HPQ. split=>/= i. by repeat f_equiv.
   - intros E1 E2 P HE12. split=>/= i.
     do 2 setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro=>?.
     rewrite (fupd_intro_mask E1 E2 (P i)) //. f_equiv.
     do 2 apply bi.forall_intro=>?. do 2 f_equiv. by etrans.
-  - intros E P. split=>/= i. by setoid_rewrite bupd_fupd.
   - intros E1 E2 P. split=>/= i. etrans; [apply bi.equiv_entails, bi.except_0_forall|].
     do 2 f_equiv. rewrite bi.pure_impl_forall bi.except_0_forall. do 2 f_equiv.
     by apply except_0_fupd.
@@ -893,15 +892,21 @@ Proof.
   - intros E P ?. split=>/= i. setoid_rewrite bi.pure_impl_forall.
     do 2 setoid_rewrite bi.later_forall. do 4 f_equiv. apply later_fupd_plain, _.
 Qed.
+Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredSI :=
+  {| bi_fupd_mixin := monPred_fupd_mixin |}.
+Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredSI.
+Proof.
+  rewrite /BiBUpdFUpd; unseal; unfold monPred_fupd_def, monPred_upclosed.
+  intros E P. split=>/= i. by setoid_rewrite bupd_fupd.
+Qed.
 
 (** Unfolding lemmas *)
-
 Lemma monPred_at_internal_eq {A : ofeT} i (a b : A) :
   @monPred_at I PROP (a ≡ b) i ⊣⊢ a ≡ b.
 Proof. by apply monPred_at_embed. Qed.
 Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
 Proof. by unseal. Qed.
-Lemma monPred_at_fupd `{FUpdFacts PROP} i E1 E2 P :
+Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
   (|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
 Proof.
   unseal. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
@@ -911,7 +916,7 @@ Qed.
 Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
 Proof. by unseal. Qed.
 
-Lemma monPred_fupd_embed `{FUpdFacts PROP} E1 E2 (P : PROP) :
+Lemma monPred_fupd_embed `{BiFUpd PROP} E1 E2 (P : PROP) :
   ⎡|={E1,E2}=> P⎤ ⊣⊢ fupd E1 E2 (PROP:=monPred) ⎡P⎤.
 Proof.
   unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
@@ -929,7 +934,6 @@ Proof.
 Qed.
 
 (** Absolute  *)
-
 Global Instance internal_eq_absolute {A : ofeT} (x y : A) :
   @Absolute I PROP (x ≡ y)%I.
 Proof. intros ??. by unseal. Qed.
@@ -941,8 +945,7 @@ Proof. induction n; apply _. Qed.
 Global Instance except0_absolute P `{!Absolute P} : Absolute (â—‡ P)%I.
 Proof. rewrite /sbi_except_0. apply _. Qed.
 
-Global Instance fupd_absolute E1 E2 P `{!Absolute P} `{FUpdFacts PROP} :
+Global Instance fupd_absolute E1 E2 P `{!Absolute P} `{BiFUpd PROP} :
   Absolute (|={E1,E2}=> P)%I.
 Proof. intros ??. by rewrite !monPred_at_fupd absolute_at. Qed.
-
 End sbi_facts.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index e84991291f1f38ab5290fe928f851f4f99507a9c..a7dbac7dac09d112d0c1ca0d4c9333f1e36ff572 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -1,6 +1,8 @@
 From stdpp Require Import coPset.
 From iris.bi Require Import interface derived_laws big_op.
 
+(* We first define operational type classes for the notations, and then later
+bundle these operational type classes with the laws. *)
 Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
 Instance : Params (@bupd) 2.
 Hint Mode BUpd ! : typeclass_instances.
@@ -35,7 +37,6 @@ Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
   (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
 
 (** Fancy updates that take a step. *)
-
 Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }â–·=>  Q") : bi_scope.
@@ -49,26 +50,102 @@ Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I
   (at level 99, E at level 50, Q at level 200,
    format "P  ={ E }▷=∗  Q") : bi_scope.
 
-(** BUpd facts  *)
-
-Class BUpdFacts (PROP : sbi) `{BUpd PROP} : Prop :=
-  { bupd_ne :> NonExpansive bupd;
-    bupd_intro (P : PROP) : P ==∗ P;
-    bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q;
-    bupd_trans (P : PROP) : (|==> |==> P) ==∗ P;
-    bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R;
-    bupd_plainly (P : PROP) : (|==> bi_plainly P) -∗ P }.
-Hint Mode BUpdFacts ! - : typeclass_instances.
+(** Bundled versions  *)
+Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
+  bi_bupd_mixin_bupd_ne : NonExpansive bupd;
+  bi_bupd_mixin_bupd_intro (P : PROP) : P ==∗ P;
+  bi_bupd_mixin_bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q;
+  bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) ==∗ P;
+  bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R;
+  bi_bupd_mixin_bupd_plainly (P : PROP) : (|==> bi_plainly P) -∗ P;
+}.
+
+Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := {
+  bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd E1 E2);
+  bi_fupd_mixin_fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
+  bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
+  bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q;
+  bi_fupd_mixin_fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P;
+  bi_fupd_mixin_fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
+    E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P;
+  bi_fupd_mixin_fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q;
+  bi_fupd_mixin_fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
+    E1 ⊆ E2 →
+    (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
+  bi_fupd_mixin_later_fupd_plain E (P : PROP) `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P;
+}.
+
+Class BiBUpd (PROP : bi) := {
+  bi_bupd_bupd :> BUpd PROP;
+  bi_bupd_mixin : BiBUpdMixin PROP bi_bupd_bupd;
+}.
+Hint Mode BiBUpd ! : typeclass_instances.
+Arguments bi_bupd_bupd : simpl never.
+
+Class BiFUpd (PROP : sbi) := {
+  bi_fupd_fupd :> FUpd PROP;
+  bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
+}.
+Hint Mode BiBUpd ! : typeclass_instances.
+Arguments bi_fupd_fupd : simpl never.
+
+Class BiBUpdFUpd (PROP : sbi) `{BiBUpd PROP, BiFUpd PROP} :=
+  bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P.
+
+Section bupd_laws.
+  Context `{BiBUpd PROP}.
+  Implicit Types P : PROP.
+
+  Global Instance bupd_ne : NonExpansive (@bupd PROP _).
+  Proof. eapply bi_bupd_mixin_bupd_ne, bi_bupd_mixin. Qed.
+  Lemma bupd_intro P : P ==∗ P.
+  Proof. eapply bi_bupd_mixin_bupd_intro, bi_bupd_mixin. Qed.
+  Lemma bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q.
+  Proof. eapply bi_bupd_mixin_bupd_mono, bi_bupd_mixin. Qed.
+  Lemma bupd_trans (P : PROP) : (|==> |==> P) ==∗ P.
+  Proof. eapply bi_bupd_mixin_bupd_trans, bi_bupd_mixin. Qed.
+  Lemma bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R.
+  Proof. eapply bi_bupd_mixin_bupd_frame_r, bi_bupd_mixin. Qed.
+  Lemma bupd_plainly (P : PROP) : (|==> bi_plainly P) -∗ P.
+  Proof. eapply bi_bupd_mixin_bupd_plainly, bi_bupd_mixin. Qed.
+End bupd_laws.
+
+Section fupd_laws.
+  Context `{BiFUpd PROP}.
+  Implicit Types P : PROP.
+
+  Global Instance fupd_ne E1 E2 : NonExpansive (@fupd PROP _ E1 E2).
+  Proof. eapply bi_fupd_mixin_fupd_ne, bi_fupd_mixin. Qed.
+  Lemma fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
+  Proof. eapply bi_fupd_mixin_fupd_intro_mask, bi_fupd_mixin. Qed.
+  Lemma except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P.
+  Proof. eapply bi_fupd_mixin_except_0_fupd, bi_fupd_mixin. Qed.
+  Lemma fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
+  Proof. eapply bi_fupd_mixin_fupd_mono, bi_fupd_mixin. Qed.
+  Lemma fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
+  Proof. eapply bi_fupd_mixin_fupd_trans, bi_fupd_mixin. Qed.
+  Lemma fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
+    E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
+  Proof. eapply bi_fupd_mixin_fupd_mask_frame_r', bi_fupd_mixin. Qed.
+  Lemma fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q.
+  Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.
+  Lemma fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
+    E1 ⊆ E2 →
+    (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+  Proof. eapply bi_fupd_mixin_fupd_plain'; eauto using bi_fupd_mixin. Qed.
+  Lemma later_fupd_plain E (P : PROP) `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P.
+  Proof. eapply bi_fupd_mixin_later_fupd_plain; eauto using bi_fupd_mixin. Qed.
+End fupd_laws.
 
 Section bupd_derived.
-  Context `{BUpdFacts PROP}.
-  Implicit Types P Q R: PROP.
+  Context `{BiBUpd PROP}.
+  Implicit Types P Q R : PROP.
 
   (* FIXME: Removing the `PROP:=` diverges. *)
-  Global Instance bupd_proper : Proper ((≡) ==> (≡)) (bupd (PROP:=PROP)) := ne_proper _.
+  Global Instance bupd_proper :
+    Proper ((≡) ==> (≡)) (bupd (PROP:=PROP)) := ne_proper _.
 
   (** BUpd derived rules *)
-
   Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (bupd (PROP:=PROP)).
   Proof. intros P Q; apply bupd_mono. Qed.
   Global Instance bupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (bupd (PROP:=PROP)).
@@ -88,44 +165,25 @@ Section bupd_derived.
   Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
 End bupd_derived.
 
-Lemma except_0_bupd {PROP : sbi} `{BUpdFacts PROP} (P : PROP) :
-  ◇ (|==> P) ⊢ (|==> ◇ P).
-Proof.
-  rewrite /sbi_except_0. apply bi.or_elim; eauto using bupd_mono, bi.or_intro_r.
-  by rewrite -bupd_intro -bi.or_intro_l.
-Qed.
-
-(** FUpd facts  *)
-
-(* Currently, this requires an SBI, because of [except_0_fupd] and
-   [later_fupd_plain]. If need be, we can generalize this to BIs by
-   extracting these propertes as lemmas to be proved by hand. *)
-Class FUpdFacts (PROP : sbi) `{BUpd PROP, FUpd PROP} : Prop :=
-  { fupd_bupd_facts :> BUpdFacts PROP;
-    fupd_ne E1 E2 :> NonExpansive (fupd E1 E2);
-    fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
-    bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P;
-    except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
-    fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q;
-    fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P;
-    fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
-      E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P;
-    fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q;
-    fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
-      E1 ⊆ E2 →
-      (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
-    later_fupd_plain E (P : PROP) `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P }.
-
-Hint Mode FUpdFacts ! - - : typeclass_instances.
+Section bupd_derived_sbi.
+  Context {PROP : sbi} `{BiBUpd PROP}.
+  Implicit Types P Q R : PROP.
+
+  Lemma except_0_bupd P : ◇ (|==> P) ⊢ (|==> ◇ P).
+  Proof.
+    rewrite /sbi_except_0. apply bi.or_elim; eauto using bupd_mono, bi.or_intro_r.
+    by rewrite -bupd_intro -bi.or_intro_l.
+  Qed.
+End bupd_derived_sbi.
 
 Section fupd_derived.
-  Context `{FUpdFacts PROP}.
-  Implicit Types P Q R: PROP.
+  Context `{BiFUpd PROP}.
+  Implicit Types P Q R : PROP.
 
-  Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
+  Global Instance fupd_proper E1 E2 :
+    Proper ((≡) ==> (≡)) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
 
   (** FUpd derived rules *)
-
   Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd (PROP:=PROP) E1 E2).
   Proof. intros P Q; apply fupd_mono. Qed.
   Global Instance fupd_flip_mono' E1 E2 :
@@ -133,7 +191,7 @@ Section fupd_derived.
   Proof. intros P Q; apply fupd_mono. Qed.
 
   Lemma fupd_intro E P : P ={E}=∗ P.
-  Proof. rewrite -bupd_fupd. apply bupd_intro. Qed.
+  Proof. by rewrite {1}(fupd_intro_mask E E P) // fupd_trans. Qed.
   Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> bi_emp (PROP:=PROP))%I.
   Proof. exact: fupd_intro_mask. Qed.
   Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
@@ -193,7 +251,6 @@ Section fupd_derived.
   Qed.
 
   (** Fancy updates that take a step derived rules. *)
-
   Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}▷=> P) -∗ (P -∗ Q) -∗ |={E1,E2}▷=> Q.
   Proof.
     apply bi.wand_intro_l.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 65ec13c6fc6ce20756abea1527b53a572c27ca8b..f4932f9ee8b9bea1d2dcc31c1f5d57e6518ade15 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -1103,10 +1103,10 @@ Global Instance from_assumption_except_0 p P Q :
   FromAssumption p P Q → FromAssumption p P (◇ Q)%I.
 Proof. rewrite /FromAssumption=>->. apply except_0_intro. Qed.
 
-Global Instance from_assumption_bupd `{BUpdFacts PROP} p P Q :
+Global Instance from_assumption_bupd `{BiBUpd PROP} p P Q :
   FromAssumption p P Q → FromAssumption p P (|==> Q).
 Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
-Global Instance from_assumption_fupd `{FUpdFacts PROP} E p P Q :
+Global Instance from_assumption_fupd `{BiBUpdFUpd PROP} E p P Q :
   FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I.
 Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
 
@@ -1121,10 +1121,10 @@ Proof. rewrite /FromPure=> ->. apply laterN_intro. Qed.
 Global Instance from_pure_except_0 a P φ : FromPure a P φ → FromPure a (◇ P) φ.
 Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.
 
-Global Instance from_pure_bupd `{BUpdFacts PROP} a P φ :
+Global Instance from_pure_bupd `{BiBUpd PROP} a P φ :
   FromPure a P φ → FromPure a (|==> P) φ.
 Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
-Global Instance from_pure_fupd `{FUpdFacts PROP} a E P φ :
+Global Instance from_pure_fupd `{BiFUpd PROP} a E P φ :
   FromPure a P φ → FromPure a (|={E}=> P) φ.
 Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
 
@@ -1161,39 +1161,39 @@ Proof.
              (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
 Qed.
 
-Global Instance into_wand_bupd `{BUpdFacts PROP} p q R P Q :
+Global Instance into_wand_bupd `{BiBUpd PROP} p q R P Q :
   IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
 Proof.
   rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
   apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
 Qed.
-Global Instance into_wand_bupd_persistent `{BUpdFacts PROP} p q R P Q :
+Global Instance into_wand_bupd_persistent `{BiBUpd PROP} p q R P Q :
   IntoWand false q R P Q → IntoWand p q (|==> R) P (|==> Q).
 Proof.
   rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
   apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
 Qed.
-Global Instance into_wand_bupd_args `{BUpdFacts PROP} p q R P Q :
+Global Instance into_wand_bupd_args `{BiBUpd PROP} p q R P Q :
   IntoWand p false R P Q → IntoWand' p q R (|==> P) (|==> Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => ->.
   apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r.
 Qed.
 
-Global Instance into_wand_fupd `{FUpdFacts PROP} E p q R P Q :
+Global Instance into_wand_fupd `{BiFUpd PROP} E p q R P Q :
   IntoWand false false R P Q →
   IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q).
 Proof.
   rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
   apply wand_intro_l. by rewrite fupd_sep wand_elim_r.
 Qed.
-Global Instance into_wand_fupd_persistent `{FUpdFacts PROP} E1 E2 p q R P Q :
+Global Instance into_wand_fupd_persistent `{BiFUpd PROP} E1 E2 p q R P Q :
   IntoWand false q R P Q → IntoWand p q (|={E1,E2}=> R) P (|={E1,E2}=> Q).
 Proof.
   rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
   apply wand_intro_l. by rewrite fupd_frame_l wand_elim_r.
 Qed.
-Global Instance into_wand_fupd_args `{FUpdFacts PROP} E1 E2 p q R P Q :
+Global Instance into_wand_fupd_args `{BiFUpd PROP} E1 E2 p q R P Q :
   IntoWand p false R P Q → IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => ->.
@@ -1222,10 +1222,10 @@ Global Instance from_sep_except_0 P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /FromSep=><-. by rewrite except_0_sep. Qed.
 
-Global Instance from_sep_bupd `{BUpdFacts PROP} P Q1 Q2 :
+Global Instance from_sep_bupd `{BiBUpd PROP} P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
 Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
-Global Instance from_sep_fupd `{FUpdFacts PROP} E P Q1 Q2 :
+Global Instance from_sep_fupd `{BiFUpd PROP} E P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
 Proof. rewrite /FromSep =><-. apply fupd_sep. Qed.
 
@@ -1286,13 +1286,13 @@ Global Instance from_or_except_0 P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /FromOr=><-. by rewrite except_0_or. Qed.
 
-Global Instance from_or_bupd `{BUpdFacts PROP} P Q1 Q2 :
+Global Instance from_or_bupd `{BiBUpd PROP} P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
 Proof.
   rewrite /FromOr=><-.
   apply or_elim; apply bupd_mono; auto using or_intro_l, or_intro_r.
 Qed.
-Global Instance from_or_fupd `{FUpdFacts PROP} E1 E2 P Q1 Q2 :
+Global Instance from_or_fupd `{BiFUpd PROP} E1 E2 P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
 Proof.
   rewrite /FromOr=><-. apply or_elim; apply fupd_mono;
@@ -1325,12 +1325,12 @@ Global Instance from_exist_except_0 {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (◇ P) (λ a, ◇ (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite except_0_exist_2. Qed.
 
-Global Instance from_exist_bupd `{BUpdFacts PROP} {A} P (Φ : A → PROP) :
+Global Instance from_exist_bupd `{BiBUpd PROP} {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
 Proof.
   rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
 Qed.
-Global Instance from_exist_fupd `{FUpdFacts PROP} {A} E1 E2 P (Φ : A → PROP) :
+Global Instance from_exist_fupd `{BiFUpd PROP} {A} E1 E2 P (Φ : A → PROP) :
   FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
 Proof.
   rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
@@ -1384,12 +1384,12 @@ Proof. by rewrite /IsExcept0 except_0_later. Qed.
 Global Instance is_except_0_embed `{SbiEmbedding PROP PROP'} P :
   IsExcept0 P → IsExcept0 ⎡P⎤.
 Proof. by rewrite /IsExcept0 -sbi_embed_except_0=>->. Qed.
-Global Instance is_except_0_bupd `{BUpdFacts PROP} P : IsExcept0 P → IsExcept0 (|==> P).
+Global Instance is_except_0_bupd `{BiBUpd PROP} P : IsExcept0 P → IsExcept0 (|==> P).
 Proof.
   rewrite /IsExcept0=> HP.
   by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
 Qed.
-Global Instance is_except_0_fupd `{FUpdFacts PROP} E1 E2 P :
+Global Instance is_except_0_fupd `{BiFUpd PROP} E1 E2 P :
   IsExcept0 (|={E1,E2}=> P).
 Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
 
@@ -1403,10 +1403,10 @@ Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_except_0 P : FromModal modality_id (â—‡ P) (â—‡ P) P.
 Proof. by rewrite /FromModal /= -except_0_intro. Qed.
 
-Global Instance from_modal_bupd `{BUpdFacts PROP} P :
+Global Instance from_modal_bupd `{BiBUpd PROP} P :
   FromModal modality_id (|==> P) (|==> P) P.
 Proof. by rewrite /FromModal /= -bupd_intro. Qed.
-Global Instance from_modal_fupd E P `{FUpdFacts PROP} :
+Global Instance from_modal_fupd E P `{BiFUpd PROP} :
   FromModal modality_id (|={E}=> P) (|={E}=> P) P.
 Proof. by rewrite /FromModal /= -fupd_intro. Qed.
 
@@ -1467,21 +1467,21 @@ Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)%I).
   by rewrite (into_except_0 P) -except_0_sep wand_elim_r.
 Qed.
-Global Instance elim_modal_bupd `{BUpdFacts PROP} P Q :
+Global Instance elim_modal_bupd `{BiBUpd PROP} P Q :
   ElimModal True (|==> P) P (|==> Q) (|==> Q).
 Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
-Global Instance elim_modal_bupd_plain_goal `{BUpdFacts PROP} P Q :
+Global Instance elim_modal_bupd_plain_goal `{BiBUpd PROP} P Q :
   Plain Q → ElimModal True (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
-Global Instance elim_modal_bupd_plain `{BUpdFacts PROP} P Q :
+Global Instance elim_modal_bupd_plain `{BiBUpd PROP} P Q :
   Plain P → ElimModal True (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
-Global Instance elim_modal_bupd_fupd `{FUpdFacts PROP} E1 E2 P Q :
+Global Instance elim_modal_bupd_fupd `{BiBUpdFUpd PROP} E1 E2 P Q :
   ElimModal True (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
 Proof.
   by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
 Qed.
-Global Instance elim_modal_fupd_fupd `{FUpdFacts PROP} E1 E2 E3 P Q :
+Global Instance elim_modal_fupd_fupd `{BiFUpd PROP} E1 E2 E3 P Q :
   ElimModal True (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
 Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 
@@ -1510,9 +1510,9 @@ Proof.
   by rewrite -except_0_sep wand_elim_r except_0_later.
 Qed.
 
-Global Instance add_modal_bupd `{BUpdFacts PROP} P Q : AddModal (|==> P) P (|==> Q).
+Global Instance add_modal_bupd `{BiBUpd PROP} P Q : AddModal (|==> P) P (|==> Q).
 Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
-Global Instance add_modal_fupd `{FUpdFacts PROP} E1 E2 P Q :
+Global Instance add_modal_fupd `{BiFUpd PROP} E1 E2 P Q :
   AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
 Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 
@@ -1546,10 +1546,10 @@ Proof.
   by rewrite laterN_affinely_persistently_if_2 laterN_sep.
 Qed.
 
-Global Instance frame_bupd `{BUpdFacts PROP} p R P Q :
+Global Instance frame_bupd `{BiBUpd PROP} p R P Q :
   Frame p R P Q → KnownFrame p R (|==> P) (|==> Q).
 Proof. rewrite /KnownFrame /Frame=><-. by rewrite bupd_frame_l. Qed.
-Global Instance frame_fupd `{FUpdFacts PROP} p E1 E2 R P Q :
+Global Instance frame_fupd `{BiFUpd PROP} p E1 E2 R P Q :
   Frame p R P Q → KnownFrame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
 Proof. rewrite /KnownFrame /Frame=><-. by rewrite fupd_frame_l. Qed.
 
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index d60a2635dab284e36feb439b4d75d49e25c1229b..2eb561cc2e8f8cbabb7d2027ea40a2261642e6d3 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -116,6 +116,9 @@ Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) ⌜i ⊑
 Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed.
 Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100.
 Proof. by rewrite /MakeMonPredAt. Qed.
+Global Instance make_monPred_at_bupd `{BiBUpd PROP} i P 𝓟 :
+  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (|==> P)%I (|==> 𝓟)%I.
+Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
 
 Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
   MakeMonPredAt i P 𝓟 → IsBiIndexRel j i → FromAssumption p (P j) 𝓟.
@@ -359,6 +362,32 @@ Qed.
 Global Instance into_embed_absolute P :
   Absolute P → IntoEmbed P (∀ i, P i).
 Proof. rewrite /IntoEmbed=> ?. by rewrite {1}(absolute_absolutely P). Qed.
+
+Global Instance elim_modal_embed_bupd_goal `{BiBUpd PROP} φ P P' 𝓠 𝓠' :
+  ElimModal φ P P' (|==> ⎡𝓠⎤)%I (|==> ⎡𝓠'⎤)%I →
+  ElimModal φ P P' ⎡|==> 𝓠⎤ ⎡|==> 𝓠'⎤.
+Proof. by rewrite /ElimModal !monPred_bupd_embed. Qed.
+Global Instance elim_modal_embed_bupd_hyp `{BiBUpd PROP} φ 𝓟 P' Q Q' :
+  ElimModal φ (|==> ⎡𝓟⎤)%I P' Q Q' →
+  ElimModal φ ⎡|==> 𝓟⎤ P' Q Q'.
+Proof. by rewrite /ElimModal monPred_bupd_embed. Qed.
+
+Global Instance add_modal_embed_bupd_goal `{BiBUpd PROP} P P' 𝓠 :
+  AddModal P P' (|==> ⎡𝓠⎤)%I → AddModal P P' ⎡|==> 𝓠⎤.
+Proof. by rewrite /AddModal !monPred_bupd_embed. Qed.
+
+Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ 𝓟 𝓟' Q Q' i :
+  ElimModal φ 𝓟 𝓟' (|==> Q i) (|==> Q' i) →
+  ElimModal φ 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
+Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
+Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ P 𝓟' 𝓠 𝓠' i:
+  ElimModal φ (|==> P i) 𝓟' 𝓠 𝓠' →
+  ElimModal φ ((|==> P) i) 𝓟' 𝓠 𝓠'.
+Proof. by rewrite /ElimModal monPred_at_bupd. Qed.
+
+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.
 End bi.
 
 (* When P and/or Q are evars when doing typeclass search on [IntoWand
@@ -407,10 +436,7 @@ Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed.
 Global Instance make_monPred_at_laterN i n P 𝓠 :
   MakeMonPredAt i P 𝓠 → MakeMonPredAt i (▷^n P)%I (▷^n 𝓠)%I.
 Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed.
-Global Instance make_monPred_at_bupd `{BUpdFacts PROP} i P 𝓟 :
-  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (|==> P)%I (|==> 𝓟)%I.
-Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
-Global Instance make_monPred_at_fupd `{FUpdFacts PROP} i E1 E2 P 𝓟 :
+Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P 𝓟 :
   MakeMonPredAt i P 𝓟 → MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> 𝓟)%I.
 Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
 
@@ -440,55 +466,29 @@ Proof.
   by rewrite monPred_at_later.
 Qed.
 
-Global Instance elim_modal_embed_bupd_goal `{BUpdFacts PROP} φ P P' 𝓠 𝓠' :
-  ElimModal φ P P' (|==> ⎡𝓠⎤)%I (|==> ⎡𝓠'⎤)%I →
-  ElimModal φ P P' ⎡|==> 𝓠⎤ ⎡|==> 𝓠'⎤.
-Proof. by rewrite /ElimModal !monPred_bupd_embed. Qed.
-Global Instance elim_modal_embed_bupd_hyp `{BUpdFacts PROP} φ 𝓟 P' Q Q' :
-  ElimModal φ (|==> ⎡𝓟⎤)%I P' Q Q' →
-  ElimModal φ ⎡|==> 𝓟⎤ P' Q Q'.
-Proof. by rewrite /ElimModal monPred_bupd_embed. Qed.
-
-Global Instance add_modal_embed_bupd_goal `{BUpdFacts PROP} P P' 𝓠 :
-  AddModal P P' (|==> ⎡𝓠⎤)%I → AddModal P P' ⎡|==> 𝓠⎤.
-Proof. by rewrite /AddModal !monPred_bupd_embed. Qed.
-
-Global Instance elim_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q Q' i :
-  ElimModal φ 𝓟 𝓟' (|==> Q i) (|==> Q' i) →
-  ElimModal φ 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
-Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
-Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} φ P 𝓟' 𝓠 𝓠' i:
-  ElimModal φ (|==> P i) 𝓟' 𝓠 𝓠' →
-  ElimModal φ ((|==> P) i) 𝓟' 𝓠 𝓠'.
-Proof. by rewrite /ElimModal monPred_at_bupd. Qed.
-
-Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q i :
-  AddModal 𝓟 𝓟' (|==> Q i)%I → AddModal 𝓟 𝓟' ((|==> Q) i).
-Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
-
-Global Instance elim_modal_embed_fupd_goal `{FUpdFacts PROP} φ E1 E2 E3 P P' 𝓠 𝓠' :
+Global Instance elim_modal_embed_fupd_goal `{BiFUpd PROP} φ E1 E2 E3 P P' 𝓠 𝓠' :
   ElimModal φ P P' (|={E1,E3}=> ⎡𝓠⎤)%I (|={E2,E3}=> ⎡𝓠'⎤)%I →
   ElimModal φ P P' ⎡|={E1,E3}=> 𝓠⎤ ⎡|={E2,E3}=> 𝓠'⎤.
 Proof. by rewrite /ElimModal !monPred_fupd_embed. Qed.
-Global Instance elim_modal_embed_fupd_hyp `{FUpdFacts PROP} φ E1 E2 𝓟 P' Q Q' :
+Global Instance elim_modal_embed_fupd_hyp `{BiFUpd PROP} φ E1 E2 𝓟 P' Q Q' :
   ElimModal φ (|={E1,E2}=> ⎡𝓟⎤)%I P' Q Q' →
   ElimModal φ ⎡|={E1,E2}=> 𝓟⎤ P' Q Q'.
 Proof. by rewrite /ElimModal monPred_fupd_embed. Qed.
 
-Global Instance add_modal_embed_fupd_goal `{FUpdFacts PROP} E1 E2 P P' 𝓠 :
+Global Instance add_modal_embed_fupd_goal `{BiFUpd PROP} E1 E2 P P' 𝓠 :
   AddModal P P' (|={E1,E2}=> ⎡𝓠⎤)%I → AddModal P P' ⎡|={E1,E2}=> 𝓠⎤.
 Proof. by rewrite /AddModal !monPred_fupd_embed. Qed.
 
-Global Instance elim_modal_at_fupd_goal `{FUpdFacts PROP} φ E1 E2 E3 𝓟 𝓟' Q Q' i :
+Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} φ E1 E2 E3 𝓟 𝓟' Q Q' i :
   ElimModal φ 𝓟 𝓟' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) →
   ElimModal φ 𝓟 𝓟' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).
 Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
-Global Instance elim_modal_at_fupd_hyp `{FUpdFacts PROP} φ E1 E2 P 𝓟' 𝓠 𝓠' i :
+Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ E1 E2 P 𝓟' 𝓠 𝓠' i :
   ElimModal φ (|={E1,E2}=> P i) 𝓟' 𝓠 𝓠' →
   ElimModal φ ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
 Proof. by rewrite /ElimModal monPred_at_fupd. Qed.
 
-Global Instance add_modal_at_fupd_goal `{FUpdFacts PROP} E1 E2 𝓟 𝓟' Q i :
+Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 𝓟 𝓟' Q i :
   AddModal 𝓟 𝓟' (|={E1,E2}=> Q i) → AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
 Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
 
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index ae928b8abccf2b7f9cc1eee8a80b5733fd3d2001..5ae50a06ebd978e0ce85aaeb0ebdf2650f0439ac 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -96,21 +96,15 @@ Section tests.
      ignore hint modes. So we assume the instances in a way that
      cannot be used by type class resolution, and then declare the
      instance. as such. *)
-  Context (BU0 : BUpd PROP * unit).
-  Instance BU : BUpd PROP := fst BU0.
-  Context (FU0 : FUpd PROP * unit).
-  Instance FU : FUpd PROP := fst FU0.
-  Context (FUF0 : FUpdFacts PROP * unit).
-  Instance FUF : FUpdFacts PROP := fst FUF0.
+  Context (FU0 : BiFUpd PROP * unit).
+  Instance FU : BiFUpd PROP := fst FU0.
 
   Lemma test_apply_fupd_intro_mask E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
-  Proof. iIntros. by iApply fupd_intro_mask. Qed.
+  Proof. iIntros. by iApply @fupd_intro_mask. Qed.
   Lemma test_apply_fupd_intro_mask_2 E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
-  Proof.
-    iIntros. iFrame. by iApply fupd_intro_mask'.
-  Qed.
+  Proof. iIntros. iFrame. by iApply @fupd_intro_mask'. Qed.
 
   Lemma test_iFrame_embed_persistent (P : PROP) (Q: monPred) :
     Q ∗ □ ⎡P⎤ ⊢ Q ∗ ⎡P ∗ P⎤.
@@ -121,5 +115,4 @@ Section tests.
   Lemma test_iNext_Bi P :
     @bi_entails monPredI (â–· P) (â–· P).
   Proof. iIntros "H". by iNext. Qed.
-
 End tests.