diff --git a/_CoqProject b/_CoqProject
index f01a9bc225191ea7c4f9cec35a2baf92f72ecdfa..894e7004117ad53b1f2bcaf1c067f5142ca5e24e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -44,8 +44,8 @@ theories/si_logic/bi.v
 theories/bi/notation.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v
-theories/bi/derived_laws_bi.v
-theories/bi/derived_laws_sbi.v
+theories/bi/derived_laws.v
+theories/bi/derived_laws_later.v
 theories/bi/plainly.v
 theories/bi/internal_eq.v
 theories/bi/big_op.v
@@ -138,8 +138,12 @@ theories/proofmode/sel_patterns.v
 theories/proofmode/tactics.v
 theories/proofmode/notation.v
 theories/proofmode/classes.v
-theories/proofmode/class_instances_bi.v
-theories/proofmode/class_instances_sbi.v
+theories/proofmode/class_instances.v
+theories/proofmode/class_instances_later.v
+theories/proofmode/class_instances_updates.v
+theories/proofmode/class_instances_embedding.v
+theories/proofmode/class_instances_plainly.v
+theories/proofmode/class_instances_internal_eq.v
 theories/proofmode/frame_instances.v
 theories/proofmode/monpred.v
 theories/proofmode/modalities.v
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 9fde00f1a5c85fb916f191363ba4ef5ddf431a44..8f5aa1aa0fc72846c4cc3cd612ef2e95d2756b1e 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,9 +1,9 @@
-From iris.bi Require Export derived_laws_bi derived_laws_sbi big_op.
+From iris.bi Require Export derived_laws derived_laws_later big_op.
 From iris.bi Require Export updates internal_eq plainly embedding.
 Set Default Proof Using "Type".
 
 Module Import bi.
   Export bi.interface.bi.
-  Export bi.derived_laws_bi.bi.
-  Export bi.derived_laws_sbi.bi.
+  Export bi.derived_laws.bi.
+  Export bi.derived_laws_later.bi.
 End bi.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 4bb1940211dcc1cb9beceeb6b55e8026ce9341df..a118ac19e392b758c9326ba07429597fa39a4a32 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1,8 +1,8 @@
 From stdpp Require Import countable fin_sets functions.
-From iris.bi Require Import derived_laws_sbi.
+From iris.bi Require Import derived_laws_later.
 From iris.algebra Require Export big_op.
 Set Default Proof Using "Type".
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (** Notations for unary variants *)
 Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
@@ -65,7 +65,7 @@ Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P" :=
   (big_sepM2 (λ _ x1 x2, P) m1 m2) : bi_scope.
 
 (** * Properties *)
-Section bi_big_op.
+Section big_op.
 Context {PROP : bi}.
 Implicit Types P Q : PROP.
 Implicit Types Ps Qs : list PROP.
@@ -231,6 +231,20 @@ Section sep_list.
     [∗] replicate (length l) P ⊣⊢ [∗ list] y ∈ l, P.
   Proof. induction l as [|x l]=> //=; by f_equiv. Qed.
 
+  Lemma big_sepL_later `{BiAffine PROP} Φ l :
+    ▷ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷ Φ k x).
+  Proof. apply (big_opL_commute _). Qed.
+  Lemma big_sepL_later_2 Φ l :
+    ([∗ list] k↦x ∈ l, ▷ Φ k x) ⊢ ▷ [∗ list] k↦x ∈ l, Φ k x.
+  Proof. by rewrite (big_opL_commute _). Qed.
+
+  Lemma big_sepL_laterN `{BiAffine PROP} Φ n l :
+    ▷^n ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷^n Φ k x).
+  Proof. apply (big_opL_commute _). Qed.
+  Lemma big_sepL_laterN_2 Φ n l :
+    ([∗ list] k↦x ∈ l, ▷^n Φ k x) ⊢ ▷^n [∗ list] k↦x ∈ l, Φ k x.
+  Proof. by rewrite (big_opL_commute _). Qed.
+
   Global Instance big_sepL_nil_persistent Φ :
     Persistent ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
@@ -249,6 +263,16 @@ Section sep_list.
   Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
   Global Instance big_sepL_affine_id Ps : TCForall Affine Ps → Affine ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
+
+  Global Instance big_sepL_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
+    Timeless ([∗ list] k↦x ∈ [], Φ k x).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_sepL_timeless `{!Timeless (emp%I : PROP)} Φ l :
+    (∀ k x, Timeless (Φ k x)) → Timeless ([∗ list] k↦x ∈ l, Φ k x).
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Global Instance big_sepL_timeless_id `{!Timeless (emp%I : PROP)} Ps :
+    TCForall Timeless Ps → Timeless ([∗] Ps).
+  Proof. induction 1; simpl; apply _. Qed.
 End sep_list.
 
 Section sep_list_more.
@@ -519,6 +543,34 @@ Section sep_list2.
       apply forall_intro=> k. by rewrite (forall_elim (S k)).
   Qed.
 
+  Lemma big_sepL2_later_1 `{BiAffine PROP} Φ l1 l2 :
+    (▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ ◇ [∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2.
+  Proof.
+    rewrite !big_sepL2_alt later_and big_sepL_later (timeless ⌜ _ ⌝%I).
+    rewrite except_0_and. auto using and_mono, except_0_intro.
+  Qed.
+
+  Lemma big_sepL2_later_2 Φ l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2) ⊢ ▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2.
+  Proof.
+    rewrite !big_sepL2_alt later_and big_sepL_later_2.
+    auto using and_mono, later_intro.
+  Qed.
+
+  Lemma big_sepL2_laterN_2 Φ n l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l1;l2, ▷^n Φ k y1 y2) ⊢ ▷^n [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2.
+  Proof.
+    rewrite !big_sepL2_alt laterN_and big_sepL_laterN_2.
+    auto using and_mono, laterN_intro.
+  Qed.
+
+  Lemma big_sepL2_flip Φ l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l2; l1, Φ k y2 y1) ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2).
+  Proof.
+    revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2]//=; simplify_eq.
+    by rewrite IH.
+  Qed.
+
   Global Instance big_sepL2_nil_persistent Φ :
     Persistent ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
   Proof. simpl; apply _. Qed.
@@ -534,6 +586,14 @@ Section sep_list2.
     (∀ k x1 x2, Affine (Φ k x1 x2)) →
     Affine ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
   Proof. rewrite big_sepL2_alt. apply _. Qed.
+
+  Global Instance big_sepL2_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
+    Timeless ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_sepL2_timeless `{!Timeless (emp%I : PROP)} Φ l1 l2 :
+    (∀ k x1 x2, Timeless (Φ k x1 x2)) →
+    Timeless ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
+  Proof. rewrite big_sepL2_alt. apply _. Qed.
 End sep_list2.
 
 Section and_list.
@@ -936,6 +996,20 @@ Section map.
       by rewrite pure_True // True_impl.
   Qed.
 
+  Lemma big_sepM_later `{BiAffine PROP} Φ m :
+    ▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x).
+  Proof. apply (big_opM_commute _). Qed.
+  Lemma big_sepM_later_2 Φ m :
+    ([∗ map] k↦x ∈ m, ▷ Φ k x) ⊢ ▷ [∗ map] k↦x ∈ m, Φ k x.
+  Proof. by rewrite big_opM_commute. Qed.
+
+  Lemma big_sepM_laterN `{BiAffine PROP} Φ n m :
+    ▷^n ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷^n Φ k x).
+  Proof. apply (big_opM_commute _). Qed.
+  Lemma big_sepM_laterN_2 Φ n m :
+    ([∗ map] k↦x ∈ m, ▷^n Φ k x) ⊢ ▷^n [∗ map] k↦x ∈ m, Φ k x.
+  Proof. by rewrite big_opM_commute. Qed.
+
   Global Instance big_sepM_empty_persistent Φ :
     Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
@@ -949,6 +1023,13 @@ Section map.
   Global Instance big_sepM_affine Φ m :
     (∀ k x, Affine (Φ k x)) → Affine ([∗ map] k↦x ∈ m, Φ k x).
   Proof. rewrite big_opM_eq. intros. apply big_sepL_affine=> _ [??]; apply _. Qed.
+
+  Global Instance big_sepM_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
+    Timeless ([∗ map] k↦x ∈ ∅, Φ k x).
+  Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
+  Global Instance big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
+    (∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x).
+  Proof. rewrite big_opM_eq. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
 End map.
 
 (** ** Big ops over two maps *)
@@ -963,6 +1044,14 @@ Section map2.
     set_unfold=>k. by rewrite !elem_of_dom.
   Qed.
 
+  Lemma big_sepM2_flip Φ m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ m2; m1, Φ k y2 y1) ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2).
+  Proof.
+    rewrite big_sepM2_eq /big_sepM2_def. apply and_proper; [apply pure_proper; naive_solver |].
+    rewrite -map_zip_with_flip map_zip_with_map_zip big_sepM_fmap.
+    apply big_sepM_proper. by intros k [b a].
+  Qed.
+
   (** The lemmas [big_sepM2_mono], [big_sepM2_ne] and [big_sepM2_proper] are more
   generic than the instances as they also give [mi !! k = Some yi] in the premise. *)
   Lemma big_sepM2_mono Φ Ψ m1 m2 :
@@ -1282,6 +1371,31 @@ Section map2.
     destruct (m1 !! k) as [x1|], (m2 !! k) as [x2|]; naive_solver.
   Qed.
 
+  Lemma big_sepM2_later_1 `{BiAffine PROP} Φ m1 m2 :
+    (▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
+    ⊢ ◇ ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2).
+  Proof.
+    rewrite big_sepM2_eq /big_sepM2_def later_and (timeless ⌜_⌝%I).
+    rewrite big_sepM_later except_0_and.
+    auto using and_mono_r, except_0_intro.
+  Qed.
+  Lemma big_sepM2_later_2 Φ m1 m2 :
+    ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2)
+    ⊢ ▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
+  Proof.
+    rewrite big_sepM2_eq /big_sepM2_def later_and -(later_intro ⌜_⌝%I).
+    apply and_mono_r. by rewrite big_opM_commute.
+  Qed.
+
+  Lemma big_sepM2_laterN_2 Φ n m1 m2 :
+    ([∗ map] k↦x1;x2 ∈ m1;m2, ▷^n Φ k x1 x2)
+    ⊢ ▷^n [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
+  Proof.
+    induction n as [|n IHn]; first done.
+    rewrite later_laterN -IHn -big_sepM2_later_2.
+    apply big_sepM2_mono. eauto.
+  Qed.
+
   Global Instance big_sepM2_empty_persistent Φ :
     Persistent ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
   Proof. rewrite big_sepM2_empty. apply _. Qed.
@@ -1297,6 +1411,14 @@ Section map2.
     (∀ k x1 x2, Affine (Φ k x1 x2)) →
     Affine ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
   Proof. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
+
+  Global Instance big_sepM2_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
+    Timeless ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
+  Proof. rewrite big_sepM2_eq /big_sepM2_def map_zip_with_empty. apply _. Qed.
+  Global Instance big_sepM2_timeless `{!Timeless (emp%I : PROP)} Φ m1 m2 :
+    (∀ k x1 x2, Timeless (Φ k x1 x2)) →
+    Timeless ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
+  Proof. intros. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
 End map2.
 
 (** ** Big ops over finite sets *)
@@ -1452,6 +1574,20 @@ Section gset.
       by rewrite pure_True ?True_impl; last set_solver.
   Qed.
 
+  Lemma big_sepS_later `{BiAffine PROP} Φ X :
+    ▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y).
+  Proof. apply (big_opS_commute _). Qed.
+  Lemma big_sepS_later_2 Φ X :
+    ([∗ set] y ∈ X, ▷ Φ y) ⊢ ▷ ([∗ set] y ∈ X, Φ y).
+  Proof. by rewrite big_opS_commute. Qed.
+
+  Lemma big_sepS_laterN `{BiAffine PROP} Φ n X :
+    ▷^n ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷^n Φ y).
+  Proof. apply (big_opS_commute _). Qed.
+  Lemma big_sepS_laterN_2 Φ n X :
+    ([∗ set] y ∈ X, ▷^n Φ y) ⊢ ▷^n ([∗ set] y ∈ X, Φ y).
+  Proof. by rewrite big_opS_commute. Qed.
+
   Global Instance big_sepS_empty_persistent Φ :
     Persistent ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
