diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 61a43216a2d60abcb382fd26ebf4017bf41730f4..bcc18e6fda4d8a48ed5b88d814decf7fa6cff062 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -23,23 +23,14 @@ Hint Immediate True_intro False_elim : I.
 Hint Immediate iff_refl internal_eq_refl : I.
 
 (* Setup of the proof mode *)
-Hint Extern 1 (coq_tactics.envs_entails _ (|==> _)) => iModIntro.
-
 Section class_instances.
 Context {M : ucmraT}.
 Implicit Types P Q R : uPred M.
 
-Global Instance from_assumption_bupd p P Q :
-  FromAssumption p P Q → FromAssumption p P (|==> Q).
-Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
-
 Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
   @IntoPure (uPredI M) (✓ a) (✓ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
-Global Instance from_pure_bupd P φ : FromPure P φ → FromPure (|==> P) φ.
-Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
-
 Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
   @FromPure (uPredI M) (✓ a) (✓ a).
 Proof.
@@ -47,27 +38,6 @@ Proof.
   rewrite -cmra_valid_intro //. by apply pure_intro.
 Qed.
 
-Global Instance into_wand_bupd 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 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 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.
-
 (* FromOp *)
 (* TODO: Worst case there could be a lot of backtracking on these instances,
 try to refactor. *)
@@ -110,45 +80,4 @@ Qed.
 Global Instance into_sep_ownM (a b1 b2 : M) :
   IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
 Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
-
-Global Instance from_sep_bupd P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
-Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
-
-Global Instance from_or_bupd 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_exist_bupd {A} P (Φ : A → uPred M) :
-  FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
-Proof.
-  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
-Qed.
-
-Global Instance from_modal_bupd P : FromModal (|==> P) P.
-Proof. apply bupd_intro. Qed.
-
-Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
-Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
-
-Global Instance elim_modal_bupd_plain_goal P Q : Plain Q → ElimModal (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
-
-Global Instance elim_modal_bupd_plain P Q : Plain P → ElimModal (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
-
-Global Instance add_modal_bupd P Q : AddModal (|==> P) P (|==> Q).
-Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
-
-Global Instance is_except_0_bupd 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 frame_bupd p R P Q : Frame p R P Q → Frame p R (|==> P) (|==> Q).
-Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
 End class_instances.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 52d0bb0165c8611bea1e9ce8a34a99ce702ff93a..0972828f21cd098bb28f9c521b88b4f5955de0b5 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -40,31 +40,11 @@ Proof.
   rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.
   apply:persistently_cmra_valid_1.
 Qed.
-
-(** * Derived rules *)
-Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@bupd _ (@uPred_bupd M)).
-Proof. intros P Q; apply bupd_mono. Qed.
-Global Instance bupd_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@bupd _ (@uPred_bupd M)).
-Proof. intros P Q; apply bupd_mono. Qed.
-Lemma bupd_frame_l R Q : (R ∗ |==> Q) ==∗ R ∗ Q.
-Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
-Lemma bupd_wand_l P Q : (P -∗ Q) ∗ (|==> P) ==∗ Q.
-Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
-Lemma bupd_wand_r P Q : (|==> P) ∗ (P -∗ Q) ==∗ Q.
-Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
-Lemma bupd_sep P Q : (|==> P) ∗ (|==> Q) ==∗ P ∗ Q.
-Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
 Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y.
 Proof.
   intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
   by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
 Qed.
-Lemma except_0_bupd P : ◇ (|==> P) ⊢ (|==> ◇ P).
-Proof.
-  rewrite /sbi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
-  by rewrite -bupd_intro -or_intro_l.
-Qed.
 
 (* Timeless instances *)
 Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
@@ -84,12 +64,6 @@ Global Instance cmra_valid_plain {A : cmraT} (a : A) :
   Plain (✓ a : uPred M)%I.
 Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
 
-Lemma bupd_affinely_plainly P : (|==> ■ P) ⊢ P.
-Proof. by rewrite affine_affinely bupd_plainly. Qed.
-
-Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
-Proof. by rewrite -{1}(plain_plainly P) bupd_plainly. Qed.
-
 (* Persistence *)
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
   Persistent (✓ a : uPred M)%I.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 7e9b763a987308a8578ed1a41fc475ae7e9e3e0e..10f0a3b448d1cee136cd7316daaa3d7444bbb9bf 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -13,237 +13,32 @@ 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.
 
-Section fupd.
-Context `{invG Σ}.
-Implicit Types P Q : iProp Σ.
-
-Global Instance fupd_ne E1 E2 : NonExpansive (fupd E1 E2).
-Proof. rewrite uPred_fupd_eq. solve_proper. Qed.
-Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (fupd E1 E2).
-Proof. apply ne_proper, _. Qed.
-
-Lemma fupd_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
-Proof.
-  intros (E1''&->&?)%subseteq_disjoint_union_L.
-  rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
-  by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
-Qed.
-
-Lemma except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P.
-Proof. rewrite uPred_fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
-
-Lemma bupd_fupd E P : (|==> P) ={E}=∗ P.
-Proof. rewrite uPred_fupd_eq. by iIntros ">? [$ $] !> !>". Qed.
-
-Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
-Proof.
-  rewrite uPred_fupd_eq. iIntros (HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
-Qed.
-
-Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
-Proof.
-  rewrite uPred_fupd_eq. iIntros "HP HwE".
-  iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
-Qed.
-
-Lemma fupd_mask_frame_r' E1 E2 Ef P :
-  E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
-Proof.
-  intros. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
-  iIntros "Hvs (Hw & HE1 &HEf)".
-  iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
-  iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
-  iIntros "!> !>". by iApply "HP".
-Qed.
-
-Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q.
-Proof. rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros "[HwP $]". Qed.
-
-Lemma fupd_plain' E1 E2 E2' P Q `{!Plain P} :
-  E1 ⊆ E2 →
-  (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
-Proof.
-  iIntros ((E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
-  rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
-  iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
-  iAssert (â—‡ P)%I as "#HP".
-  { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
-  iMod "HP". iFrame. auto.
+Instance fupd_facts `{invG Σ} : FUpdFacts (uPredSI (iResUR Σ)).
+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) ">? [$ $] !> !>".
+  - 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".
+    iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
+  - intros E1 E2 Ef P HE1Ef. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
+    iIntros "Hvs (Hw & HE1 &HEf)".
+    iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
+    iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
+    iIntros "!> !>". by iApply "HP".
+  - rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
+  - iIntros (E1 E2 E2' P Q ? (E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
+    rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
+    iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
+    iAssert (â—‡ P)%I as "#HP".
+    { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
+    iMod "HP". iFrame. auto.
+  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P ?) "HP [Hw HE]".
+    iAssert (â–· â—‡ P)%I with "[-]" as "#$"; last by iFrame.
+    iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
 Qed.
-
-Lemma later_fupd_plain E P `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P.
-Proof.
-  rewrite uPred_fupd_eq /uPred_fupd_def. iIntros "HP [Hw HE]".
-  iAssert (â–· â—‡ P)%I with "[-]" as "#$"; last by iFrame.
-  iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
-Qed.
-
-(** * Derived rules *)
-Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
-Proof. intros P Q; apply fupd_mono. Qed.
-Global Instance fupd_flip_mono' E1 E2 :
-  Proper (flip (⊢) ==> flip (⊢)) (fupd E1 E2).
-Proof. intros P Q; apply fupd_mono. Qed.
-
-Lemma fupd_intro E P : P ={E}=∗ P.
-Proof. iIntros "HP". by iApply bupd_fupd. Qed.
-Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> True)%I.
-Proof. exact: fupd_intro_mask. Qed.
-Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
-Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
-
-Lemma fupd_frame_l E1 E2 P Q : (P ∗ |={E1,E2}=> Q) ={E1,E2}=∗ P ∗ Q.
-Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
-Lemma fupd_wand_l E1 E2 P Q : (P -∗ Q) ∗ (|={E1,E2}=> P) ={E1,E2}=∗ Q.
-Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
-Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ={E1,E2}=∗ Q.
-Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
-
-Lemma fupd_trans_frame E1 E2 E3 P Q :
-  ((Q ={E2,E3}=∗ True) ∗ |={E1,E2}=> (Q ∗ P)) ={E1,E3}=∗ P.
-Proof.
-  rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
-  by rewrite fupd_frame_r left_id fupd_trans.
-Qed.
-
-Lemma fupd_mask_frame_r E1 E2 Ef P :
-  E1 ## Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
-Proof.
-  iIntros (?) "H". iApply fupd_mask_frame_r'; auto.
-  iApply fupd_wand_r; iFrame "H"; eauto.
-Qed.
-Lemma fupd_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=∗ P.
-Proof.
-  intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
-Qed.
-
-Lemma fupd_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ={E}=∗ P ∗ Q.
-Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
-Lemma fupd_big_sepL {A} E (Φ : nat → A → iProp Σ) (l : list A) :
-  ([∗ list] k↦x ∈ l, |={E}=> Φ k x) ={E}=∗ [∗ list] k↦x ∈ l, Φ k x.
-Proof.
-  apply (big_opL_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
-  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
-Qed.
-Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Σ) (m : gmap K A) :
-  ([∗ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=∗ [∗ map] k↦x ∈ m, Φ k x.
-Proof.
-  apply (big_opM_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
-  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
-Qed.
-Lemma fupd_big_sepS `{Countable A} E (Φ : A → iProp Σ) X :
-  ([∗ set] x ∈ X, |={E}=> Φ x) ={E}=∗ [∗ set] x ∈ X, Φ x.
-Proof.
-  apply (big_opS_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
-  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
-Qed.
-
-Lemma fupd_plain E1 E2 P Q `{!Plain P} :
-  E1 ⊆ E2 → (Q -∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
-Proof.
-  iIntros (HE) "HQP HQ". iApply (fupd_plain' _ _ E1 with "[HQP] HQ"); first done.
-  iIntros "?". iApply fupd_intro. by iApply "HQP".
-Qed.
-End fupd.
-
-(** Proofmode class instances *)
-Section proofmode_classes.
-  Context `{invG Σ}.
-  Implicit Types P Q : iProp Σ.
-
-  Global Instance from_pure_fupd E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
-  Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
-
-  Global Instance from_assumption_fupd E p P Q :
-    FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I.
-  Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
-
-  Global Instance into_wand_fupd 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 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 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 /= => ->.
-    apply wand_intro_l. by rewrite affinely_persistently_if_elim fupd_wand_r.
-  Qed.
-
-  Global Instance from_sep_fupd E P Q1 Q2 :
-    FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
-  Proof. rewrite /FromSep =><-. apply fupd_sep. Qed.
-
-  Global Instance from_or_fupd 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; auto with I. Qed.
-
-  Global Instance from_exist_fupd {A} E1 E2 P (Φ : A → iProp Σ) :
-    FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
-  Proof.
-    rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
-  Qed.
-
-  Global Instance frame_fupd p E1 E2 R P Q :
-    Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
-  Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
-
-  Global Instance is_except_0_fupd E1 E2 P : IsExcept0 (|={E1,E2}=> P).
-  Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
-
-  Global Instance from_modal_fupd E P : FromModal (|={E}=> P) P.
-  Proof. rewrite /FromModal. apply fupd_intro. Qed.
-
-  Global Instance elim_modal_bupd_fupd E1 E2 P Q :
-    ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
-  Proof.
-    by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
-  Qed.
-  Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
-    ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
-  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
-
-  Global Instance add_modal_fupd E1 E2 P Q :
-    AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
-  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
-End proofmode_classes.
-
-Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.
-
-(** Fancy updates that take a step. *)
-
-Section step_fupd.
-Context `{invG Σ}.
-
-Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}▷=> P) -∗ (P -∗ Q) -∗ |={E1,E2}▷=> Q.
-Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.
-
-Lemma step_fupd_mask_frame_r E1 E2 Ef P :
-  E1 ## Ef → E2 ## Ef → (|={E1,E2}▷=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}▷=> P.
-Proof.
-  iIntros (??) "HP". iApply fupd_mask_frame_r. done. iMod "HP". iModIntro.
-  iNext. by iApply fupd_mask_frame_r.
-Qed.
-
-Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
-  F1 ⊆ F2 → E1 ⊆ E2 → (|={E1,F2}▷=> P) ⊢ |={E2,F1}▷=> P.
-Proof.
-  iIntros (??) "HP".
-  iMod (fupd_intro_mask') as "HM1"; first done. iMod "HP".
-  iMod (fupd_intro_mask') as "HM2"; first done. iModIntro.
-  iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
-Qed.
-
-Lemma step_fupd_intro E1 E2 P : E2 ⊆ E1 → ▷ P -∗ |={E1,E2}▷=> P.
-Proof. iIntros (?) "HP". iApply (step_fupd_mask_mono E2 _ _ E2); auto. Qed.
-End step_fupd.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 8a49cf8a3ada75fe2ad780e352f1e847d4f0ff26..88e0b7aaec97c794747cf4b732c9ff98c0c24cb2 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -601,16 +601,6 @@ Qed.
 Global Instance cmra_valid_proper {A : cmraT} :
   Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
 
-Global Instance bupd_ne : NonExpansive (@bupd _ (@uPred_bupd M)).
-Proof.
-  intros n P Q HPQ.
-  unseal; split=> n' x; split; intros HP k yf ??;
-    destruct (HP k yf) as (x'&?&?); auto;
-    exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
-Qed.
-Global Instance bupd_proper :
-  Proper ((≡) ==> (≡)) (@bupd _ (@uPred_bupd M)) := ne_proper _.
-
 (** BI instances *)
 
 Global Instance uPred_affine : BiAffine (uPredI M) | 0.
@@ -686,27 +676,29 @@ Lemma ofe_fun_validI `{Finite A} {B : A → ucmraT} (g : ofe_fun B) :
 Proof. by uPred.unseal. Qed.
 
 (* Basic update modality *)
-Lemma bupd_intro P : P ==∗ P.
-Proof.
-  unseal. split=> n x ? HP k yf ?; exists x; split; first done.
-  apply uPred_mono with n x; eauto using cmra_validN_op_l.
-Qed.
-Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ==∗ Q.
+Global Instance bupd_facts : BUpdFacts (uPredI M).
 Proof.
-  unseal. intros HPQ; split=> n x ? HP k yf ??.
-  destruct (HP k yf) as (x'&?&?); eauto.
-  exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
-Qed.
-Lemma bupd_trans P : (|==> |==> P) ==∗ P.
-Proof. unseal; split; naive_solver. Qed.
-Lemma bupd_frame_r P R : (|==> P) ∗ R ==∗ P ∗ R.
-Proof.
-  unseal. split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
-  destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto.
-  { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
-  exists (x' â‹… x2); split; first by rewrite -assoc.
-  exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
+  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.
@@ -716,11 +708,5 @@ Proof.
   exists (y â‹… x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
-Lemma bupd_plainly P : (|==> bi_plainly P) ⊢ P.
-Proof.
-  unseal; split => n x Hnx /= Hng.
-  destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
-  eapply uPred_mono; eauto using ucmra_unit_leastN.
-Qed.
 End uPred.
 End uPred.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index e4bc4e09184429ddd542b74a5f8dc0007401aba2..cdd0d4250b3e9bf53e3dc190ff18dbfafa695022 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -1,7 +1,7 @@
 From stdpp Require Import coPset.
-From iris.bi Require Import interface.
+From iris.bi Require Import interface derived_laws big_op.
 
-Class BUpd (A : Type) : Type := bupd : A → A.
+Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
 Instance : Params (@bupd) 2.
 
 Notation "|==> Q" := (bupd Q)
@@ -11,7 +11,7 @@ Notation "P ==∗ Q" := (P ⊢ |==> Q)
 Notation "P ==∗ Q" := (P -∗ |==> Q)%I
   (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.
 
-Class FUpd (A : Type) : Type := fupd : coPset → coPset → A → A.
+Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
 Instance: Params (@fupd) 4.
 
 Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
@@ -46,3 +46,174 @@ Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I
 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 : bi) `{BUpd PROP} : Prop :=
+  { bupd_ne :> NonExpansive bupd;
+    bupd_intro P : P ==∗ P;
+    bupd_mono P Q : (P ⊢ Q) → (|==> P) ==∗ Q;
+    bupd_trans P : (|==> |==> P) ==∗ P;
+    bupd_frame_r P R : (|==> P) ∗ R ==∗ P ∗ R;
+    bupd_plainly P : (|==> bi_plainly P) -∗ P }.
+
+Section bupd_derived.
+  Context `{BUpdFacts PROP}.
+
+  Global Instance bupd_proper : Proper ((≡) ==> (≡)) bupd := ne_proper _.
+
+  (** BUpd derived rules *)
+
+  Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) bupd.
+  Proof. intros P Q; apply bupd_mono. Qed.
+  Global Instance bupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) bupd.
+  Proof. intros P Q; apply bupd_mono. Qed.
+
+  Lemma bupd_frame_l R Q : (R ∗ |==> Q) ==∗ R ∗ Q.
+  Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
+  Lemma bupd_wand_l P Q : (P -∗ Q) ∗ (|==> P) ==∗ Q.
+  Proof. by rewrite bupd_frame_l bi.wand_elim_l. Qed.
+  Lemma bupd_wand_r P Q : (|==> P) ∗ (P -∗ Q) ==∗ Q.
+  Proof. by rewrite bupd_frame_r bi.wand_elim_r. Qed.
+  Lemma bupd_sep P Q : (|==> P) ∗ (|==> Q) ==∗ P ∗ Q.
+  Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
+  Lemma bupd_affinely_plainly `{BiAffine PROP} P : (|==> ■ P) ⊢ P.
+  Proof. by rewrite bi.affine_affinely bupd_plainly. Qed.
+  Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
+  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 : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
+    bupd_fupd E P : (|==> P) ={E}=∗ P;
+    except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
+    fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q;
+    fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P;
+    fupd_mask_frame_r' E1 E2 Ef P :
+      E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P;
+    fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q;
+    fupd_plain' E1 E2 E2' P Q `{!Plain P} :
+      E1 ⊆ E2 →
+      (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
+    later_fupd_plain E P `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P }.
+
+Section fupd_derived.
+  Context `{FUpdFacts PROP}.
+
+  Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (fupd E1 E2) := ne_proper _.
+
+  (** FUpd derived rules *)
+
+  Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
+  Proof. intros P Q; apply fupd_mono. Qed.
+  Global Instance fupd_flip_mono' E1 E2 :
+    Proper (flip (⊢) ==> flip (⊢)) (fupd E1 E2).
+  Proof. intros P Q; apply fupd_mono. Qed.
+
+  Lemma fupd_intro E P : P ={E}=∗ P.
+  Proof. rewrite -bupd_fupd. apply bupd_intro. Qed.
+  Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> emp)%I.
+  Proof. exact: fupd_intro_mask. Qed.
+  Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
+  Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
+
+  Lemma fupd_frame_l E1 E2 P Q : (P ∗ |={E1,E2}=> Q) ={E1,E2}=∗ P ∗ Q.
+  Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
+  Lemma fupd_wand_l E1 E2 P Q : (P -∗ Q) ∗ (|={E1,E2}=> P) ={E1,E2}=∗ Q.
+  Proof. by rewrite fupd_frame_l bi.wand_elim_l. Qed.
+  Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ={E1,E2}=∗ Q.
+  Proof. by rewrite fupd_frame_r bi.wand_elim_r. Qed.
+
+  Lemma fupd_trans_frame E1 E2 E3 P Q :
+    ((Q ={E2,E3}=∗ emp) ∗ |={E1,E2}=> (Q ∗ P)) ={E1,E3}=∗ P.
+  Proof.
+    rewrite fupd_frame_l assoc -(comm _ Q) bi.wand_elim_r.
+    by rewrite fupd_frame_r left_id fupd_trans.
+  Qed.
+
+  Lemma fupd_mask_frame_r E1 E2 Ef P :
+    E1 ## Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
+  Proof.
+    intros ?. rewrite -fupd_mask_frame_r' //. f_equiv.
+    apply bi.impl_intro_l, bi.and_elim_r.
+  Qed.
+  Lemma fupd_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=∗ P.
+  Proof.
+    intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
+  Qed.
+
+  Lemma fupd_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ={E}=∗ P ∗ Q.
+  Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
+  Lemma fupd_big_sepL {A} E (Φ : nat → A → PROP) (l : list A) :
+    ([∗ list] k↦x ∈ l, |={E}=> Φ k x) ={E}=∗ [∗ list] k↦x ∈ l, Φ k x.
+  Proof.
+    apply (big_opL_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
+    intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
+  Qed.
+  Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K → A → PROP) (m : gmap K A) :
+    ([∗ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=∗ [∗ map] k↦x ∈ m, Φ k x.
+  Proof.
+    apply (big_opM_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
+    intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
+  Qed.
+  Lemma fupd_big_sepS `{Countable A} E (Φ : A → PROP) X :
+    ([∗ set] x ∈ X, |={E}=> Φ x) ={E}=∗ [∗ set] x ∈ X, Φ x.
+  Proof.
+    apply (big_opS_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
+    intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
+  Qed.
+
+  Lemma fupd_plain E1 E2 P Q `{!Plain P} :
+    E1 ⊆ E2 → (Q -∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+  Proof.
+    intros HE. rewrite -(fupd_plain' _ _ E1) //. apply bi.wand_intro_l.
+    by rewrite bi.wand_elim_r -fupd_intro.
+  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.
+    by rewrite (bi.later_intro (P -∗ Q)%I) fupd_frame_l -bi.later_sep fupd_frame_l
+               bi.wand_elim_l.
+  Qed.
+
+  Lemma step_fupd_mask_frame_r E1 E2 Ef P :
+    E1 ## Ef → E2 ## Ef → (|={E1,E2}▷=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}▷=> P.
+  Proof.
+    intros. rewrite -fupd_mask_frame_r //. do 2 f_equiv. by apply fupd_mask_frame_r.
+  Qed.
+
+  Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
+    F1 ⊆ F2 → E1 ⊆ E2 → (|={E1,F2}▷=> P) ⊢ |={E2,F1}▷=> P.
+  Proof.
+    intros ??. rewrite -(left_id emp%I _ (|={E1,F2}â–·=> P)%I).
+    rewrite (fupd_intro_mask E2 E1 emp%I) //.
+    rewrite fupd_frame_r -(fupd_trans E2 E1 F1). f_equiv.
+    rewrite fupd_frame_l -(fupd_trans E1 F2 F1). f_equiv.
+    rewrite (fupd_intro_mask F2 F1 (|={_,_}=> emp)%I) //.
+    rewrite fupd_frame_r. f_equiv.
+    rewrite [X in (X ∗ _)%I]bi.later_intro -bi.later_sep. f_equiv.
+    rewrite fupd_frame_r -(fupd_trans F1 F2 E2). f_equiv.
+    rewrite fupd_frame_l -(fupd_trans F2 E1 E2). f_equiv.
+    by rewrite fupd_frame_r left_id.
+  Qed.
+
+  Lemma step_fupd_intro E1 E2 P : E2 ⊆ E1 → ▷ P -∗ |={E1,E2}▷=> P.
+  Proof. intros. by rewrite -(step_fupd_mask_mono E2 _ _ E2) // -!fupd_intro. Qed.
+End fupd_derived.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 8a1bc66264b68acc943e6b95cacce4c7960ed63e..356dea9be0a19ae0c067e180bb39a7ef0b6d6683 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -73,6 +73,10 @@ Global Instance from_assumption_forall {A} p (Φ : A → PROP) Q x :
   FromAssumption p (Φ x) Q → FromAssumption p (∀ x, Φ x) Q.
 Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
 
+Global Instance from_assumption_bupd `{BUpdFacts PROP} p P Q :
+  FromAssumption p P Q → FromAssumption p P (|==> Q).
+Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
+
 (* IntoPure *)
 Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
 Proof. by rewrite /IntoPure. Qed.
@@ -168,6 +172,10 @@ Global Instance from_pure_embed `{BiEmbedding PROP PROP'} P φ :
   FromPure P φ → FromPure ⎡P⎤ φ.
 Proof. rewrite /FromPure=> <-. by rewrite bi_embed_pure. Qed.
 
+Global Instance from_pure_bupd `{BUpdFacts PROP} P φ :
+  FromPure P φ → FromPure (|==> P) φ.
+Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
+
 (* IntoInternalEq *)
 Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
   @IntoInternalEq PROP A (x ≡ y) x y.
@@ -330,6 +338,27 @@ Proof.
           -bi_embed_wand => -> //.
 Qed.
 
+Global Instance into_wand_bupd `{BUpdFacts 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 :
+  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 :
+  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.
+
 (* FromAnd *)
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
 Proof. by rewrite /FromAnd. Qed.
@@ -422,6 +451,10 @@ Global Instance from_sep_big_sepL_app {A} (Φ : nat → A → PROP) l1 l2 :
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
 Proof. by rewrite /FromSep big_opL_app. Qed.
 
+Global Instance from_sep_bupd `{BUpdFacts PROP} P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
+Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
+
 (* IntoAnd *)
 Global Instance into_and_and p P Q : IntoAnd p (P ∧ Q) P Q | 10.
 Proof. by rewrite /IntoAnd affinely_persistently_if_and. Qed.
@@ -563,6 +596,12 @@ Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
 Global Instance from_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
 Proof. by rewrite /FromOr -bi_embed_or => <-. Qed.
+Global Instance from_or_bupd `{BUpdFacts 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.
 
 (* IntoOr *)
 Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
@@ -607,6 +646,11 @@ Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
 Global Instance from_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
 Proof. by rewrite /FromExist -bi_embed_exist => <-. Qed.
+Global Instance from_exist_bupd `{BUpdFacts 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.
 
 (* IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ.
@@ -711,9 +755,19 @@ Global Instance elim_modal_forall {A} P P' (Φ Ψ : A → PROP) :
 Proof.
   rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
-Global Instance elim_modal_absorbingly P Q : Absorbing Q → ElimModal (bi_absorbingly P) P Q Q.
+(* We use this proxy type class to make sure that the instance is only
+   used when we know that Pabs is not an existential, so that this
+   instance is only triggered when a [bi_absorbingly] modality
+   actually appears, thanks to the [Hint Mode] lower in this
+   file. Otherwise, this instance is too generic and gets used in
+   irrelevant contexts. *)
+Class ElimModalAbsorbingly Pabs P Q :=
+  elim_modal_absorbingly :> ElimModal Pabs P Q Q.
+Global Instance elim_modal_absorbingly_here P Q :
+  Absorbing Q → ElimModalAbsorbingly (bi_absorbingly P) P Q.
 Proof.
-  rewrite /ElimModal=> H. by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
+  rewrite /ElimModalAbsorbingly /ElimModal=> H.
+  by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
 Qed.
 
 (* AddModal *)
@@ -728,6 +782,8 @@ Global Instance add_modal_forall {A} P P' (Φ : A → PROP) :
 Proof.
   rewrite /AddModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
+Global Instance add_modal_bupd `{BUpdFacts PROP} P Q : AddModal (|==> P) P (|==> Q).
+Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
 
 (* Frame *)
 Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
@@ -944,14 +1000,32 @@ Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
   (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 
+Global Instance frame_bupd `{BUpdFacts PROP} p R P Q :
+  Frame p R P Q → Frame p R (|==> P) (|==> Q).
+Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
+
 (* FromModal *)
 Global Instance from_modal_absorbingly P : FromModal (bi_absorbingly P) P.
 Proof. apply absorbingly_intro. Qed.
 Global Instance from_modal_embed `{BiEmbedding PROP PROP'} P Q :
   FromModal P Q → FromModal ⎡P⎤ ⎡Q⎤.
 Proof. by rewrite /FromModal=> ->. Qed.
+Global Instance from_modal_bupd `{BUpdFacts PROP} P : FromModal (|==> P) P.
+Proof. apply bupd_intro. Qed.
+
+(* ElimModal *)
+Global Instance elim_modal_bupd `{BUpdFacts PROP} P Q :
+  ElimModal (|==> 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 :
+  Plain Q → ElimModal (|==> 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 :
+  Plain P → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
 End bi_instances.
 
+Hint Mode ElimModalAbsorbingly + ! - - : typeclass_instances.
 
 Section sbi_instances.
 Context {PROP : sbi}.
@@ -967,6 +1041,9 @@ Proof. rewrite /FromAssumption=>->. apply laterN_intro. Qed.
 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_fupd `{FUpdFacts PROP} E p P Q :
+  FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I.
+Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
 
 (* FromPure *)
 Global Instance from_pure_later P φ : FromPure P φ → FromPure (▷ P) φ.
@@ -975,6 +1052,9 @@ Global Instance from_pure_laterN n P φ : FromPure P φ → FromPure (▷^n P) 
 Proof. rewrite /FromPure=> ->. apply laterN_intro. Qed.
 Global Instance from_pure_except_0 P φ : FromPure P φ → FromPure (◇ P) φ.
 Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.
+Global Instance from_pure_fupd `{FUpdFacts PROP} E P φ :
+  FromPure P φ → FromPure (|={E}=> P) φ.
+Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
 
 (* IntoWand *)
 Global Instance into_wand_later p q R P Q :
@@ -1007,6 +1087,26 @@ Proof.
              (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
 Qed.
 
+Global Instance into_wand_fupd `{FUpdFacts 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 :
+  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 :
+  IntoWand p false R P Q → IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+Proof.
+  rewrite /IntoWand' /IntoWand /= => ->.
+  apply wand_intro_l. by rewrite affinely_persistently_if_elim fupd_wand_r.
+Qed.
+
 (* FromAnd *)
 Global Instance from_and_later P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd (▷ P) (▷ Q1) (▷ Q2).
@@ -1028,6 +1128,9 @@ Proof. rewrite /FromSep=> <-. by rewrite laterN_sep. Qed.
 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_fupd `{FUpdFacts PROP} E P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
+Proof. rewrite /FromSep =><-. apply fupd_sep. Qed.
 
 (* IntoAnd *)
 Global Instance into_and_later p P Q1 Q2 :
@@ -1085,6 +1188,12 @@ Proof. rewrite /FromOr=><-. by rewrite laterN_or. Qed.
 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_fupd `{FUpdFacts 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;
+                         [apply bi.or_intro_l|apply bi.or_intro_r].
+Qed.
 
 (* IntoOr *)
 Global Instance into_or_later P Q1 Q2 :
@@ -1111,6 +1220,11 @@ Qed.
 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_fupd `{FUpdFacts 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).
+Qed.
 
 (* IntoExist *)
 Global Instance into_exist_later {A} P (Φ : A → PROP) :
@@ -1159,12 +1273,22 @@ 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).
+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 :
+  IsExcept0 (|={E1,E2}=> P).
+Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
 
 (* FromModal *)
 Global Instance from_modal_later P : FromModal (â–· P) P.
 Proof. apply later_intro. Qed.
 Global Instance from_modal_except_0 P : FromModal (â—‡ P) P.
 Proof. apply except_0_intro. Qed.
+Global Instance from_modal_fupd E P `{FUpdFacts PROP} : FromModal (|={E}=> P) P.
+Proof. rewrite /FromModal. apply fupd_intro. Qed.
 
 (* IntoExcept0 *)
 Global Instance into_except_0_except_0 P : IntoExcept0 (â—‡ P) P.
@@ -1197,6 +1321,14 @@ 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_fupd `{FUpdFacts PROP} E1 E2 P Q :
+  ElimModal (|==> 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 :
+  ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 
 (* AddModal *)
 (* High priority to add a â–· rather than a â—‡ when P is timeless. *)
@@ -1222,6 +1354,9 @@ Proof.
   intros. rewrite /AddModal (except_0_intro (_ -∗ _)%I).
   by rewrite -except_0_sep wand_elim_r except_0_later.
 Qed.
+Global Instance add_modal_fupd `{FUpdFacts 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.
 
 (* Frame *)
 Class MakeLater (P lP : PROP) := make_later : ▷ P ⊣⊢ lP.
@@ -1239,6 +1374,10 @@ Proof.
   by rewrite later_affinely_persistently_if_2 later_sep.
 Qed.
 
+Global Instance frame_fupd `{FUpdFacts PROP} p E1 E2 R P Q :
+  Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
+
 Class MakeLaterN (n : nat) (P lP : PROP) := make_laterN : ▷^n P ⊣⊢ lP.
 Arguments MakeLaterN _%nat _%I _%I.
 
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a5f23b9255fbe83244aecef1be08650e38f1c0a0..2f5a1756538228f002ab62a4400215175f09f81c 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1853,5 +1853,8 @@ Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _.
 Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro.
 Hint Extern 1 (envs_entails _ (_ ∨ _)) => iLeft.
 Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight.
+Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro.
+Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro.
+
 
 Hint Extern 2 (envs_entails _ (_ ∗ _)) => progress iFrame : iFrame.