From cd5f38bf7ba5ef3010a33a5a72eacdeabd69cabb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 May 2020 14:08:15 +0200
Subject: [PATCH] Fine-grained split of `class_instances` based on the
 structure of the `bi` folder.

---
 _CoqProject                                   |   8 +-
 theories/bi/lib/fractional.v                  |   2 +-
 ...class_instances_bi.v => class_instances.v} | 216 +------------
 .../proofmode/class_instances_embedding.v     | 211 ++++++++++++
 .../proofmode/class_instances_internal_eq.v   |  50 +++
 ...nstances_sbi.v => class_instances_later.v} | 303 +-----------------
 theories/proofmode/class_instances_plainly.v  | 101 ++++++
 theories/proofmode/class_instances_updates.v  | 182 +++++++++++
 theories/proofmode/tactics.v                  |   5 +-
 9 files changed, 567 insertions(+), 511 deletions(-)
 rename theories/proofmode/{class_instances_bi.v => class_instances.v} (81%)
 create mode 100644 theories/proofmode/class_instances_embedding.v
 create mode 100644 theories/proofmode/class_instances_internal_eq.v
 rename theories/proofmode/{class_instances_sbi.v => class_instances_later.v} (56%)
 create mode 100644 theories/proofmode/class_instances_plainly.v
 create mode 100644 theories/proofmode/class_instances_updates.v

diff --git a/_CoqProject b/_CoqProject
index fa1ddef99..894e70041 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -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/lib/fractional.v b/theories/bi/lib/fractional.v
index ec7b4666a..51253b19f 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/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 30f3d1879..e3e88c265 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 000000000..6e964003e
--- /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 000000000..c33c76c79
--- /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 3e40fc8dc..7b2271f5b 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 000000000..0559fc027
--- /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 000000000..3d9d0bf7d
--- /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/tactics.v b/theories/proofmode/tactics.v
index 22ece1b62..636885cb8 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.
-- 
GitLab