diff --git a/_CoqProject b/_CoqProject
index ee5700f0322e82ceede757e3304858662751f3c6..86c783a15c58f8a092d97d4f40458bcafa12f1fe 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -103,6 +103,7 @@ theories/proofmode/notation.v
 theories/proofmode/classes.v
 theories/proofmode/class_instances_bi.v
 theories/proofmode/class_instances_sbi.v
+theories/proofmode/frame_instances.v
 theories/proofmode/monpred.v
 theories/proofmode/modalities.v
 theories/proofmode/modality_instances.v
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 720d877e8a58d998af94be46ac442247ff1da147..bbe5c72bc98d348bad32c868aa8d02450be5c7dd 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -811,262 +811,6 @@ Global Instance add_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
   AddModal P P' (|==> ⎡Q⎤)%I → AddModal P P' ⎡|==> Q⎤.
 Proof. by rewrite /AddModal !embed_bupd. Qed.
 
-(* Frame *)
-Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
-Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
-Global Instance frame_here p R : Frame p R R emp | 1.
-Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
-Global Instance frame_affinely_here_absorbing p R :
-  Absorbing R → Frame p (<affine> R) R True | 0.
-Proof.
-  intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
-  apply sep_elim_l, _.
-Qed.
-Global Instance frame_affinely_here p R : Frame p (<affine> R) R emp | 1.
-Proof.
-  intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
-  apply sep_elim_l, _.
-Qed.
-
-Global Instance frame_here_pure p φ Q : FromPure false Q φ → Frame p ⌜φ⌝ Q True.
-Proof.
-  rewrite /FromPure /Frame=> <-.
-  by rewrite intuitionistically_if_elim sep_elim_l.
-Qed.
-
-Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
-  KnownMakeEmbed ⌜φ⌝ ⌜φ⌝.
-Proof. apply embed_pure. Qed.
-Global Instance make_embed_emp `{BiEmbed PROP PROP'} :
-  KnownMakeEmbed emp emp.
-Proof. apply embed_emp. Qed.
-Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
-  MakeEmbed P ⎡P⎤ | 100.
-Proof. by rewrite /MakeEmbed. Qed.
-
-Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
-  Frame p R P Q → MakeEmbed Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
-Proof.
-  rewrite /Frame /MakeEmbed => <- <-.
-  rewrite embed_sep embed_intuitionistically_if => //.
-Qed.
-Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
-  Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' → Frame p ⌜φ⌝ ⎡P⎤ Q'.
-Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
-
-Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
-Proof. apply left_id, _. Qed.
-Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
-Proof. apply right_id, _. Qed.
-Global Instance make_sep_true_l P : Absorbing P → KnownLMakeSep True P P.
-Proof. intros. apply True_sep, _. Qed.
-Global Instance make_and_emp_l_absorbingly P : KnownLMakeSep True P (<absorb> P) | 10.
-Proof. intros. by rewrite /KnownLMakeSep /MakeSep. Qed.
-Global Instance make_sep_true_r P : Absorbing P → KnownRMakeSep P True P.
-Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed.
-Global Instance make_and_emp_r_absorbingly P : KnownRMakeSep P True (<absorb> P) | 10.
-Proof. intros. by rewrite /KnownRMakeSep /MakeSep comm. Qed.
-Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
-Proof. by rewrite /MakeSep. Qed.
-
-Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
-  Frame true R P1 Q1 → MaybeFrame true R P2 Q2 progress → MakeSep Q1 Q2 Q' →
-  Frame true R (P1 ∗ P2) Q' | 9.
-Proof.
-  rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
-  rewrite {1}(intuitionistically_sep_dup R). solve_sep_entails.
-Qed.
-Global Instance frame_sep_l R P1 P2 Q Q' :
-  Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
-Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
-Global Instance frame_sep_r p R P1 P2 Q Q' :
-  Frame p R P2 Q → MakeSep P1 Q Q' → Frame p R (P1 ∗ P2) Q' | 10.
-Proof.
-  rewrite /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc.
-Qed.
-
-Global Instance frame_big_sepL_cons {A} p (Φ : nat → A → PROP) R Q l x l' :
-  IsCons l x l' →
-  Frame p R (Φ 0 x ∗ [∗ list] k ↦ y ∈ l', Φ (S k) y) Q →
-  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
-Proof. rewrite /IsCons=>->. by rewrite /Frame big_sepL_cons. Qed.
-Global Instance frame_big_sepL_app {A} p (Φ : nat → A → PROP) R Q l l1 l2 :
-  IsApp l l1 l2 →
-  Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
-           [∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
-  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
-Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
-
-Global Instance make_and_true_l P : KnownLMakeAnd True P P.
-Proof. apply left_id, _. Qed.
-Global Instance make_and_true_r P : KnownRMakeAnd P True P.
-Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
-Global Instance make_and_emp_l P : Affine P → KnownLMakeAnd emp P P.
-Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd emp_and. Qed.
-Global Instance make_and_emp_l_affinely P : KnownLMakeAnd emp P (<affine> P) | 10.
-Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd. Qed.
-Global Instance make_and_emp_r P : Affine P → KnownRMakeAnd P emp P.
-Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed.
-Global Instance make_and_emp_r_affinely P : KnownRMakeAnd P emp (<affine> P) | 10.
-Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd comm. Qed.
-Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
-Proof. by rewrite /MakeAnd. Qed.
-
-Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
-  MaybeFrame p R P1 Q1 progress1 →
-  MaybeFrame p R P2 Q2 progress2 →
-  TCEq (progress1 || progress2) true →
-  MakeAnd Q1 Q2 Q' →
-  Frame p R (P1 ∧ P2) Q' | 9.
-Proof.
-  rewrite /MaybeFrame /Frame /MakeAnd => <- <- _ <-. apply and_intro;
-  [rewrite and_elim_l|rewrite and_elim_r]; done.
-Qed.
-
-Global Instance make_or_true_l P : KnownLMakeOr True P True.
-Proof. apply left_absorb, _. Qed.
-Global Instance make_or_true_r P : KnownRMakeOr P True True.
-Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed.
-Global Instance make_or_emp_l P : Affine P → KnownLMakeOr emp P emp.
-Proof. intros. by rewrite /KnownLMakeOr /MakeOr emp_or. Qed.
-Global Instance make_or_emp_r P : Affine P → KnownRMakeOr P emp emp.
-Proof. intros. by rewrite /KnownRMakeOr /MakeOr or_emp. Qed.
-Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
-Proof. by rewrite /MakeOr. Qed.
-
-(* We could in principle write the instance [frame_or_spatial] by a bunch of
-instances, i.e. (omitting the parameter [p = false]):
-
-  Frame R P1 Q1 → Frame R P2 Q2 → Frame R (P1 ∨ P2) (Q1 ∨ Q2)
-  Frame R P1 True → Frame R (P1 ∨ P2) P2
-  Frame R P2 True → Frame R (P1 ∨ P2) P1
-
-The problem here is that Coq will try to infer [Frame R P1 ?] and [Frame R P2 ?]
-multiple times, whereas the current solution makes sure that said inference
-appears at most once.
-
-If Coq would memorize the results of type class resolution, the solution with
-multiple instances would be preferred (and more Prolog-like). *)
-Global Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
-  MaybeFrame false R P1 Q1 progress1 → MaybeFrame false R P2 Q2 progress2 →
-  TCOr (TCEq (progress1 && progress2) true) (TCOr
-    (TCAnd (TCEq progress1 true) (TCEq Q1 True%I))
-    (TCAnd (TCEq progress2 true) (TCEq Q2 True%I))) →
-  MakeOr Q1 Q2 Q →
-  Frame false R (P1 ∨ P2) Q | 9.
-Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
-
-Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
-  MaybeFrame true R P1 Q1 progress1 → MaybeFrame true R P2 Q2 progress2 →
-  TCEq (progress1 || progress2) true →
-  MakeOr Q1 Q2 Q → Frame true R (P1 ∨ P2) Q | 9.
-Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
-
-Global Instance frame_wand p R P1 P2 Q2 :
-  Frame p R P2 Q2 → Frame p R (P1 -∗ P2) (P1 -∗ Q2).
-Proof.
-  rewrite /Frame=> ?. apply wand_intro_l.
-  by rewrite assoc (comm _ P1) -assoc wand_elim_r.
-Qed.
-
-Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
-Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_emp. Qed.
-Global Instance make_affinely_affine P : Affine P → KnownMakeAffinely P P | 1.
-Proof. intros. by rewrite /KnownMakeAffinely /MakeAffinely affine_affinely. Qed.
-Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
-Proof. by rewrite /MakeAffinely. Qed.
-
-Global Instance frame_affinely R P Q Q' :
-  Frame true R P Q → MakeAffinely Q Q' → Frame true R (<affine> P) Q'.
-Proof.
-  rewrite /Frame /MakeAffinely=> <- <- /=.
-  rewrite -{1}(affine_affinely (â–¡ R)%I) affinely_sep_2 //.
-Qed.
-
-Global Instance make_intuitionistically_True :
-  @KnownMakeIntuitionistically PROP True emp | 0.
-Proof.
-  by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
-             intuitionistically_True_emp.
-Qed.
-Global Instance make_intuitionistically_intuitionistic P :
-  Affine P → Persistent P → KnownMakeIntuitionistically P P | 1.
-Proof.
-  intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically.
-  rewrite intuitionistic_intuitionistically //.
-Qed.
-Global Instance make_intuitionistically_default P :
-  MakeIntuitionistically P (â–¡ P) | 100.
-Proof. by rewrite /MakeIntuitionistically. Qed.
-
-Global Instance frame_intuitionistically R P Q Q' :
-  Frame true R P Q → MakeIntuitionistically Q Q' → Frame true R (□ P) Q'.
-Proof.
-  rewrite /Frame /MakeIntuitionistically=> <- <- /=.
-  rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
-Qed.
-
-Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
-Proof.
-  by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
-     -absorbingly_True_emp absorbingly_pure.
-Qed.
-(* Note: there is no point in having an instance `Absorbing P → MakeAbsorbingly P P`
-because framing will never turn a proposition that is not absorbing into
-something that is absorbing. *)
-Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
-Proof. by rewrite /MakeAbsorbingly. Qed.
-
-Global Instance frame_absorbingly p R P Q Q' :
-  Frame p R P Q → MakeAbsorbingly Q Q' → Frame p R (<absorb> P) Q'.
-Proof.
-  rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
-Qed.
-
-Global Instance make_persistently_true : @KnownMakePersistently PROP True True.
-Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.
-Global Instance make_persistently_emp : @KnownMakePersistently PROP emp True.
-Proof.
-  by rewrite /KnownMakePersistently /MakePersistently
-     -persistently_True_emp persistently_pure.
-Qed.
-Global Instance make_persistently_default P :
-  MakePersistently P (<pers> P) | 100.
-Proof. by rewrite /MakePersistently. Qed.
-
-Global Instance frame_persistently R P Q Q' :
-  Frame true R P Q → MakePersistently Q Q' → Frame true R (<pers> P) Q'.
-Proof.
-  rewrite /Frame /MakePersistently=> <- <- /=.
-  rewrite -persistently_and_intuitionistically_sep_l.
-  by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_affinely
-              persistently_idemp.
-Qed.
-
-Global Instance frame_exist {A} p R (Φ Ψ : A → PROP) :
-  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∃ x, Φ x) (∃ x, Ψ x).
-Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
-Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
-  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x).
-Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
-
-Global Instance frame_impl_persistent R P1 P2 Q2 :
-  Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2).
-Proof.
-  rewrite /Frame /= => ?. apply impl_intro_l.
-  by rewrite -persistently_and_intuitionistically_sep_l assoc (comm _ P1) -assoc impl_elim_r
-             persistently_and_intuitionistically_sep_l.
-Qed.
-Global Instance frame_impl R P1 P2 Q2 :
-  Persistent P1 → Absorbing P1 →
-  Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2).
-Proof.
-  rewrite /Frame /==> ???. apply impl_intro_l.
-  rewrite {1}(persistent P1) persistently_and_intuitionistically_sep_l assoc.
-  rewrite (comm _ (â–¡ P1)%I) -assoc -persistently_and_intuitionistically_sep_l.
-  rewrite persistently_elim impl_elim_r //.
-Qed.
-
 (* IntoEmbed *)
 Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
   IntoEmbed ⎡P⎤ P.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index c2001de076d9128213c0fd1a80cf861de9b72237..61a838d9cbfbc33669e8567336877e729cc0de38 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -1,6 +1,6 @@
 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import modality_instances classes class_instances_bi.
+From iris.proofmode Require Import modality_instances classes.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -544,55 +544,6 @@ Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
   AddModal P P' (|={E1,E2}=> ⎡Q⎤)%I → AddModal P P' ⎡|={E1,E2}=> Q⎤.
 Proof. by rewrite /AddModal !embed_fupd. Qed.
 
-(* Frame *)
-Global Instance frame_eq_embed `{SbiEmbed PROP PROP'} p P Q (Q' : PROP')
-       {A : ofeT} (a b : A) :
-  Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
-Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
-
-Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
-Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
-Global Instance make_laterN_0 P : MakeLaterN 0 P P | 0.
-Proof. by rewrite /MakeLaterN. Qed.
-Global Instance make_laterN_1 P : MakeLaterN 1 P (â–· P) | 2.
-Proof. by rewrite /MakeLaterN. Qed.
-Global Instance make_laterN_default P : MakeLaterN n P (â–·^n P) | 100.
-Proof. by rewrite /MakeLaterN. Qed.
-
-Global Instance frame_later p R R' P Q Q' :
-  NoBackTrack (MaybeIntoLaterN true 1 R' R) →
-  Frame p R P Q → MakeLaterN 1 Q Q' → Frame p R' (▷ P) Q'.
-Proof.
-  rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
-  by rewrite later_intuitionistically_if_2 later_sep.
-Qed.
-Global Instance frame_laterN p n R R' P Q Q' :
-  NoBackTrack (MaybeIntoLaterN true n R' R) →
-  Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
-Proof.
-  rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
-  by rewrite laterN_intuitionistically_if_2 laterN_sep.
-Qed.
-
-Global Instance frame_bupd `{BiBUpd PROP} p R P Q :
-  Frame p R P Q → Frame p R (|==> P) (|==> Q).
-Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
-Global Instance frame_fupd `{BiFUpd PROP} p E1 E2 R P Q :
-  Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
-Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
-
-Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
-Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.
-Global Instance make_except_0_default P : MakeExcept0 P (â—‡ P) | 100.
-Proof. by rewrite /MakeExcept0. Qed.
-
-Global Instance frame_except_0 p R P Q Q' :
-  Frame p R P Q → MakeExcept0 Q Q' → Frame p R (◇ P) Q'.
-Proof.
-  rewrite /Frame /MakeExcept0=><- <-.
-  by rewrite except_0_sep -(except_0_intro (â–¡?p R)%I).
-Qed.
-
 (* IntoLater *)
 Global Instance into_laterN_0 only_head P : IntoLaterN only_head 0 P P.
 Proof. by rewrite /IntoLaterN /MaybeIntoLaterN. Qed.
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
new file mode 100644
index 0000000000000000000000000000000000000000..c13a250337bda4d7fbe80daf291ab933aaa497a0
--- /dev/null
+++ b/theories/proofmode/frame_instances.v
@@ -0,0 +1,321 @@
+From stdpp Require Import nat_cancel.
+From iris.bi Require Import bi tactics.
+From iris.proofmode Require Import classes.
+Set Default Proof Using "Type".
+Import bi.
+
+(** This file defines the instances that make up the framing machinery. *)
+
+Section bi.
+Context {PROP : bi}.
+Implicit Types P Q R : PROP.
+(* Frame *)
+Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
+Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
+Global Instance frame_here p R : Frame p R R emp | 1.
+Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
+Global Instance frame_affinely_here_absorbing p R :
+  Absorbing R → Frame p (<affine> R) R True | 0.
+Proof.
+  intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
+  apply sep_elim_l, _.
+Qed.
+Global Instance frame_affinely_here p R : Frame p (<affine> R) R emp | 1.
+Proof.
+  intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
+  apply sep_elim_l, _.
+Qed.
+
+Global Instance frame_here_pure p φ Q : FromPure false Q φ → Frame p ⌜φ⌝ Q True.
+Proof.
+  rewrite /FromPure /Frame=> <-.
+  by rewrite intuitionistically_if_elim sep_elim_l.
+Qed.
+
+Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
+  KnownMakeEmbed ⌜φ⌝ ⌜φ⌝.
+Proof. apply embed_pure. Qed.
+Global Instance make_embed_emp `{BiEmbed PROP PROP'} :
+  KnownMakeEmbed emp emp.
+Proof. apply embed_emp. Qed.
+Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
+  MakeEmbed P ⎡P⎤ | 100.
+Proof. by rewrite /MakeEmbed. Qed.
+
+Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
+  Frame p R P Q → MakeEmbed Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
+Proof.
+  rewrite /Frame /MakeEmbed => <- <-.
+  rewrite embed_sep embed_intuitionistically_if => //.
+Qed.
+Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
+  Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' → Frame p ⌜φ⌝ ⎡P⎤ Q'.
+Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
+
+Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
+Proof. apply left_id, _. Qed.
+Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
+Proof. apply right_id, _. Qed.
+Global Instance make_sep_true_l P : Absorbing P → KnownLMakeSep True P P.
+Proof. intros. apply True_sep, _. Qed.
+Global Instance make_and_emp_l_absorbingly P : KnownLMakeSep True P (<absorb> P) | 10.
+Proof. intros. by rewrite /KnownLMakeSep /MakeSep. Qed.
+Global Instance make_sep_true_r P : Absorbing P → KnownRMakeSep P True P.
+Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed.
+Global Instance make_and_emp_r_absorbingly P : KnownRMakeSep P True (<absorb> P) | 10.
+Proof. intros. by rewrite /KnownRMakeSep /MakeSep comm. Qed.
+Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
+Proof. by rewrite /MakeSep. Qed.
+
+Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
+  Frame true R P1 Q1 → MaybeFrame true R P2 Q2 progress → MakeSep Q1 Q2 Q' →
+  Frame true R (P1 ∗ P2) Q' | 9.
+Proof.
+  rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
+  rewrite {1}(intuitionistically_sep_dup R). solve_sep_entails.
+Qed.
+Global Instance frame_sep_l R P1 P2 Q Q' :
+  Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
+Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
+Global Instance frame_sep_r p R P1 P2 Q Q' :
+  Frame p R P2 Q → MakeSep P1 Q Q' → Frame p R (P1 ∗ P2) Q' | 10.
+Proof.
+  rewrite /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc.
+Qed.
+
+Global Instance frame_big_sepL_cons {A} p (Φ : nat → A → PROP) R Q l x l' :
+  IsCons l x l' →
+  Frame p R (Φ 0 x ∗ [∗ list] k ↦ y ∈ l', Φ (S k) y) Q →
+  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
+Proof. rewrite /IsCons=>->. by rewrite /Frame big_sepL_cons. Qed.
+Global Instance frame_big_sepL_app {A} p (Φ : nat → A → PROP) R Q l l1 l2 :
+  IsApp l l1 l2 →
+  Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
+           [∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
+  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
+Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
+
+Global Instance make_and_true_l P : KnownLMakeAnd True P P.
+Proof. apply left_id, _. Qed.
+Global Instance make_and_true_r P : KnownRMakeAnd P True P.
+Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
+Global Instance make_and_emp_l P : Affine P → KnownLMakeAnd emp P P.
+Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd emp_and. Qed.
+Global Instance make_and_emp_l_affinely P : KnownLMakeAnd emp P (<affine> P) | 10.
+Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd. Qed.
+Global Instance make_and_emp_r P : Affine P → KnownRMakeAnd P emp P.
+Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed.
+Global Instance make_and_emp_r_affinely P : KnownRMakeAnd P emp (<affine> P) | 10.
+Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd comm. Qed.
+Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
+Proof. by rewrite /MakeAnd. Qed.
+
+Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
+  MaybeFrame p R P1 Q1 progress1 →
+  MaybeFrame p R P2 Q2 progress2 →
+  TCEq (progress1 || progress2) true →
+  MakeAnd Q1 Q2 Q' →
+  Frame p R (P1 ∧ P2) Q' | 9.
+Proof.
+  rewrite /MaybeFrame /Frame /MakeAnd => <- <- _ <-. apply and_intro;
+  [rewrite and_elim_l|rewrite and_elim_r]; done.
+Qed.
+
+Global Instance make_or_true_l P : KnownLMakeOr True P True.
+Proof. apply left_absorb, _. Qed.
+Global Instance make_or_true_r P : KnownRMakeOr P True True.
+Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed.
+Global Instance make_or_emp_l P : Affine P → KnownLMakeOr emp P emp.
+Proof. intros. by rewrite /KnownLMakeOr /MakeOr emp_or. Qed.
+Global Instance make_or_emp_r P : Affine P → KnownRMakeOr P emp emp.
+Proof. intros. by rewrite /KnownRMakeOr /MakeOr or_emp. Qed.
+Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
+Proof. by rewrite /MakeOr. Qed.
+
+(* We could in principle write the instance [frame_or_spatial] by a bunch of
+instances, i.e. (omitting the parameter [p = false]):
+
+  Frame R P1 Q1 → Frame R P2 Q2 → Frame R (P1 ∨ P2) (Q1 ∨ Q2)
+  Frame R P1 True → Frame R (P1 ∨ P2) P2
+  Frame R P2 True → Frame R (P1 ∨ P2) P1
+
+The problem here is that Coq will try to infer [Frame R P1 ?] and [Frame R P2 ?]
+multiple times, whereas the current solution makes sure that said inference
+appears at most once.
+
+If Coq would memorize the results of type class resolution, the solution with
+multiple instances would be preferred (and more Prolog-like). *)
+Global Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
+  MaybeFrame false R P1 Q1 progress1 → MaybeFrame false R P2 Q2 progress2 →
+  TCOr (TCEq (progress1 && progress2) true) (TCOr
+    (TCAnd (TCEq progress1 true) (TCEq Q1 True%I))
+    (TCAnd (TCEq progress2 true) (TCEq Q2 True%I))) →
+  MakeOr Q1 Q2 Q →
+  Frame false R (P1 ∨ P2) Q | 9.
+Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
+
+Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
+  MaybeFrame true R P1 Q1 progress1 → MaybeFrame true R P2 Q2 progress2 →
+  TCEq (progress1 || progress2) true →
+  MakeOr Q1 Q2 Q → Frame true R (P1 ∨ P2) Q | 9.
+Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
+
+Global Instance frame_wand p R P1 P2 Q2 :
+  Frame p R P2 Q2 → Frame p R (P1 -∗ P2) (P1 -∗ Q2).
+Proof.
+  rewrite /Frame=> ?. apply wand_intro_l.
+  by rewrite assoc (comm _ P1) -assoc wand_elim_r.
+Qed.
+
+Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
+Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_emp. Qed.
+Global Instance make_affinely_affine P : Affine P → KnownMakeAffinely P P | 1.
+Proof. intros. by rewrite /KnownMakeAffinely /MakeAffinely affine_affinely. Qed.
+Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
+Proof. by rewrite /MakeAffinely. Qed.
+
+Global Instance frame_affinely R P Q Q' :
+  Frame true R P Q → MakeAffinely Q Q' → Frame true R (<affine> P) Q'.
+Proof.
+  rewrite /Frame /MakeAffinely=> <- <- /=.
+  rewrite -{1}(affine_affinely (â–¡ R)%I) affinely_sep_2 //.
+Qed.
+
+Global Instance make_intuitionistically_True :
+  @KnownMakeIntuitionistically PROP True emp | 0.
+Proof.
+  by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
+             intuitionistically_True_emp.
+Qed.
+Global Instance make_intuitionistically_intuitionistic P :
+  Affine P → Persistent P → KnownMakeIntuitionistically P P | 1.
+Proof.
+  intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically.
+  rewrite intuitionistic_intuitionistically //.
+Qed.
+Global Instance make_intuitionistically_default P :
+  MakeIntuitionistically P (â–¡ P) | 100.
+Proof. by rewrite /MakeIntuitionistically. Qed.
+
+Global Instance frame_intuitionistically R P Q Q' :
+  Frame true R P Q → MakeIntuitionistically Q Q' → Frame true R (□ P) Q'.
+Proof.
+  rewrite /Frame /MakeIntuitionistically=> <- <- /=.
+  rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
+Qed.
+
+Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
+Proof.
+  by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
+     -absorbingly_True_emp absorbingly_pure.
+Qed.
+(* Note: there is no point in having an instance `Absorbing P → MakeAbsorbingly P P`
+because framing will never turn a proposition that is not absorbing into
+something that is absorbing. *)
+Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
+Proof. by rewrite /MakeAbsorbingly. Qed.
+
+Global Instance frame_absorbingly p R P Q Q' :
+  Frame p R P Q → MakeAbsorbingly Q Q' → Frame p R (<absorb> P) Q'.
+Proof.
+  rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
+Qed.
+
+Global Instance make_persistently_true : @KnownMakePersistently PROP True True.
+Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.
+Global Instance make_persistently_emp : @KnownMakePersistently PROP emp True.
+Proof.
+  by rewrite /KnownMakePersistently /MakePersistently
+     -persistently_True_emp persistently_pure.
+Qed.
+Global Instance make_persistently_default P :
+  MakePersistently P (<pers> P) | 100.
+Proof. by rewrite /MakePersistently. Qed.
+
+Global Instance frame_persistently R P Q Q' :
+  Frame true R P Q → MakePersistently Q Q' → Frame true R (<pers> P) Q'.
+Proof.
+  rewrite /Frame /MakePersistently=> <- <- /=.
+  rewrite -persistently_and_intuitionistically_sep_l.
+  by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_affinely
+              persistently_idemp.
+Qed.
+
+Global Instance frame_exist {A} p R (Φ Ψ : A → PROP) :
+  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∃ x, Φ x) (∃ x, Ψ x).
+Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
+Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
+  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x).
+Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
+
+Global Instance frame_impl_persistent R P1 P2 Q2 :
+  Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2).
+Proof.
+  rewrite /Frame /= => ?. apply impl_intro_l.
+  by rewrite -persistently_and_intuitionistically_sep_l assoc (comm _ P1) -assoc impl_elim_r
+             persistently_and_intuitionistically_sep_l.
+Qed.
+Global Instance frame_impl R P1 P2 Q2 :
+  Persistent P1 → Absorbing P1 →
+  Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2).
+Proof.
+  rewrite /Frame /==> ???. apply impl_intro_l.
+  rewrite {1}(persistent P1) persistently_and_intuitionistically_sep_l assoc.
+  rewrite (comm _ (â–¡ P1)%I) -assoc -persistently_and_intuitionistically_sep_l.
+  rewrite persistently_elim impl_elim_r //.
+Qed.
+End bi.
+
+(** SBI Framing *)
+Section sbi.
+Context {PROP : sbi}.
+Implicit Types P Q R : PROP.
+
+Global Instance frame_eq_embed `{SbiEmbed PROP PROP'} p P Q (Q' : PROP')
+       {A : ofeT} (a b : A) :
+  Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
+Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
+
+Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
+Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
+Global Instance make_laterN_0 P : MakeLaterN 0 P P | 0.
+Proof. by rewrite /MakeLaterN. Qed.
+Global Instance make_laterN_1 P : MakeLaterN 1 P (â–· P) | 2.
+Proof. by rewrite /MakeLaterN. Qed.
+Global Instance make_laterN_default P : MakeLaterN n P (â–·^n P) | 100.
+Proof. by rewrite /MakeLaterN. Qed.
+
+Global Instance frame_later p R R' P Q Q' :
+  NoBackTrack (MaybeIntoLaterN true 1 R' R) →
+  Frame p R P Q → MakeLaterN 1 Q Q' → Frame p R' (▷ P) Q'.
+Proof.
+  rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
+  by rewrite later_intuitionistically_if_2 later_sep.
+Qed.
+Global Instance frame_laterN p n R R' P Q Q' :
+  NoBackTrack (MaybeIntoLaterN true n R' R) →
+  Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
+Proof.
+  rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
+  by rewrite laterN_intuitionistically_if_2 laterN_sep.
+Qed.
+
+Global Instance frame_bupd `{BiBUpd PROP} p R P Q :
+  Frame p R P Q → Frame p R (|==> P) (|==> Q).
+Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
+Global Instance frame_fupd `{BiFUpd PROP} p E1 E2 R P Q :
+  Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
+
+Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
+Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.
+Global Instance make_except_0_default P : MakeExcept0 P (â—‡ P) | 100.
+Proof. by rewrite /MakeExcept0. Qed.
+
+Global Instance frame_except_0 p R P Q Q' :
+  Frame p R P Q → MakeExcept0 Q Q' → Frame p R (◇ P) Q'.
+Proof.
+  rewrite /Frame /MakeExcept0=><- <-.
+  by rewrite except_0_sep -(except_0_intro (â–¡?p R)%I).
+Qed.
+End sbi.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 908b01fdb355e54d0eb243bd1ff22f9793825c5c..e17593eb7c4ef17646f14830c9b0114479a82d7a 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -3,7 +3,8 @@ From iris.proofmode Require Import base intro_patterns spec_patterns sel_pattern
 From iris.bi Require Export bi.
 From stdpp Require Import namespaces.
 From iris.proofmode Require Export classes notation.
-From iris.proofmode Require Import class_instances_bi class_instances_sbi.
+From iris.proofmode Require Import modality_instances frame_instances
+     class_instances_bi class_instances_sbi.
 From stdpp Require Import hlist pretty.
 Set Default Proof Using "Type".
 Export ident.