@@ -1464,6 +1600,13 @@ Section gset.
   Global Instance big_sepS_affine Φ X :
     (∀ x, Affine (Φ x)) → Affine ([∗ set] x ∈ X, Φ x).
   Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
+
+  Global Instance big_sepS_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
+    Timeless ([∗ set] x ∈ ∅, Φ x).
+  Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
+  Global Instance big_sepS_timeless `{!Timeless (emp%I : PROP)} Φ X :
+    (∀ x, Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
+  Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
 End gset.
 
 Lemma big_sepM_dom `{Countable K} {A} (Φ : K → PROP) (m : gmap K A) :
@@ -1536,6 +1679,20 @@ Section gmultiset.
     ([∗ mset] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ mset] y ∈ X, Φ y) ∧ ([∗ mset] y ∈ X, Ψ y).
   Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
 
+  Lemma big_sepMS_later `{BiAffine PROP} Φ X :
+    ▷ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷ Φ y).
+  Proof. apply (big_opMS_commute _). Qed.
+  Lemma big_sepMS_later_2 Φ X :
+    ([∗ mset] y ∈ X, ▷ Φ y) ⊢ ▷ [∗ mset] y ∈ X, Φ y.
+  Proof. by rewrite big_opMS_commute. Qed.
+
+  Lemma big_sepMS_laterN `{BiAffine PROP} Φ n X :
+    ▷^n ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷^n Φ y).
+  Proof. apply (big_opMS_commute _). Qed.
+  Lemma big_sepMS_laterN_2 Φ n X :
+    ([∗ mset] y ∈ X, ▷^n Φ y) ⊢ ▷^n [∗ mset] y ∈ X, Φ y.
+  Proof. by rewrite big_opMS_commute. Qed.
+
   Lemma big_sepMS_persistently `{BiAffine PROP} Φ X :
     <pers> ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, <pers> (Φ y).
   Proof. apply (big_opMS_commute _). Qed.
@@ -1552,208 +1709,6 @@ Section gmultiset.
   Global Instance big_sepMS_affine Φ X :
     (∀ x, Affine (Φ x)) → Affine ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite big_opMS_eq /big_opMS_def. apply _. Qed.
-End gmultiset.
-End bi_big_op.
-
-(** * Properties for step-indexed BIs*)
-Section sbi_big_op.
-Context {PROP : bi}.
-Implicit Types Ps Qs : list PROP.
-Implicit Types A : Type.
-
-(** ** Big ops over lists *)
-Section list.
-  Context {A : Type}.
-  Implicit Types l : list A.
-  Implicit Types Φ Ψ : nat → A → PROP.
-
-  Lemma big_sepL_later `{BiAffine PROP} Φ l :
-    ▷ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷ Φ k x).
-  Proof. apply (big_opL_commute _). Qed.
-  Lemma big_sepL_later_2 Φ l :
-    ([∗ list] k↦x ∈ l, ▷ Φ k x) ⊢ ▷ [∗ list] k↦x ∈ l, Φ k x.
-  Proof. by rewrite (big_opL_commute _). Qed.
-
-  Lemma big_sepL_laterN `{BiAffine PROP} Φ n l :
-    ▷^n ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷^n Φ k x).
-  Proof. apply (big_opL_commute _). Qed.
-  Lemma big_sepL_laterN_2 Φ n l :
-    ([∗ list] k↦x ∈ l, ▷^n Φ k x) ⊢ ▷^n [∗ list] k↦x ∈ l, Φ k x.
-  Proof. by rewrite (big_opL_commute _). Qed.
-
-  Global Instance big_sepL_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
-    Timeless ([∗ list] k↦x ∈ [], Φ k x).
-  Proof. simpl; apply _. Qed.
-  Global Instance big_sepL_timeless `{!Timeless (emp%I : PROP)} Φ l :
-    (∀ k x, Timeless (Φ k x)) → Timeless ([∗ list] k↦x ∈ l, Φ k x).
-  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
-  Global Instance big_sepL_timeless_id `{!Timeless (emp%I : PROP)} Ps :
-    TCForall Timeless Ps → Timeless ([∗] Ps).
-  Proof. induction 1; simpl; apply _. Qed.
-End list.
-
-Section list2.
-  Context {A B : Type}.
-  Implicit Types Φ Ψ : nat → A → B → PROP.
-
-  Lemma big_sepL2_later_1 `{BiAffine PROP} Φ l1 l2 :
-    (▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ ◇ [∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2.
-  Proof.
-    rewrite !big_sepL2_alt later_and big_sepL_later (timeless ⌜ _ ⌝%I).
-    rewrite except_0_and. auto using and_mono, except_0_intro.
-  Qed.
-
-  Lemma big_sepL2_later_2 Φ l1 l2 :
-    ([∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2) ⊢ ▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2.
-  Proof.
-    rewrite !big_sepL2_alt later_and big_sepL_later_2.
-    auto using and_mono, later_intro.
-  Qed.
-
-  Lemma big_sepL2_laterN_2 Φ n l1 l2 :
-    ([∗ list] k↦y1;y2 ∈ l1;l2, ▷^n Φ k y1 y2) ⊢ ▷^n [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2.
-  Proof.
-    rewrite !big_sepL2_alt laterN_and big_sepL_laterN_2.
-    auto using and_mono, laterN_intro.
-  Qed.
-
-  Lemma big_sepL2_flip Φ l1 l2 :
-    ([∗ list] k↦y1;y2 ∈ l2; l1, Φ k y2 y1) ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2).
-  Proof.
-    revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2]//=; simplify_eq.
-    by rewrite IH.
-  Qed.
-
-  Global Instance big_sepL2_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
-    Timeless ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
-  Proof. simpl; apply _. Qed.
-  Global Instance big_sepL2_timeless `{!Timeless (emp%I : PROP)} Φ l1 l2 :
-    (∀ k x1 x2, Timeless (Φ k x1 x2)) →
-    Timeless ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
-  Proof. rewrite big_sepL2_alt. apply _. Qed.
-End list2.
-
-(** ** Big ops over finite maps *)
-Section gmap.
-  Context `{Countable K} {A : Type}.
-  Implicit Types m : gmap K A.
-  Implicit Types Φ Ψ : K → A → PROP.
-
-  Lemma big_sepM_later `{BiAffine PROP} Φ m :
-    ▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x).
-  Proof. apply (big_opM_commute _). Qed.
-  Lemma big_sepM_later_2 Φ m :
-    ([∗ map] k↦x ∈ m, ▷ Φ k x) ⊢ ▷ [∗ map] k↦x ∈ m, Φ k x.
-  Proof. by rewrite big_opM_commute. Qed.
-
-  Lemma big_sepM_laterN `{BiAffine PROP} Φ n m :
-    ▷^n ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷^n Φ k x).
-  Proof. apply (big_opM_commute _). Qed.
-  Lemma big_sepM_laterN_2 Φ n m :
-    ([∗ map] k↦x ∈ m, ▷^n Φ k x) ⊢ ▷^n [∗ map] k↦x ∈ m, Φ k x.
-  Proof. by rewrite big_opM_commute. Qed.
-
-  Global Instance big_sepM_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
-    Timeless ([∗ map] k↦x ∈ ∅, Φ k x).
-  Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
-  Global Instance big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
-    (∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x).
-  Proof. rewrite big_opM_eq. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
-End gmap.
-
-Section gmap2.
-  Context `{Countable K} {A B : Type}.
-  Implicit Types Φ Ψ : K → A → B → PROP.
-
-  Lemma big_sepM2_later_1 `{BiAffine PROP} Φ m1 m2 :
-    (▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
-    ⊢ ◇ ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2).
-  Proof.
-    rewrite big_sepM2_eq /big_sepM2_def later_and (timeless ⌜_⌝%I).
-    rewrite big_sepM_later except_0_and.
-    auto using and_mono_r, except_0_intro.
-  Qed.
-  Lemma big_sepM2_later_2 Φ m1 m2 :
-    ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2)
-    ⊢ ▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
-  Proof.
-    rewrite big_sepM2_eq /big_sepM2_def later_and -(later_intro ⌜_⌝%I).
-    apply and_mono_r. by rewrite big_opM_commute.
-  Qed.
-
-  Lemma big_sepM2_laterN_2 Φ n m1 m2 :
-    ([∗ map] k↦x1;x2 ∈ m1;m2, ▷^n Φ k x1 x2)
-    ⊢ ▷^n [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
-  Proof.
-    induction n as [|n IHn]; first done.
-    rewrite later_laterN -IHn -big_sepM2_later_2.
-    apply big_sepM2_mono. eauto.
-  Qed.
-
-  Lemma big_sepM2_flip Φ m1 m2 :
-    ([∗ map] k↦y1;y2 ∈ m2; m1, Φ k y2 y1) ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2).
-  Proof.
-    rewrite big_sepM2_eq /big_sepM2_def. apply and_proper; [apply pure_proper; naive_solver |].
-    rewrite -map_zip_with_flip map_zip_with_map_zip big_sepM_fmap.
-    apply big_sepM_proper. by intros k [b a].
-  Qed.
-
-  Global Instance big_sepM2_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
-    Timeless ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
-  Proof. rewrite big_sepM2_eq /big_sepM2_def map_zip_with_empty. apply _. Qed.
-  Global Instance big_sepM2_timeless `{!Timeless (emp%I : PROP)} Φ m1 m2 :
-    (∀ k x1 x2, Timeless (Φ k x1 x2)) →
-    Timeless ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
-  Proof. intros. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
-End gmap2.
-
-(** ** Big ops over finite sets *)
-Section gset.
-  Context `{Countable A}.
-  Implicit Types X : gset A.
-  Implicit Types Φ : A → PROP.
-
-  Lemma big_sepS_later `{BiAffine PROP} Φ X :
-    ▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y).
-  Proof. apply (big_opS_commute _). Qed.
-  Lemma big_sepS_later_2 Φ X :
-    ([∗ set] y ∈ X, ▷ Φ y) ⊢ ▷ ([∗ set] y ∈ X, Φ y).
-  Proof. by rewrite big_opS_commute. Qed.
-
-  Lemma big_sepS_laterN `{BiAffine PROP} Φ n X :
-    ▷^n ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷^n Φ y).
-  Proof. apply (big_opS_commute _). Qed.
-  Lemma big_sepS_laterN_2 Φ n X :
-    ([∗ set] y ∈ X, ▷^n Φ y) ⊢ ▷^n ([∗ set] y ∈ X, Φ y).
-  Proof. by rewrite big_opS_commute. Qed.
-
-  Global Instance big_sepS_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
-    Timeless ([∗ set] x ∈ ∅, Φ x).
-  Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
-  Global Instance big_sepS_timeless `{!Timeless (emp%I : PROP)} Φ X :
-    (∀ x, Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
-  Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
-End gset.
-
-(** ** Big ops over finite multisets *)
-Section gmultiset.
-  Context `{Countable A}.
-  Implicit Types X : gmultiset A.
-  Implicit Types Φ : A → PROP.
-
-  Lemma big_sepMS_later `{BiAffine PROP} Φ X :
-    ▷ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷ Φ y).
-  Proof. apply (big_opMS_commute _). Qed.
-  Lemma big_sepMS_later_2 Φ X :
-    ([∗ mset] y ∈ X, ▷ Φ y) ⊢ ▷ [∗ mset] y ∈ X, Φ y.
-  Proof. by rewrite big_opMS_commute. Qed.
-
-  Lemma big_sepMS_laterN `{BiAffine PROP} Φ n X :
-    ▷^n ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷^n Φ y).
-  Proof. apply (big_opMS_commute _). Qed.
-  Lemma big_sepMS_laterN_2 Φ n X :
-    ([∗ mset] y ∈ X, ▷^n Φ y) ⊢ ▷^n [∗ mset] y ∈ X, Φ y.
-  Proof. by rewrite big_opMS_commute. Qed.
 
   Global Instance big_sepMS_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
     Timeless ([∗ mset] x ∈ ∅, Φ x).
@@ -1762,4 +1717,4 @@ Section gmultiset.
     (∀ x, Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite big_opMS_eq /big_opMS_def. apply _. Qed.
 End gmultiset.
-End sbi_big_op.
+End big_op.
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 4a64793a0cc79df75d0f6564b205ee2216d61097..b6c10d542eddc892f94d3645be889c87a3015a6b 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -119,7 +119,7 @@ Notation "mP -∗? Q" := (bi_wandM mP Q)
 
 (** This class is required for the [iLöb] tactic. For most logics this class
 should not be inhabited directly, but the instance [Contractive (▷) → BiLöb PROP]
-in [derived_laws_sbi] should be used. A direct instance of the class is useful
+in [derived_laws_later] should be used. A direct instance of the class is useful
 when considering a BI logic with a discrete OFE, instead of a OFE that takes
 step-indexing of the logic in account.*)
 Class BiLöb (PROP : bi) :=
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws.v
similarity index 99%
rename from theories/bi/derived_laws_bi.v
rename to theories/bi/derived_laws.v
index 1127e290b4b9f33db6276c7f74b8d6b877c800b8..40641c9b975a54c79f0e2b5c1fe7298add4d6ff9 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws.v
@@ -10,7 +10,7 @@ From iris.algebra Require Import monoid.
 
 Module bi.
 Import interface.bi.
-Section bi_derived.
+Section derived.
 Context {PROP : bi}.
 Implicit Types φ : Prop.
 Implicit Types P Q R : PROP.
@@ -1551,5 +1551,5 @@ Qed.
 Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → PROP) :
   NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
-End bi_derived.
+End derived.
 End bi.
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_later.v
similarity index 99%
rename from theories/bi/derived_laws_sbi.v
rename to theories/bi/derived_laws_later.v
index 19bafd7bfde2abab9adff074be32961ce5b47cc3..7f3d4bd4e93b9a0d60a7f2cef929fb4be8622e58 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_later.v
@@ -1,10 +1,11 @@
-From iris.bi Require Export derived_laws_bi.
+From iris.bi Require Export derived_laws.
 From iris.algebra Require Import monoid.
 
 Module bi.
 Import interface.bi.
-Import derived_laws_bi.bi.
-Section sbi_derived.
+Import derived_laws.bi.
+
+Section later_derived.
 Context {PROP : bi}.
 Implicit Types φ : Prop.
 Implicit Types P Q R : PROP.
@@ -398,5 +399,5 @@ Proof. split; try apply _. apply laterN_intro. Qed.
 Global Instance bi_except_0_sep_entails_homomorphism :
   MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_except_0 PROP).
 Proof. split; try apply _. apply except_0_intro. Qed.
-End sbi_derived.
+End later_derived.
 End bi.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 24f4c237f29151889720cc74c3656b67cc75e8e8..9862bcd959f05e81187e958f753729ccb387388f 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,4 +1,4 @@
-From iris.bi Require Import interface derived_laws_sbi big_op.
+From iris.bi Require Import interface derived_laws_later big_op.
 From iris.bi Require Import plainly updates internal_eq.
 From iris.algebra Require Import monoid.
 
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 5a460db1ca45961fad65dd39457c41e327478644..c0044e908c5eecde2697d9c080af039c8194d1b4 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -121,7 +121,7 @@ Section bi_mixin.
   identity function, as the Löb axiom or contractiveness of later is not part of
   [BiLaterMixin]. For step-indexed BIs one should separately prove an instance
   of the class [BiLöb PROP] or [Contractive (▷)]. (Note that there is an
-  instance [Contractive (▷) → BiLöb PROP] in [derived_laws_sbi].)
+  instance [Contractive (▷) → BiLöb PROP] in [derived_laws_later].)
 
   For non step-indexed BIs one can get a "free" instance of [BiLaterMixin] using
   the smart constructor [bi_later_mixin_id] below. *)
diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
index 6e97b92e65b31f04af244213095d902e2788b051..6ecd8ec6f4a8cca9bd468c85124b177d36e471ee 100644
--- a/theories/bi/internal_eq.v
+++ b/theories/bi/internal_eq.v
@@ -1,5 +1,5 @@
-From iris.bi Require Import derived_laws_sbi big_op.
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+From iris.bi Require Import derived_laws_later big_op.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (** 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]
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index ec7b4666ac4e3ba9b1dc67ff1908d1eca9301c72..51253b19f4c192a4da0bb62e86b1ea5c1f38f937 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -1,5 +1,5 @@
 From iris.bi Require Export bi.
-From iris.proofmode Require Import classes class_instances_bi.
+From iris.proofmode Require Import classes class_instances.
 Set Default Proof Using "Type".
 
 Class Fractional {PROP : bi} (Φ : Qp → PROP) :=
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index f99e4b68a5c74ec6909a8ca971caa2ca2f27a72e..a5b5af0210bf293e7b5abf9ac2c7cf67c656cf2c 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,6 +1,6 @@
-From iris.bi Require Import derived_laws_sbi big_op internal_eq.
+From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris.algebra Require Import monoid.
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 Class Plainly (A : Type) := plainly : A → A.
 Hint Mode Plainly ! : typeclass_instances.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 7b2498dafe59a76bb95e473b08da7b811b664722..51f54aa594416bc12dfbfd5497455cb50f101db5 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -1,6 +1,6 @@
 From stdpp Require Import coPset.
-From iris.bi Require Import interface derived_laws_sbi big_op plainly.
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+From iris.bi Require Import interface derived_laws_later big_op plainly.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (* We first define operational type classes for the notations, and then later
 bundle these operational type classes with the laws. *)
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances.v
similarity index 81%
rename from theories/proofmode/class_instances_bi.v
rename to theories/proofmode/class_instances.v
index 30f3d187957a5ffd587f672309bac73a26edaf91..e3e88c265dee97f73af548b8d574c4d0e5c36f99 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances.v
@@ -1,6 +1,7 @@
 From stdpp Require Import nat_cancel.
-From iris.bi Require Import bi tactics telescopes.
-From iris.proofmode Require Import base modality_instances classes ltac_tactics.
+From iris.bi Require Import bi telescopes.
+From iris.proofmode Require Import base modality_instances classes.
+From iris.proofmode Require Import ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -25,7 +26,7 @@ Proof. by rewrite /FromExist. Qed.
 Hint Extern 0 (FromExist _ _) =>
   notypeclasses refine (from_exist_exist _) : typeclass_instances.
 
-Section bi_instances.
+Section class_instances.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 Implicit Types mP : option PROP.
@@ -52,17 +53,6 @@ Proof.
   apply as_emp_valid_forall.
 Qed.
 
-(* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
-   sure this instance is not used when there is no embedding between
-   PROP and PROP'.
-   The first [`{BiEmbed PROP PROP'}] is not considered as a premise by
-   Coq TC search mechanism because the rest of the hypothesis is dependent
-   on it. *)
-Global Instance as_emp_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
-  BiEmbed PROP PROP' →
-  AsEmpValid0 φ P → AsEmpValid φ ⎡P⎤.
-Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ ->. rewrite embed_emp_valid //. Qed.
-
 (** FromAffinely *)
 Global Instance from_affinely_affine P : Affine P → FromAffinely P P.
 Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
@@ -155,10 +145,6 @@ Proof.
   by rewrite bi_tforall_forall forall_elim.
 Qed.
 
-Global Instance from_assumption_bupd `{BiBUpd PROP} p P Q :
-  FromAssumption p P Q → KnownRFromAssumption p P (|==> Q).
-Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_intro. Qed.
-
 (** IntoPure *)
 Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
 Proof. by rewrite /IntoPure. Qed.
@@ -209,9 +195,6 @@ Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
 Global Instance into_pure_persistently P φ :
   IntoPure P φ → IntoPure (<pers> P) φ.
 Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
-Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ :
-  IntoPure P φ → IntoPure ⎡P⎤ φ.
-Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed.
 
 (** FromPure *)
 Global Instance from_pure_emp : @FromPure PROP true emp True.
@@ -303,13 +286,6 @@ Proof.
   rewrite /FromPure=> <- /=. rewrite -affinely_affinely_if.
   by rewrite -persistent_absorbingly_affinely_2.
 Qed.
-Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
-  FromPure a P φ → FromPure a ⎡P⎤ φ.
-Proof. rewrite /FromPure=> <-. by rewrite -embed_pure embed_affinely_if_2. Qed.
-
-Global Instance from_pure_bupd `{BiBUpd PROP} a P φ :
-  FromPure a P φ → FromPure a (|==> P) φ.
-Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
 
 (** IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
@@ -329,11 +305,6 @@ Proof.
     eauto using persistently_mono, intuitionistically_elim,
     intuitionistically_into_persistently_1.
 Qed.
-Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
-  IntoPersistent p P Q → IntoPersistent p ⎡P⎤ ⎡Q⎤ | 0.
-Proof.
-  rewrite /IntoPersistent -embed_persistently -embed_persistently_if=> -> //.
-Qed.
 Global Instance into_persistent_here P : IntoPersistent true P P | 1.
 Proof. by rewrite /IntoPersistent. Qed.
 Global Instance into_persistent_persistent P :
@@ -361,34 +332,6 @@ Global Instance from_modal_absorbingly P :
   FromModal modality_id (<absorb> P) (<absorb> P) P.
 Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.
 
-(* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
-the embedding over the modality. *)
-Global Instance from_modal_embed `{BiEmbed PROP PROP'} (P : PROP) :
-  FromModal (@modality_embed PROP PROP' _) ⎡P⎤ ⎡P⎤ P.
-Proof. by rewrite /FromModal. Qed.
-
-Global Instance from_modal_id_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
-  FromModal modality_id sel P Q →
-  FromModal modality_id sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. by rewrite /FromModal /= =><-. Qed.
-
-Global Instance from_modal_affinely_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
-  FromModal modality_affinely sel P Q →
-  FromModal modality_affinely sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely_2. Qed.
-Global Instance from_modal_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
-  FromModal modality_persistently sel P Q →
-  FromModal modality_persistently sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
-Global Instance from_modal_intuitionistically_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
-  FromModal modality_intuitionistically sel P Q →
-  FromModal modality_intuitionistically sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_intuitionistically_2. Qed.
-
-Global Instance from_modal_bupd `{BiBUpd PROP} P :
-  FromModal modality_id (|==> P) (|==> P) P.
-Proof. by rewrite /FromModal /= -bupd_intro. Qed.
-
 (** IntoWand *)
 Global Instance into_wand_wand' p q (P Q P' Q' : PROP) :
   IntoWand' p q (P -∗ Q) P' Q' → IntoWand p q (P -∗ Q) P' Q' | 100.
@@ -508,69 +451,16 @@ Global Instance into_wand_persistently_false q R P Q :
   Absorbing R → IntoWand false q R P Q → IntoWand false q (<pers> R) P Q.
 Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.
 
-Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q :
-  IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤.
-Proof. by rewrite /IntoWand !embed_intuitionistically_if_2 -embed_wand=> ->. Qed.
-
-(* There are two versions for [IntoWand ⎡RR⎤ ...] with the argument being
-[<affine> ⎡PP⎤]. When the wand [⎡RR⎤] resides in the intuitionistic context
-the result of wand elimination will have the affine modality. Otherwise, it
-won't. Note that when the wand [⎡RR⎤] is under an affine modality, the instance
-[into_wand_affine] would already have been used. *)
-Global Instance into_wand_affine_embed_true `{BiEmbed PROP PROP'} q (PP QQ RR : PROP) :
-  IntoWand true q RR PP QQ → IntoWand true q ⎡RR⎤ (<affine> ⎡PP⎤) (<affine> ⎡QQ⎤) | 100.
-Proof.
-  rewrite /IntoWand /=.
-  rewrite -(intuitionistically_idemp ⎡ _ ⎤%I) embed_intuitionistically_2=> ->.
-  apply bi.wand_intro_l. destruct q; simpl.
-  - rewrite affinely_elim  -(intuitionistically_idemp ⎡ _ ⎤%I).
-    rewrite embed_intuitionistically_2 intuitionistically_sep_2 -embed_sep.
-    by rewrite wand_elim_r intuitionistically_affinely.
-  - by rewrite intuitionistically_affinely affinely_sep_2 -embed_sep wand_elim_r.
-Qed.
-Global Instance into_wand_affine_embed_false `{BiEmbed PROP PROP'} q (PP QQ RR : PROP) :
-  IntoWand false q RR (<affine> PP) QQ → IntoWand false q ⎡RR⎤ (<affine> ⎡PP⎤) ⎡QQ⎤ | 100.
-Proof.
-  rewrite /IntoWand /= => ->.
-  by rewrite embed_affinely_2 embed_intuitionistically_if_2 embed_wand.
-Qed.
-
-
-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 !intuitionistically_if_elim HR.
-  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
-Qed.
-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 intuitionistically_if_elim HR.
-  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
-Qed.
-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 intuitionistically_if_elim bupd_wand_r.
-Qed.
-
 (** FromWand *)
 Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
 Proof. by rewrite /FromWand. Qed.
 Global Instance from_wand_wandM mP1 P2 :
   FromWand (mP1 -∗? P2) (default emp mP1)%I P2.
 Proof. by rewrite /FromWand wandM_sound. Qed.
-Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
-  FromWand P Q1 Q2 → FromWand ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromWand -embed_wand => <-. Qed.
 
 (** FromImpl *)
 Global Instance from_impl_impl P1 P2 : FromImpl (P1 → P2) P1 P2.
 Proof. by rewrite /FromImpl. Qed.
-Global Instance from_impl_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
-  FromImpl P Q1 Q2 → FromImpl ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
 
 (** FromAnd *)
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
@@ -602,10 +492,6 @@ Global Instance from_and_persistently_sep P Q1 Q2 :
   FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
 Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
 
-Global Instance from_and_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
-  FromAnd P Q1 Q2 → FromAnd ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromAnd -embed_and => <-. Qed.
-
 Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP) l x l' :
   IsCons l x l' →
   Persistent (Φ 0 x) →
@@ -671,10 +557,6 @@ Global Instance from_sep_persistently P Q1 Q2 :
   FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
 
-Global Instance from_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromSep -embed_sep => <-. Qed.
-
 Global Instance from_sep_big_sepL_cons {A} (Φ : nat → A → PROP) l x l' :
   IsCons l x l' →
   FromSep ([∗ list] k ↦ y ∈ l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y).
@@ -703,10 +585,6 @@ Global Instance from_sep_big_sepMS_disj_union `{Countable A} (Φ : A → PROP) X
   FromSep ([∗ mset] y ∈ X1 ⊎ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
 Proof. by rewrite /FromSep big_sepMS_disj_union. Qed.
 
-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.
-
 (** IntoAnd *)
 Global Instance into_and_and p P Q : IntoAnd p (P ∧ Q) P Q | 10.
 Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
@@ -758,12 +636,6 @@ Proof.
   - rewrite -persistently_and !intuitionistically_persistently_elim //.
   - intros ->. by rewrite persistently_and.
 Qed.
-Global Instance into_and_embed `{BiEmbed PROP PROP'} p P Q1 Q2 :
-  IntoAnd p P Q1 Q2 → IntoAnd p ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof.
-  rewrite /IntoAnd -embed_and=> HP. apply intuitionistically_if_intro'.
-  by rewrite embed_intuitionistically_if_2 HP intuitionistically_if_elim.
-Qed.
 
 (** IntoSep *)
 Global Instance into_sep_sep P Q : IntoSep (P ∗ Q) P Q.
@@ -796,10 +668,6 @@ Qed.
 Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
 
-Global Instance into_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
-  IntoSep P Q1 Q2 → IntoSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. rewrite /IntoSep -embed_sep=> -> //. Qed.
-
 Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (<affine> P) (<affine> Q1) (<affine> Q2) | 0.
 Proof. rewrite /IntoSep /= => ->. by rewrite affinely_sep. Qed.
@@ -875,16 +743,6 @@ Global Instance from_or_persistently P Q1 Q2 :
   FromOr P Q1 Q2 →
   FromOr (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
-Global Instance from_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromOr -embed_or => <-. Qed.
-
-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.
 
 (** IntoOr *)
 Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
@@ -904,9 +762,6 @@ Global Instance into_or_persistently P Q1 Q2 :
   IntoOr P Q1 Q2 →
   IntoOr (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
-Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
-  IntoOr P Q1 Q2 → IntoOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /IntoOr -embed_or => <-. Qed.
 
 (** FromExist *)
 Global Instance from_exist_texist {TT : tele} (Φ : TT → PROP) :
@@ -927,15 +782,6 @@ Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
 Global Instance from_exist_persistently {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (<pers> P) (λ a, <pers> (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
-Global Instance from_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
-  FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /FromExist -embed_exist => <-. Qed.
-
-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.
 
 (** IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ.
@@ -971,9 +817,6 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
 Global Instance into_exist_persistently {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (<pers> P) (λ a, <pers> (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
-Global Instance into_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
 
 (** IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
@@ -990,9 +833,6 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP intuitionistically_forall. Qed.
 Global Instance into_forall_persistently {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (<pers> P) (λ a, <pers> (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
-Global Instance into_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
-  IntoForall P Φ → IntoForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /IntoForall -embed_forall => <-. Qed.
 
 Global Instance into_forall_impl_pure a φ P Q :
   FromPureT a P φ →
@@ -1062,13 +902,6 @@ Qed.
 Global Instance from_forall_persistently {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (<pers> P) (λ a, <pers> (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
-Global Instance from_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /FromForall -embed_forall => <-. Qed.
-
-(** IntoInv *)
-Global Instance into_inv_embed {PROP' : bi} `{BiEmbed PROP PROP'} P N :
-  IntoInv P N → IntoInv ⎡P⎤ N := {}.
 
 (** ElimModal *)
 Global Instance elim_modal_wand φ p p' P P' Q Q' R :
@@ -1098,24 +931,6 @@ Proof.
     absorbingly_sep_l wand_elim_r absorbing_absorbingly.
 Qed.
 
-Global Instance elim_modal_bupd `{BiBUpd PROP} p P Q :
-  ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
-Proof.
-  by rewrite /ElimModal
-    intuitionistically_if_elim bupd_frame_r wand_elim_r bupd_trans.
-Qed.
-
-Global Instance elim_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
-    p p' φ (P P' : PROP') (Q Q' : PROP) :
-  ElimModal φ p p' P P' (|==> ⎡Q⎤)%I (|==> ⎡Q'⎤)%I →
-  ElimModal φ p p' P P' ⎡|==> Q⎤ ⎡|==> Q'⎤.
-Proof. by rewrite /ElimModal !embed_bupd. Qed.
-Global Instance elim_modal_embed_bupd_hyp `{BiEmbedBUpd PROP PROP'}
-    p p' φ (P : PROP) (P' Q Q' : PROP') :
-  ElimModal φ p p' (|==> ⎡P⎤)%I P' Q Q' →
-  ElimModal φ p p' ⎡|==> P⎤ P' Q Q'.
-Proof. by rewrite /ElimModal !embed_bupd. Qed.
-
 (** AddModal *)
 Global Instance add_modal_wand P P' Q R :
   AddModal P P' Q → AddModal P P' (R -∗ Q).
@@ -1134,18 +949,10 @@ Qed.
 Global Instance add_modal_tforall {TT : tele} P P' (Φ : TT → PROP) :
   (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀.. x, Φ x).
 Proof. rewrite /AddModal bi_tforall_forall. apply add_modal_forall. Qed.
-Global Instance add_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
-       (P P' : PROP') (Q : PROP) :
-  AddModal P P' (|==> ⎡Q⎤)%I → AddModal P P' ⎡|==> Q⎤.
-Proof. by rewrite /AddModal !embed_bupd. Qed.
-
-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.
 
 (** ElimInv *)
 Global Instance elim_inv_acc_without_close {X : Type}
-       φ Pinv Pin
-       M1 M2 α β mγ Q (Q' : X → PROP) :
+     φ Pinv Pin (M1 M2 : PROP → PROP) α β mγ Q (Q' : X → PROP) :
   IntoAcc (X:=X) Pinv φ Pin M1 M2 α β mγ →
   ElimAcc (X:=X) M1 M2 α β mγ Q Q' →
   ElimInv φ Pinv Pin α None Q Q'.
@@ -1161,8 +968,7 @@ Qed.
 [None] or [Some _] there, so we want to reduce the combinator before showing the
 goal to the user. *)
 Global Instance elim_inv_acc_with_close {X : Type}
-       φ1 φ2 Pinv Pin
-       M1 M2 α β mγ Q Q' :
+    φ1 φ2 Pinv Pin (M1 M2 : PROP → PROP) α β mγ Q Q' :
   IntoAcc Pinv φ1 Pin M1 M2 α β mγ →
   (∀ R, ElimModal φ2 false false (M1 R) R Q Q') →
   ElimInv (X:=X) (φ1 ∧ φ2) Pinv Pin
@@ -1175,12 +981,4 @@ Proof.
   iMod (Hacc with "Hinv Hin") as (x) "[Hα Hclose]"; first done.
   iApply "Hcont". simpl. iSplitL "Hα"; done.
 Qed.
-
-(** IntoEmbed *)
-Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
-  IntoEmbed ⎡P⎤ P.
-Proof. by rewrite /IntoEmbed. Qed.
-Global Instance into_embed_affinely `{BiEmbedBUpd PROP PROP'} (P : PROP') (Q : PROP) :
-  IntoEmbed P Q → IntoEmbed (<affine> P) (<affine> Q).
-Proof. rewrite /IntoEmbed=> ->. by rewrite embed_affinely_2. Qed.
-End bi_instances.
+End class_instances.
diff --git a/theories/proofmode/class_instances_embedding.v b/theories/proofmode/class_instances_embedding.v
new file mode 100644
index 0000000000000000000000000000000000000000..6e964003e154d4c1c45866ec35ae162d30835dd2
--- /dev/null
+++ b/theories/proofmode/class_instances_embedding.v
@@ -0,0 +1,211 @@
+From iris.bi Require Import bi.
+From iris.proofmode Require Import modality_instances classes.
+Set Default Proof Using "Type".
+Import bi.
+
+(** We add a useless hypothesis [BiEmbed PROP PROP'] in order to make sure this
+instance is not used when there is no embedding between [PROP] and [PROP']. The
+first [`{BiEmbed PROP PROP'}] is not considered as a premise by Coq TC search
+mechanism because the rest of the hypothesis is dependent on it. *)
+Global Instance as_emp_valid_embed `{!BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
+  BiEmbed PROP PROP' →
+  AsEmpValid0 φ P → AsEmpValid φ ⎡P⎤.
+Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ ->. rewrite embed_emp_valid //. Qed.
+
+Section class_instances_embedding.
+Context `{!BiEmbed PROP PROP'}.
+Implicit Types P Q R : PROP.
+
+Global Instance into_pure_embed P φ :
+  IntoPure P φ → IntoPure ⎡P⎤ φ.
+Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed.
+
+Global Instance from_pure_embed a P φ :
+  FromPure a P φ → FromPure a ⎡P⎤ φ.
+Proof. rewrite /FromPure=> <-. by rewrite -embed_pure embed_affinely_if_2. Qed.
+
+Global Instance into_persistent_embed p P Q :
+  IntoPersistent p P Q → IntoPersistent p ⎡P⎤ ⎡Q⎤ | 0.
+Proof.
+  rewrite /IntoPersistent -embed_persistently -embed_persistently_if=> -> //.
+Qed.
+
+(* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
+the embedding over the modality. *)
+Global Instance from_modal_embed P :
+  FromModal (@modality_embed PROP PROP' _) ⎡P⎤ ⎡P⎤ P.
+Proof. by rewrite /FromModal. Qed.
+
+Global Instance from_modal_id_embed `(sel : A) P Q :
+  FromModal modality_id sel P Q →
+  FromModal modality_id sel ⎡P⎤ ⎡Q⎤ | 100.
+Proof. by rewrite /FromModal /= =><-. Qed.
+
+Global Instance from_modal_affinely_embed `(sel : A) P Q :
+  FromModal modality_affinely sel P Q →
+  FromModal modality_affinely sel ⎡P⎤ ⎡Q⎤ | 100.
+Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely_2. Qed.
+Global Instance from_modal_persistently_embed `(sel : A) P Q :
+  FromModal modality_persistently sel P Q →
+  FromModal modality_persistently sel ⎡P⎤ ⎡Q⎤ | 100.
+Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
+Global Instance from_modal_intuitionistically_embed `(sel : A) P Q :
+  FromModal modality_intuitionistically sel P Q →
+  FromModal modality_intuitionistically sel ⎡P⎤ ⎡Q⎤ | 100.
+Proof. rewrite /FromModal /= =><-. by rewrite embed_intuitionistically_2. Qed.
+
+Global Instance into_wand_embed p q R P Q :
+  IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤.
+Proof. by rewrite /IntoWand !embed_intuitionistically_if_2 -embed_wand=> ->. Qed.
+
+(* There are two versions for [IntoWand ⎡R⎤ ...] with the argument being
+[<affine> ⎡P⎤]. When the wand [⎡R⎤] resides in the intuitionistic context
+the result of wand elimination will have the affine modality. Otherwise, it
+won't. Note that when the wand [⎡R⎤] is under an affine modality, the instance
+[into_wand_affine] would already have been used. *)
+Global Instance into_wand_affine_embed_true q P Q R :
+  IntoWand true q R P Q → IntoWand true q ⎡R⎤ (<affine> ⎡P⎤) (<affine> ⎡Q⎤) | 100.
+Proof.
+  rewrite /IntoWand /=.
+  rewrite -(intuitionistically_idemp ⎡ _ ⎤%I) embed_intuitionistically_2=> ->.
+  apply bi.wand_intro_l. destruct q; simpl.
+  - rewrite affinely_elim  -(intuitionistically_idemp ⎡ _ ⎤%I).
+    rewrite embed_intuitionistically_2 intuitionistically_sep_2 -embed_sep.
+    by rewrite wand_elim_r intuitionistically_affinely.
+  - by rewrite intuitionistically_affinely affinely_sep_2 -embed_sep wand_elim_r.
+Qed.
+Global Instance into_wand_affine_embed_false q P Q R :
+  IntoWand false q R (<affine> P) Q →
+  IntoWand false q ⎡R⎤ (<affine> ⎡P⎤) ⎡Q⎤ | 100.
+Proof.
+  rewrite /IntoWand /= => ->.
+  by rewrite embed_affinely_2 embed_intuitionistically_if_2 embed_wand.
+Qed.
+
+Global Instance from_wand_embed P Q1 Q2 :
+  FromWand P Q1 Q2 → FromWand ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromWand -embed_wand => <-. Qed.
+
+Global Instance from_impl_embed P Q1 Q2 :
+  FromImpl P Q1 Q2 → FromImpl ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
+
+Global Instance from_and_embed P Q1 Q2 :
+  FromAnd P Q1 Q2 → FromAnd ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromAnd -embed_and => <-. Qed.
+
+Global Instance from_sep_embed P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromSep -embed_sep => <-. Qed.
+
+Global Instance into_and_embed p P Q1 Q2 :
+  IntoAnd p P Q1 Q2 → IntoAnd p ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof.
+  rewrite /IntoAnd -embed_and=> HP. apply intuitionistically_if_intro'.
+  by rewrite embed_intuitionistically_if_2 HP intuitionistically_if_elim.
+Qed.
+
+Global Instance into_sep_embed P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. rewrite /IntoSep -embed_sep=> -> //. Qed.
+
+Global Instance from_or_embed P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromOr -embed_or => <-. Qed.
+
+Global Instance into_or_embed P Q1 Q2 :
+  IntoOr P Q1 Q2 → IntoOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /IntoOr -embed_or => <-. Qed.
+
+Global Instance from_exist_embed {A} P (Φ : A → PROP) :
+  FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /FromExist -embed_exist => <-. Qed.
+
+Global Instance into_exist_embed {A} P (Φ : A → PROP) :
+  IntoExist P Φ → IntoExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
+
+Global Instance into_forall_embed {A} P (Φ : A → PROP) :
+  IntoForall P Φ → IntoForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /IntoForall -embed_forall => <-. Qed.
+
+Global Instance from_forall_embed {A} P (Φ : A → PROP) :
+  FromForall P Φ → FromForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /FromForall -embed_forall => <-. Qed.
+
+Global Instance into_inv_embed P N : IntoInv P N → IntoInv ⎡P⎤ N := {}.
+
+Global Instance is_except_0_embed `{!BiEmbedLater PROP PROP'} P :
+  IsExcept0 P → IsExcept0 ⎡P⎤.
+Proof. by rewrite /IsExcept0 -embed_except_0=>->. Qed.
+
+Global Instance from_modal_later_embed `{!BiEmbedLater PROP PROP'} `(sel : A) n P Q :
+  FromModal (modality_laterN n) sel P Q →
+  FromModal (modality_laterN n) sel ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromModal /= =><-. by rewrite embed_laterN. Qed.
+
+Global Instance from_modal_plainly_embed
+    `{!BiPlainly PROP, !BiPlainly PROP', !BiEmbedPlainly PROP PROP'} `(sel : A) P Q :
+  FromModal modality_plainly sel P Q →
+  FromModal (PROP2:=PROP') modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
+Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
+
+Global Instance into_internal_eq_embed
+    `{!BiInternalEq PROP, !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
+    {A : ofeT} (x y : A) (P : PROP) :
+  IntoInternalEq P x y → IntoInternalEq (⎡P⎤ : PROP')%I x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
+
+Global Instance into_except_0_embed `{!BiEmbedLater PROP PROP'} P Q :
+  IntoExcept0 P Q → IntoExcept0 ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /IntoExcept0=> ->. by rewrite embed_except_0. Qed.
+
+Global Instance elim_modal_embed_bupd_goal
+    `{!BiBUpd PROP, !BiBUpd PROP', !BiEmbedBUpd PROP PROP'}
+    p p' φ (P P' : PROP') (Q Q' : PROP) :
+  ElimModal φ p p' P P' (|==> ⎡Q⎤)%I (|==> ⎡Q'⎤)%I →
+  ElimModal φ p p' P P' ⎡|==> Q⎤ ⎡|==> Q'⎤.
+Proof. by rewrite /ElimModal !embed_bupd. Qed.
+Global Instance elim_modal_embed_bupd_hyp
+    `{!BiBUpd PROP, !BiBUpd PROP', !BiEmbedBUpd PROP PROP'}
+    p p' φ (P : PROP) (P' Q Q' : PROP') :
+  ElimModal φ p p' (|==> ⎡P⎤)%I P' Q Q' →
+  ElimModal φ p p' ⎡|==> P⎤ P' Q Q'.
+Proof. by rewrite /ElimModal !embed_bupd. Qed.
+
+Global Instance elim_modal_embed_fupd_goal
+    `{!BiFUpd PROP, !BiFUpd PROP', !BiEmbedFUpd PROP PROP'}
+    p p' φ E1 E2 E3 (P P' : PROP') (Q Q' : PROP) :
+  ElimModal φ p p' P P' (|={E1,E3}=> ⎡Q⎤)%I (|={E2,E3}=> ⎡Q'⎤)%I →
+  ElimModal φ p p' P P' ⎡|={E1,E3}=> Q⎤ ⎡|={E2,E3}=> Q'⎤.
+Proof. by rewrite /ElimModal !embed_fupd. Qed.
+Global Instance elim_modal_embed_fupd_hyp
+    `{!BiFUpd PROP, !BiFUpd PROP', !BiEmbedFUpd PROP PROP'}
+    p p' φ E1 E2 (P : PROP) (P' Q Q' : PROP') :
+  ElimModal φ p p' (|={E1,E2}=> ⎡P⎤)%I P' Q Q' →
+  ElimModal φ p p' ⎡|={E1,E2}=> P⎤ P' Q Q'.
+Proof. by rewrite /ElimModal embed_fupd. Qed.
+
+Global Instance add_modal_embed_bupd_goal
+    `{!BiBUpd PROP, !BiBUpd PROP', !BiEmbedBUpd PROP PROP'}
+    (P P' : PROP') (Q : PROP) :
+  AddModal P P' (|==> ⎡Q⎤)%I → AddModal P P' ⎡|==> Q⎤.
+Proof. by rewrite /AddModal !embed_bupd. Qed.
+
+Global Instance add_modal_embed_fupd_goal
+    `{!BiFUpd PROP, !BiFUpd PROP', !BiEmbedFUpd PROP PROP'}
+    E1 E2 (P P' : PROP') (Q : PROP) :
+  AddModal P P' (|={E1,E2}=> ⎡Q⎤)%I → AddModal P P' ⎡|={E1,E2}=> Q⎤.
+Proof. by rewrite /AddModal !embed_fupd. Qed.
+
+Global Instance into_embed_embed P : IntoEmbed ⎡P⎤ P.
+Proof. by rewrite /IntoEmbed. Qed.
+Global Instance into_embed_affinely
+    `{!BiBUpd PROP, !BiBUpd PROP', !BiEmbedBUpd PROP PROP'} (P : PROP') (Q : PROP) :
+  IntoEmbed P Q → IntoEmbed (<affine> P) (<affine> Q).
+Proof. rewrite /IntoEmbed=> ->. by rewrite embed_affinely_2. Qed.
+
+Global Instance into_later_embed`{!BiEmbedLater PROP PROP'} n P Q :
+  IntoLaterN false n P Q → IntoLaterN false n ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite embed_laterN. Qed.
+End class_instances_embedding.
diff --git a/theories/proofmode/class_instances_internal_eq.v b/theories/proofmode/class_instances_internal_eq.v
new file mode 100644
index 0000000000000000000000000000000000000000..c33c76c7929de18128c85c4b968a358ad75208d0
--- /dev/null
+++ b/theories/proofmode/class_instances_internal_eq.v
@@ -0,0 +1,50 @@
+From stdpp Require Import nat_cancel.
+From iris.bi Require Import bi.
+From iris.proofmode Require Import modality_instances classes.
+Set Default Proof Using "Type".
+Import bi.
+
+Section class_instances_internal_eq.
+Context `{!BiInternalEq PROP}.
+Implicit Types P Q R : PROP.
+
+Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
+  @FromPure PROP false (a ≡ b) (a ≡ b).
+Proof. by rewrite /FromPure pure_internal_eq. Qed.
+
+Global Instance into_pure_eq {A : ofeT} (a b : A) :
+  Discrete a → @IntoPure PROP (a ≡ b) (a ≡ b).
+Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
+
+Global Instance from_modal_Next {A : ofeT} (x y : A) :
+  FromModal (PROP1:=PROP) (PROP2:=PROP) (modality_laterN 1)
+    (▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
+Proof. by rewrite /FromModal /= later_equivI. Qed.
+
+Global Instance into_laterN_Next {A : ofeT} only_head n n' (x y : A) :
+  NatCancel n 1 n' 0 →
+  IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
+Proof.
+  rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel Nat.add_0_r.
+  move=> <-. rewrite later_equivI. by rewrite Nat.add_comm /= -laterN_intro.
+Qed.
+
+Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
+  @IntoInternalEq PROP _ A (x ≡ y) x y.
+Proof. by rewrite /IntoInternalEq. Qed.
+Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
+Global Instance into_internal_eq_intuitionistically {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (□ P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.
+Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
+Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (■ P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
+Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
+End class_instances_internal_eq.
\ No newline at end of file
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_later.v
similarity index 56%
rename from theories/proofmode/class_instances_sbi.v
rename to theories/proofmode/class_instances_later.v
index 3e40fc8dcb29cd5855821f6a53570e7388984d46..7b2271f5b086d612af47399e9375f301d6ff2ad9 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_later.v
@@ -1,10 +1,10 @@
 From stdpp Require Import nat_cancel.
-From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import base modality_instances classes class_instances_bi ltac_tactics.
+From iris.bi Require Import bi.
+From iris.proofmode Require Import modality_instances classes.
 Set Default Proof Using "Type".
 Import bi.
 
-Section sbi_instances.
+Section class_instances_later.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 
@@ -19,27 +19,7 @@ Global Instance from_assumption_except_0 p P Q :
   FromAssumption p P Q → KnownRFromAssumption p P (◇ Q)%I.
 Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply except_0_intro. Qed.
 
-Global Instance from_assumption_fupd `{BiBUpdFUpd PROP} E p P Q :
-  FromAssumption p P (|==> Q) → KnownRFromAssumption p P (|={E}=> Q)%I.
-Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_fupd. Qed.
-
-Global Instance from_assumption_plainly_l_true `{BiPlainly PROP} P Q :
-  FromAssumption true P Q → KnownLFromAssumption true (■ P) Q.
-Proof.
-  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
-  rewrite intuitionistically_plainly_elim //.
-Qed.
-Global Instance from_assumption_plainly_l_false `{BiPlainly PROP, BiAffine PROP} P Q :
-  FromAssumption true P Q → KnownLFromAssumption false (■ P) Q.
-Proof.
-  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
-  rewrite plainly_elim_persistently intuitionistically_into_persistently //.
-Qed.
-
 (** FromPure *)
-Global Instance from_pure_internal_eq `{!BiInternalEq PROP} {A : ofeT} (a b : A) :
-  @FromPure PROP false (a ≡ b) (a ≡ b).
-Proof. by rewrite /FromPure pure_internal_eq. Qed.
 Global Instance from_pure_later a P φ : FromPure a P φ → FromPure a (▷ P) φ.
 Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
 Global Instance from_pure_laterN a n P φ : FromPure a P φ → FromPure a (▷^n P) φ.
@@ -47,23 +27,6 @@ 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_fupd `{BiFUpd PROP} a E P φ :
-  FromPure a P φ → FromPure a (|={E}=> P) φ.
-Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
-
-Global Instance from_pure_plainly `{BiPlainly PROP} P φ :
-  FromPure false P φ → FromPure false (■ P) φ.
-Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
-
-(** IntoPure *)
-Global Instance into_pure_eq `{!BiInternalEq PROP} {A : ofeT} (a b : A) :
-  Discrete a → @IntoPure PROP (a ≡ b) (a ≡ b).
-Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
-
-Global Instance into_pure_plainly `{BiPlainly PROP} P φ :
-  IntoPure P φ → IntoPure (■ P) φ.
-Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
-
 (** IntoWand *)
 Global Instance into_wand_later p q R P Q :
   IntoWand p q R P Q → IntoWand p q (▷ R) (▷ P) (▷ Q).
@@ -92,33 +55,6 @@ Proof.
              (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
 Qed.
 
-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 !intuitionistically_if_elim HR.
-  apply wand_intro_l. by rewrite fupd_sep wand_elim_r.
-Qed.
-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 intuitionistically_if_elim HR.
-  apply wand_intro_l. by rewrite fupd_frame_l wand_elim_r.
-Qed.
-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 /= => ->.
-  apply wand_intro_l. by rewrite intuitionistically_if_elim fupd_wand_r.
-Qed.
-
-Global Instance into_wand_plainly_true `{BiPlainly PROP} q R P Q :
-  IntoWand true q R P Q → IntoWand true q (■ R) P Q.
-Proof. rewrite /IntoWand /= intuitionistically_plainly_elim //. Qed.
-Global Instance into_wand_plainly_false `{BiPlainly PROP} q R P Q :
-  Absorbing R → IntoWand false q R P Q → IntoWand false q (■ R) P Q.
-Proof. intros ?. by rewrite /IntoWand plainly_elim. Qed.
-
 (** FromAnd *)
 Global Instance from_and_later P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd (▷ P) (▷ Q1) (▷ Q2).
@@ -130,10 +66,6 @@ Global Instance from_and_except_0 P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /FromAnd=><-. by rewrite except_0_and. Qed.
 
-Global Instance from_and_plainly `{BiPlainly PROP} P Q1 Q2 :
-  FromAnd P Q1 Q2 → FromAnd (■ P) (■ Q1) (■ Q2).
-Proof. rewrite /FromAnd=> <-. by rewrite plainly_and. Qed.
-
 (** FromSep *)
 Global Instance from_sep_later P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
@@ -145,14 +77,6 @@ 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 `{BiFUpd PROP} 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_sep_plainly `{BiPlainly PROP} P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (■ P) (■ Q1) (■ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite plainly_sep_2. Qed.
-
 (** IntoAnd *)
 Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
@@ -176,15 +100,6 @@ Proof.
              intuitionistically_if_elim except_0_and.
 Qed.
 
-Global Instance into_and_plainly `{BiPlainly PROP} p P Q1 Q2 :
-  IntoAnd p P Q1 Q2 → IntoAnd p (■ P) (■ Q1) (■ Q2).
-Proof.
-  rewrite /IntoAnd /=. destruct p; simpl.
-  - rewrite -plainly_and -[(â–¡ â–  P)%I]intuitionistically_idemp intuitionistically_plainly =>->.
-    rewrite [(□ (_ ∧ _))%I]intuitionistically_elim //.
-  - intros ->. by rewrite plainly_and.
-Qed.
-
 (** IntoSep *)
 Global Instance into_sep_later P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (▷ P) (▷ Q1) (▷ Q2).
@@ -208,18 +123,6 @@ Proof.
   by rewrite -(False_elim Q1) -(False_elim Q2).
 Qed.
 
-Global Instance into_sep_plainly `{BiPlainly PROP, BiPositive PROP} P Q1 Q2 :
-  IntoSep P Q1 Q2 → IntoSep (■ P) (■ Q1) (■ Q2).
-Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
-
-Global Instance into_sep_plainly_affine `{BiPlainly PROP} P Q1 Q2 :
-  IntoSep P Q1 Q2 →
-  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Absorbing Q1) (Affine Q2) →
-  IntoSep (â–  P) (â–  Q1) (â–  Q2).
-Proof.
-  rewrite /IntoSep /= => -> ??. by rewrite sep_and plainly_and plainly_and_sep_l_1.
-Qed.
-
 (** FromOr *)
 Global Instance from_or_later P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
@@ -231,17 +134,6 @@ 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 `{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;
-                         [apply bi.or_intro_l|apply bi.or_intro_r].
-Qed.
-
-Global Instance from_or_plainly `{BiPlainly PROP} P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (■ P) (■ Q1) (■ Q2).
-Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed.
-
 (** IntoOr *)
 Global Instance into_or_later P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
@@ -253,10 +145,6 @@ Global Instance into_or_except_0 P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /IntoOr=>->. by rewrite except_0_or. Qed.
 
-Global Instance into_or_plainly `{BiPlainly PROP, BiPlainlyExist PROP} P Q1 Q2 :
-  IntoOr P Q1 Q2 → IntoOr (■ P) (■ Q1) (■ Q2).
-Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
-
 (** FromExist *)
 Global Instance from_exist_later {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (▷ P) (λ a, ▷ (Φ a))%I.
@@ -272,16 +160,6 @@ 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 `{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).
-Qed.
-
-Global Instance from_exist_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :
-  FromExist P Φ → FromExist (■ P) (λ a, ■ (Φ a))%I.
-Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
-
 (** IntoExist *)
 Global Instance into_exist_later {A} P (Φ : A → PROP) :
   IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
@@ -293,10 +171,6 @@ Global Instance into_exist_except_0 {A} P (Φ : A → PROP) :
   IntoExist P Φ → Inhabited A → IntoExist (◇ P) (λ a, ◇ (Φ a))%I.
 Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
 
-Global Instance into_exist_plainly `{BiPlainlyExist PROP} {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (■ P) (λ a, ■ (Φ a))%I.
-Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
-
 (** IntoForall *)
 Global Instance into_forall_later {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (▷ P) (λ a, ▷ (Φ a))%I.
@@ -310,10 +184,6 @@ Global Instance into_forall_except_0 {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (◇ P) (λ a, ◇ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
 
-Global Instance into_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :
-  IntoForall P Φ → IntoForall (■ P) (λ a, ■ (Φ a))%I.
-Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
-
 (** FromForall *)
 Global Instance from_forall_later {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (▷ P)%I (λ a, ▷ (Φ a))%I.
@@ -327,44 +197,11 @@ Global Instance from_forall_except_0 {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (◇ P)%I (λ a, ◇ (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed.
 
-Global Instance from_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall (■ P)%I (λ a, ■ (Φ a))%I.
-Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
-
-Global Instance from_forall_fupd `{BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) :
-  (* Some cases in which [E2 ⊆ E1] holds *)
-  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
-  FromForall P Φ → (∀ x, Plain (Φ x)) →
-  FromForall (|={E1,E2}=> P)%I (λ a, |={E1,E2}=> (Φ a))%I.
-Proof.
-  rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite fupd_plain_forall; set_solver.
-Qed.
-
-Global Instance from_forall_step_fupd `{BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) :
-  (* Some cases in which [E2 ⊆ E1] holds *)
-  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
-  FromForall P Φ → (∀ x, Plain (Φ x)) →
-  FromForall (|={E1,E2}▷=> P)%I (λ a, |={E1,E2}▷=> (Φ a))%I.
-Proof.
-  rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
-Qed.
-
 (** IsExcept0 *)
 Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P).
 Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
 Global Instance is_except_0_later P : IsExcept0 (â–· P).
 Proof. by rewrite /IsExcept0 except_0_later. Qed.
-Global Instance is_except_0_embed `{BiEmbedLater PROP PROP'} P :
-  IsExcept0 P → IsExcept0 ⎡P⎤.
-Proof. by rewrite /IsExcept0 -embed_except_0=>->. Qed.
-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 `{BiFUpd PROP} E1 E2 P :
-  IsExcept0 (|={E1,E2}=> P).
-Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
 
 (** FromModal *)
 Global Instance from_modal_later P :
@@ -373,62 +210,9 @@ Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_laterN n P :
   FromModal (modality_laterN n) (â–·^n P) (â–·^n P) P.
 Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_Next `{!BiInternalEq PROP} {A : ofeT} (x y : A) :
-  FromModal (PROP1:=PROP) (PROP2:=PROP) (modality_laterN 1)
-    (▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
-Proof. by rewrite /FromModal /= later_equivI. 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_fupd E P `{BiFUpd PROP} :
-  FromModal modality_id (|={E}=> P) (|={E}=> P) P.
-Proof. by rewrite /FromModal /= -fupd_intro. Qed.
-
-Global Instance from_modal_later_embed `{BiEmbedLater PROP PROP'} `(sel : A) n P Q :
-  FromModal (modality_laterN n) sel P Q →
-  FromModal (modality_laterN n) sel ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_laterN. Qed.
-
-Global Instance from_modal_plainly `{BiPlainly PROP} P :
-  FromModal modality_plainly (â–  P) (â–  P) P | 2.
-Proof. by rewrite /FromModal. Qed.
-
-Global Instance from_modal_plainly_embed `{!BiPlainly PROP, !BiPlainly PROP',
-    !BiEmbed PROP PROP', !BiEmbedPlainly PROP PROP'} `(sel : A) P Q :
-  FromModal modality_plainly sel P Q →
-  FromModal (PROP2:=PROP') modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
-
-(** IntoInternalEq *)
-Section internal_eq.
-  Context `{!BiInternalEq PROP}.
-
-  Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
-    @IntoInternalEq PROP _ A (x ≡ y) x y.
-  Proof. by rewrite /IntoInternalEq. Qed.
-  Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
-    IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
-  Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
-  Global Instance into_internal_eq_intuitionistically {A : ofeT} (x y : A) P :
-    IntoInternalEq P x y → IntoInternalEq (□ P) x y.
-  Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.
-  Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
-    IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
-  Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
-  Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofeT} (x y : A) P :
-    IntoInternalEq P x y → IntoInternalEq (■ P) x y.
-  Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
-  Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
-    IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
-  Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
-  Global Instance into_internal_eq_embed
-       `{!BiInternalEq PROP', BiEmbedInternalEq PROP PROP'}
-       {A : ofeT} (x y : A) (P : PROP) :
-    IntoInternalEq P x y → IntoInternalEq (⎡P⎤ : PROP')%I x y.
-  Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
-End internal_eq.
-
 (** IntoExcept0 *)
 Global Instance into_except_0_except_0 P : IntoExcept0 (â—‡ P) P.
 Proof. by rewrite /IntoExcept0. Qed.
@@ -446,15 +230,9 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_intuitionistically_2. Qed.
 Global Instance into_except_0_absorbingly P Q :
   IntoExcept0 P Q → IntoExcept0 (<absorb> P) (<absorb> Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_absorbingly. Qed.
-Global Instance into_except_0_plainly `{BiPlainly PROP, BiPlainlyExist PROP} P Q :
-  IntoExcept0 P Q → IntoExcept0 (■ P) (■ Q).
-Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
 Global Instance into_except_0_persistently P Q :
   IntoExcept0 P Q → IntoExcept0 (<pers> P) (<pers> Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
-Global Instance into_except_0_embed `{BiEmbedLater PROP PROP'} P Q :
-  IntoExcept0 P Q → IntoExcept0 ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /IntoExcept0=> ->. by rewrite embed_except_0. Qed.
 
 (** ElimModal *)
 Global Instance elim_modal_timeless p P Q :
@@ -464,42 +242,8 @@ Proof.
   by rewrite except_0_intuitionistically_if_2 -except_0_sep wand_elim_r.
 Qed.
 
-Global Instance elim_modal_bupd_plain_goal `{BiBUpdPlainly 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_plain.
-Qed.
-Global Instance elim_modal_bupd_plain `{BiBUpdPlainly PROP} p P Q :
-  Plain P → ElimModal True p p (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
-Global Instance elim_modal_bupd_fupd `{BiBUpdFUpd PROP} p E1 E2 P Q :
-  ElimModal True p false (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
-Proof.
-  by rewrite /ElimModal intuitionistically_if_elim
-    (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
-Qed.
-
-Global Instance elim_modal_fupd_fupd `{BiFUpd PROP} p E1 E2 E3 P Q :
-  ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
-Proof.
-  by rewrite /ElimModal intuitionistically_if_elim
-    fupd_frame_r wand_elim_r fupd_trans.
-Qed.
-
-Global Instance elim_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
-    p p' φ E1 E2 E3 (P P' : PROP') (Q Q' : PROP) :
-  ElimModal φ p p' P P' (|={E1,E3}=> ⎡Q⎤)%I (|={E2,E3}=> ⎡Q'⎤)%I →
-  ElimModal φ p p' P P' ⎡|={E1,E3}=> Q⎤ ⎡|={E2,E3}=> Q'⎤.
-Proof. by rewrite /ElimModal !embed_fupd. Qed.
-Global Instance elim_modal_embed_fupd_hyp `{BiEmbedFUpd PROP PROP'}
-    p p' φ E1 E2 (P : PROP) (P' Q Q' : PROP') :
-  ElimModal φ p p' (|={E1,E2}=> ⎡P⎤)%I P' Q Q' →
-  ElimModal φ p p' ⎡|={E1,E2}=> P⎤ P' Q Q'.
-Proof. by rewrite /ElimModal embed_fupd. Qed.
-
 (** AddModal *)
-(* High priority to add a â–· rather than a â—‡ when P is timeless. *)
+(* High priority to add a [â–·] rather than a [â—‡] when [P] is timeless. *)
 Global Instance add_modal_later_except_0 P Q :
   Timeless P → AddModal (▷ P) P (◇ Q) | 0.
 Proof.
@@ -523,28 +267,6 @@ Proof.
   by rewrite -except_0_sep wand_elim_r except_0_later.
 Qed.
 
-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.
-
-Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
-       E1 E2 (P P' : PROP') (Q : PROP) :
-  AddModal P P' (|={E1,E2}=> ⎡Q⎤)%I → AddModal P P' ⎡|={E1,E2}=> Q⎤.
-Proof. by rewrite /AddModal !embed_fupd. Qed.
-
-(** ElimAcc *)
-Global Instance elim_acc_fupd `{BiFUpd PROP} {X} E1 E2 E α β mγ Q :
-  (* FIXME: Why %I? ElimAcc sets the right scopes! *)
-  ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β mγ
-          (|={E1,E}=> Q)
-          (λ x, |={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q))%I.
-Proof.
-  rewrite /ElimAcc.
-  iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
-  iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
-  iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
-Qed.
-
 (** IntoAcc *)
 (* TODO: We could have instances from "unfolded" accessors with or without
    the first binder. *)
@@ -577,15 +299,6 @@ Proof.
   move=> Hn [_ ->|->] <-; by rewrite -!laterN_plus -Hn Nat.add_comm.
 Qed.
 
-Global Instance into_laterN_Next `{!BiInternalEq PROP}
-    {A : ofeT} only_head n n' (x y : A) :
-  NatCancel n 1 n' 0 →
-  IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
-Proof.
-  rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel Nat.add_0_r.
-  move=> <-. rewrite later_equivI. by rewrite Nat.add_comm /= -laterN_intro.
-Qed.
-
 Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
   IntoLaterN false n P1 Q1 → MaybeIntoLaterN false n P2 Q2 →
   IntoLaterN false n (P1 ∧ P2) (Q1 ∧ Q2) | 10.
@@ -625,15 +338,9 @@ Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_intuitionist
 Global Instance into_later_absorbingly n P Q :
   IntoLaterN false n P Q → IntoLaterN false n (<absorb> P) (<absorb> Q).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
-Global Instance into_later_plainly `{BiPlainly PROP} n P Q :
-  IntoLaterN false n P Q → IntoLaterN false n (■ P) (■ Q).
-Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
 Global Instance into_later_persistently n P Q :
   IntoLaterN false n P Q → IntoLaterN false n (<pers> P) (<pers> Q).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
-Global Instance into_later_embed`{BiEmbedLater PROP PROP'} n P Q :
-  IntoLaterN false n P Q → IntoLaterN false n ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite embed_laterN. Qed.
 
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
   IntoLaterN false n P1 Q1 → MaybeIntoLaterN false n P2 Q2 →
@@ -693,4 +400,4 @@ Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opMS_commute. by apply big_sepMS_mono.
 Qed.
-End sbi_instances.
+End class_instances_later.
diff --git a/theories/proofmode/class_instances_plainly.v b/theories/proofmode/class_instances_plainly.v
new file mode 100644
index 0000000000000000000000000000000000000000..0559fc027096340b00c6837d18f2bfb4f9a1dc86
--- /dev/null
+++ b/theories/proofmode/class_instances_plainly.v
@@ -0,0 +1,101 @@
+From iris.bi Require Import bi.
+From iris.proofmode Require Import modality_instances classes.
+Set Default Proof Using "Type".
+Import bi.
+
+Section class_instances_plainly.
+Context `{!BiPlainly PROP}.
+Implicit Types P Q R : PROP.
+
+Global Instance from_assumption_plainly_l_true P Q :
+  FromAssumption true P Q → KnownLFromAssumption true (■ P) Q.
+Proof.
+  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
+  rewrite intuitionistically_plainly_elim //.
+Qed.
+Global Instance from_assumption_plainly_l_false `{BiAffine PROP} P Q :
+  FromAssumption true P Q → KnownLFromAssumption false (■ P) Q.
+Proof.
+  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
+  rewrite plainly_elim_persistently intuitionistically_into_persistently //.
+Qed.
+
+Global Instance from_pure_plainly P φ :
+  FromPure false P φ → FromPure false (■ P) φ.
+Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
+
+Global Instance into_pure_plainly P φ :
+  IntoPure P φ → IntoPure (■ P) φ.
+Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
+
+Global Instance into_wand_plainly_true q R P Q :
+  IntoWand true q R P Q → IntoWand true q (■ R) P Q.
+Proof. rewrite /IntoWand /= intuitionistically_plainly_elim //. Qed.
+Global Instance into_wand_plainly_false q R P Q :
+  Absorbing R → IntoWand false q R P Q → IntoWand false q (■ R) P Q.
+Proof. intros ?. by rewrite /IntoWand plainly_elim. Qed.
+
+Global Instance from_and_plainly P Q1 Q2 :
+  FromAnd P Q1 Q2 → FromAnd (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite plainly_and. Qed.
+
+Global Instance from_sep_plainly P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /FromSep=> <-. by rewrite plainly_sep_2. Qed.
+
+Global Instance into_and_plainly p P Q1 Q2 :
+  IntoAnd p P Q1 Q2 → IntoAnd p (■ P) (■ Q1) (■ Q2).
+Proof.
+  rewrite /IntoAnd /=. destruct p; simpl.
+  - rewrite -plainly_and -[(â–¡ â–  P)%I]intuitionistically_idemp intuitionistically_plainly =>->.
+    rewrite [(□ (_ ∧ _))%I]intuitionistically_elim //.
+  - intros ->. by rewrite plainly_and.
+Qed.
+
+Global Instance into_sep_plainly `{!BiPositive PROP} P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
+Global Instance into_sep_plainly_affine P Q1 Q2 :
+  IntoSep P Q1 Q2 →
+  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Absorbing Q1) (Affine Q2) →
+  IntoSep (â–  P) (â–  Q1) (â–  Q2).
+Proof.
+  rewrite /IntoSep /= => -> ??. by rewrite sep_and plainly_and plainly_and_sep_l_1.
+Qed.
+
+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 :
+  IntoOr P Q1 Q2 → IntoOr (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
+
+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) :
+  IntoExist P Φ → IntoExist (■ P) (λ a, ■ (Φ a))%I.
+Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
+
+Global Instance into_forall_plainly {A} P (Φ : A → PROP) :
+  IntoForall P Φ → IntoForall (■ P) (λ a, ■ (Φ a))%I.
+Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
+
+Global Instance from_forall_plainly {A} P (Φ : A → PROP) :
+  FromForall P Φ → FromForall (■ P)%I (λ a, ■ (Φ a))%I.
+Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
+
+Global Instance from_modal_plainly P :
+  FromModal modality_plainly (â–  P) (â–  P) P | 2.
+Proof. by rewrite /FromModal. Qed.
+
+Global Instance into_except_0_plainly `{!BiPlainlyExist PROP} P Q :
+  IntoExcept0 P Q → IntoExcept0 (■ P) (■ Q).
+Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
+
+Global Instance into_later_plainly n P Q :
+  IntoLaterN false n P Q → IntoLaterN false n (■ P) (■ Q).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
+End class_instances_plainly.
diff --git a/theories/proofmode/class_instances_updates.v b/theories/proofmode/class_instances_updates.v
new file mode 100644
index 0000000000000000000000000000000000000000..3d9d0bf7d37fd6afc312597e60fba6d3dfe294ab
--- /dev/null
+++ b/theories/proofmode/class_instances_updates.v
@@ -0,0 +1,182 @@
+From stdpp Require Import nat_cancel.
+From iris.bi Require Import bi.
+From iris.proofmode Require Import modality_instances classes.
+From iris.proofmode Require Import ltac_tactics class_instances.
+Set Default Proof Using "Type".
+Import bi.
+
+Section class_instances_updates.
+Context {PROP : bi}.
+Implicit Types P Q R : PROP.
+
+Global Instance from_assumption_bupd `{!BiBUpd PROP} p P Q :
+  FromAssumption p P Q → KnownRFromAssumption p P (|==> Q).
+Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_intro. Qed.
+Global Instance from_assumption_fupd
+    `{!BiBUpd PROP, !BiFUpd PROP, !BiBUpdFUpd PROP} E p P Q :
+  FromAssumption p P (|==> Q) → KnownRFromAssumption p P (|={E}=> Q)%I.
+Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_fupd. Qed.
+
+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 `{!BiFUpd PROP} a E P φ :
+  FromPure a P φ → FromPure a (|={E}=> P) φ.
+Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
+
+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 !intuitionistically_if_elim HR.
+  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
+Qed.
+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 !intuitionistically_if_elim HR.
+  apply wand_intro_l. by rewrite fupd_sep wand_elim_r.
+Qed.
+
+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 intuitionistically_if_elim HR.
+  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
+Qed.
+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 intuitionistically_if_elim HR.
+  apply wand_intro_l. by rewrite fupd_frame_l wand_elim_r.
+Qed.
+
+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 intuitionistically_if_elim bupd_wand_r.
+Qed.
+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 /= => ->.
+  apply wand_intro_l. by rewrite intuitionistically_if_elim fupd_wand_r.
+Qed.
+
+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 `{!BiFUpd PROP} 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_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 `{!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;
+                         [apply bi.or_intro_l|apply bi.or_intro_r].
+Qed.
+
+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 `{!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).
+Qed.
+
+Global Instance from_forall_fupd
+    `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) :
+  (* Some cases in which [E2 ⊆ E1] holds *)
+  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
+  FromForall P Φ → (∀ x, Plain (Φ x)) →
+  FromForall (|={E1,E2}=> P)%I (λ a, |={E1,E2}=> (Φ a))%I.
+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) :
+  (* Some cases in which [E2 ⊆ E1] holds *)
+  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
+  FromForall P Φ → (∀ x, Plain (Φ x)) →
+  FromForall (|={E1,E2}▷=> P)%I (λ a, |={E1,E2}▷=> (Φ a))%I.
+Proof.
+  rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
+Qed.
+
+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 `{!BiFUpd PROP} E1 E2 P :
+  IsExcept0 (|={E1,E2}=> P).
+Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
+
+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 `{!BiFUpd PROP} :
+  FromModal modality_id (|={E}=> P) (|={E}=> P) P.
+Proof. by rewrite /FromModal /= -fupd_intro. Qed.
+
+Global Instance elim_modal_bupd `{!BiBUpd PROP} p P Q :
+  ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
+Proof.
+  by rewrite /ElimModal
+    intuitionistically_if_elim bupd_frame_r wand_elim_r bupd_trans.
+Qed.
+
+Global Instance elim_modal_bupd_plain_goal
+    `{!BiBUpd PROP, !BiPlainly PROP, !BiBUpdPlainly 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_plain.
+Qed.
+Global Instance elim_modal_bupd_plain
+    `{!BiBUpd PROP, !BiPlainly PROP, !BiBUpdPlainly PROP} p P Q :
+  Plain P → ElimModal True p p (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
+Global Instance elim_modal_bupd_fupd
+    `{!BiBUpd PROP, !BiFUpd PROP, !BiBUpdFUpd PROP} p E1 E2 P Q :
+  ElimModal True p false (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
+Proof.
+  by rewrite /ElimModal intuitionistically_if_elim
+    (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
+Qed.
+Global Instance elim_modal_fupd_fupd `{!BiFUpd PROP} p E1 E2 E3 P Q :
+  ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+Proof.
+  by rewrite /ElimModal intuitionistically_if_elim
+    fupd_frame_r wand_elim_r fupd_trans.
+Qed.
+
+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 `{!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.
+
+Global Instance elim_acc_fupd `{!BiFUpd PROP} {X} E1 E2 E α β mγ Q :
+  ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β mγ
+          (|={E1,E}=> Q)
+          (λ x, |={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q))%I.
+Proof.
+  rewrite /ElimAcc.
+  iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+  iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
+  iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
+Qed.
+End class_instances_updates.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 5159c0a588fb4c3cc6b1f517bd708063a669345c..cc180547136fb42d0114b3294f8c825e666eeb63 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -8,7 +8,7 @@ Import env_notations.
 Local Open Scope lazy_bool_scope.
 
 (* Coq versions of the tactics *)
-Section bi_tactics.
+Section tactics.
 Context {PROP : bi}.
 Implicit Types Γ : env PROP.
 Implicit Types Δ : envs PROP.
@@ -791,8 +791,68 @@ Proof.
   - setoid_rewrite <-(right_id emp%I _ (Pout _)). auto.
 Qed.
 
-End bi_tactics.
+(** * Rewriting *)
+Lemma tac_rewrite `{!BiInternalEq PROP} Δ i p Pxy d Q :
+  envs_lookup i Δ = Some (p, Pxy) →
+  ∀ {A : ofeT} (x y : A) (Φ : A → PROP),
+    IntoInternalEq Pxy x y →
+    (Q ⊣⊢ Φ (if d is Left then y else x)) →
+    NonExpansive Φ →
+    envs_entails Δ (Φ (if d is Left then x else y)) → envs_entails Δ Q.
+Proof.
+  intros ? A x y ? HPxy -> ?. rewrite envs_entails_eq.
+  apply internal_eq_rewrite'; auto. rewrite {1}envs_lookup_sound //.
+  rewrite (into_internal_eq Pxy x y) intuitionistically_if_elim sep_elim_l.
+  destruct d; auto using internal_eq_sym.
+Qed.
 
+Lemma tac_rewrite_in `{!BiInternalEq PROP} Δ i p Pxy j q P d Q :
+  envs_lookup i Δ = Some (p, Pxy) →
+  envs_lookup j Δ = Some (q, P) →
+  ∀ {A : ofeT} (x y : A) (Φ : A → PROP),
+    IntoInternalEq Pxy x y →
+    (P ⊣⊢ Φ (if d is Left then y else x)) →
+    NonExpansive Φ →
+    match envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ with
+    | None => False
+    | Some Δ' => envs_entails Δ' Q
+    end →
+    envs_entails Δ Q.
+Proof.
+  rewrite envs_entails_eq /IntoInternalEq => ?? A x y Φ HPxy HP ? Hentails.
+  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done. rewrite -Hentails.
+  rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
+  rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
+  rewrite HP HPxy (intuitionistically_if_elim _ (_ ≡ _)%I) sep_elim_l.
+  rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
+  rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
+  - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
+  - rewrite internal_eq_sym.
+    eapply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
+Qed.
+
+(** * Löb *)
+Lemma tac_löb Δ i Q :
+  BiLöb PROP →
+  env_spatial_is_nil Δ = true →
+  match envs_app true (Esnoc Enil i (▷ Q)%I) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
+Proof.
+  destruct (envs_app _ _ _) eqn:?; last done.
+  rewrite envs_entails_eq => ?? HQ.
+  rewrite (env_spatial_is_nil_intuitionistically Δ) //.
+  rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
+  rewrite -(löb (<pers> Q)%I) later_persistently. apply impl_intro_l.
+  rewrite envs_app_singleton_sound //; simpl; rewrite HQ.
+  rewrite persistently_and_intuitionistically_sep_l -{1}intuitionistically_idemp.
+  rewrite intuitionistically_sep_2 wand_elim_r intuitionistically_into_persistently_1 //.
+Qed.
+End tactics.
+
+(** * Introduction of modalities *)
 (** The following _private_ classes are used internally by [tac_modal_intro] /
 [iModIntro] to transform the proofmode environments when introducing a modality.
 
@@ -1015,56 +1075,9 @@ Section tac_modal_intro.
   Qed.
 End tac_modal_intro.
 
-Section sbi_tactics.
-Context {PROP : bi}.
-Implicit Types Γ : env PROP.
-Implicit Types Δ : envs PROP.
-Implicit Types P Q : PROP.
-
-(** * Rewriting *)
-Lemma tac_rewrite `{!BiInternalEq PROP} Δ i p Pxy d Q :
-  envs_lookup i Δ = Some (p, Pxy) →
-  ∀ {A : ofeT} (x y : A) (Φ : A → PROP),
-    IntoInternalEq Pxy x y →
-    (Q ⊣⊢ Φ (if d is Left then y else x)) →
-    NonExpansive Φ →
-    envs_entails Δ (Φ (if d is Left then x else y)) → envs_entails Δ Q.
-Proof.
-  intros ? A x y ? HPxy -> ?. rewrite envs_entails_eq.
-  apply internal_eq_rewrite'; auto. rewrite {1}envs_lookup_sound //.
-  rewrite (into_internal_eq Pxy x y) intuitionistically_if_elim sep_elim_l.
-  destruct d; auto using internal_eq_sym.
-Qed.
-
-Lemma tac_rewrite_in `{!BiInternalEq PROP} Δ i p Pxy j q P d Q :
-  envs_lookup i Δ = Some (p, Pxy) →
-  envs_lookup j Δ = Some (q, P) →
-  ∀ {A : ofeT} (x y : A) (Φ : A → PROP),
-    IntoInternalEq Pxy x y →
-    (P ⊣⊢ Φ (if d is Left then y else x)) →
-    NonExpansive Φ →
-    match envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ with
-    | None => False
-    | Some Δ' => envs_entails Δ' Q
-    end →
-    envs_entails Δ Q.
-Proof.
-  rewrite envs_entails_eq /IntoInternalEq => ?? A x y Φ HPxy HP ? Hentails.
-  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done. rewrite -Hentails.
-  rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
-  rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
-  rewrite HP HPxy (intuitionistically_if_elim _ (_ ≡ _)%I) sep_elim_l.
-  rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
-  rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
-  - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
-  - rewrite internal_eq_sym.
-    eapply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
-Qed.
-
-(** * Later *)
 (** The class [MaybeIntoLaterNEnvs] is used by tactics that need to introduce
-laters, e.g. the symbolic execution tactics. *)
-Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
+laters, e.g., the symbolic execution tactics. *)
+Class MaybeIntoLaterNEnvs {PROP : bi} (n : nat) (Δ1 Δ2 : envs PROP) := {
   into_later_intuitionistic :
     TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n)
       (env_intuitionistic Δ1) (env_intuitionistic Δ2);
@@ -1073,13 +1086,13 @@ Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
       (MaybeIntoLaterN false n) (env_spatial Δ1) (env_spatial Δ2) false
 }.
 
-Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 m :
+Global Instance into_laterN_envs {PROP : bi} n (Γp1 Γp2 Γs1 Γs2 : env PROP) m :
   TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n) Γp1 Γp2 →
   TransformSpatialEnv (modality_laterN n) (MaybeIntoLaterN false n) Γs1 Γs2 false →
   MaybeIntoLaterNEnvs n (Envs Γp1 Γs1 m) (Envs Γp2 Γs2 m).
 Proof. by split. Qed.
 
-Lemma into_laterN_env_sound n Δ1 Δ2 :
+Lemma into_laterN_env_sound {PROP : bi} n (Δ1 Δ2 : envs PROP) :
   MaybeIntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2).
 Proof.
   intros [[Hp ??] [Hs ??]]; rewrite !of_envs_eq /= !laterN_and !laterN_sep.
@@ -1090,23 +1103,3 @@ Proof.
     + intros P Q. by rewrite laterN_and.
   - by rewrite Hs //= right_id.
 Qed.
-
-Lemma tac_löb Δ i Q :
-  BiLöb PROP →
-  env_spatial_is_nil Δ = true →
-  match envs_app true (Esnoc Enil i (▷ Q)%I) Δ with
-  | None => False
-  | Some Δ' => envs_entails Δ' Q
-  end →
-  envs_entails Δ Q.
-Proof.
-  destruct (envs_app _ _ _) eqn:?; last done.
-  rewrite envs_entails_eq => ?? HQ.
-  rewrite (env_spatial_is_nil_intuitionistically Δ) //.
-  rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
-  rewrite -(löb (<pers> Q)%I) later_persistently. apply impl_intro_l.
-  rewrite envs_app_singleton_sound //; simpl; rewrite HQ.
-  rewrite persistently_and_intuitionistically_sep_l -{1}intuitionistically_idemp.
-  rewrite intuitionistically_sep_2 wand_elim_r intuitionistically_into_persistently_1 //.
-Qed.
-End sbi_tactics.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 22ece1b62360aa2cc02b921d35300e691ef53bdf..636885cb87bda5d3e9d7a1044becdd6924e41037 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1,4 +1,7 @@
 From iris.proofmode Require Export ltac_tactics.
 (* This [Require Import] is not a no-op: it exports typeclass instances from
 these files. *)
-From iris.proofmode Require Import class_instances_bi class_instances_sbi frame_instances modality_instances.
+From iris.proofmode Require Import class_instances class_instances_later
+  class_instances_updates class_instances_embedding
+  class_instances_plainly class_instances_internal_eq.
+From iris.proofmode Require Import frame_instances modality_instances.