diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v
index 9ccd7acca11e15263d75e8dcd8e87b5b86867bb7..3fef78dbeff1d87bc30e43a03079f5f0545b190f 100644
--- a/iris/proofmode/class_instances_make.v
+++ b/iris/proofmode/class_instances_make.v
@@ -8,6 +8,29 @@ Section class_instances_make.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 
+(** Affine *)
+Global Instance bi_affine_quick_affine P : BiAffine PROP → QuickAffine P.
+Proof. rewrite /QuickAffine. apply _. Qed.
+Global Instance False_quick_affine : @QuickAffine PROP False.
+Proof. rewrite /QuickAffine. apply _. Qed.
+Global Instance emp_quick_affine : @QuickAffine PROP emp.
+Proof. rewrite /QuickAffine. apply _. Qed.
+Global Instance affinely_quick_affine P : QuickAffine (<affine> P).
+Proof. rewrite /QuickAffine. apply _. Qed.
+Global Instance intuitionistically_quick_affine P : QuickAffine (â–¡ P).
+Proof. rewrite /QuickAffine. apply _. Qed.
+
+(** Absorbing *)
+Global Instance bi_affine_quick_absorbing P : BiAffine PROP → QuickAbsorbing P.
+Proof. rewrite /QuickAbsorbing. apply _. Qed.
+Global Instance pure_quick_absorbing φ : @QuickAbsorbing PROP ⌜ φ ⌝.
+Proof. rewrite /QuickAbsorbing. apply _. Qed.
+Global Instance absorbingly_quick_absorbing P : QuickAbsorbing (<absorb> P).
+Proof. rewrite /QuickAbsorbing. apply _. Qed.
+Global Instance persistently_quick_absorbing P : QuickAbsorbing (<pers> P).
+Proof. rewrite /QuickAbsorbing. apply _. Qed.
+
+(** Embed *)
 Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
   KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
 Proof. apply embed_pure. Qed.
@@ -18,46 +41,83 @@ Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
   MakeEmbed P ⎡P⎤ | 100.
 Proof. by rewrite /MakeEmbed. Qed.
 
+(** Sep *)
 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_sep_true_r P : Absorbing P → KnownRMakeSep P True P.
-Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed.
+Global Instance make_sep_true_l P : QuickAbsorbing P → KnownLMakeSep True P P.
+Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep=> ?. by apply True_sep. Qed.
+Global Instance make_sep_true_r P : QuickAbsorbing P →  KnownRMakeSep P True P.
+Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep=> ?. by apply sep_True. Qed.
 Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
 Proof. by rewrite /MakeSep. Qed.
 
+(** And *)
 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_r P : Affine P → KnownRMakeAnd P emp P.
-Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed.
+Global Instance make_and_emp_l P : QuickAffine P → KnownLMakeAnd emp P P.
+Proof. apply emp_and. Qed.
+Global Instance make_and_emp_r P : QuickAffine P → KnownRMakeAnd P emp P.
+Proof. apply and_emp. Qed.
 Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. by rewrite /MakeAnd. Qed.
 
+(** Or *)
 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_emp_l P : QuickAffine P → KnownLMakeOr emp P emp.
+Proof. apply emp_or. Qed.
+Global Instance make_or_emp_r P : QuickAffine P → KnownRMakeOr P emp emp.
+Proof. apply or_emp. Qed.
 Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
 Proof. by rewrite /MakeOr. Qed.
 
-Global Instance make_affinely_emp : @KnownMakeAffinely PROP emp emp | 0.
-Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_emp. Qed.
-Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
+(** Affinely
+
+- [make_affinely_affine] adds no modality, but only if the argument is affine.
+- [make_affinely_True] turns [True] into [emp]. For an affine BI this instance
+  overlaps with [make_affinely_affine], since [True] is affine. Since we prefer
+  to avoid [emp] in goals involving affine BIs, we give [make_affinely_affine]
+  a lower cost than [make_affinely_True].
+- [make_affinely_default] adds the modality. This is the default instance since
+  it can always be used, and thus has the highest cost. *)
+
+Global Instance make_affinely_affine P :
+  QuickAffine P → MakeAffinely P P | 0.
+Proof. apply affine_affinely. Qed.
+Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 1.
 Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
 Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
 Proof. by rewrite /MakeAffinely. Qed.
 
+(** Absorbingly
+
+- [make_absorbingly_absorbing] adds no modality, but only if the argument is
+  absorbing.
+- [make_absorbingly_emp] turns [emp] into [True]. For an affine BI this instance
+  overlaps with [make_absorbingly_absorbing], since [emp] is absorbing. For
+  consistency, we give this instance the same cost as [make_affinely_True], but
+  it does not really matter since goals in affine BIs typically do not contain
+  occurrences of [emp] to start with.
+- [make_absorbingly_default] adds the modality. This is the default instance
+  since it can always be used, and thus has the highest cost. *)
+
+Global Instance make_absorbingly_absorbing P :
+  QuickAbsorbing P → MakeAbsorbingly P P | 0.
+Proof. apply absorbing_absorbingly. Qed.
+Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 1.
+Proof.
+  by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly -absorbingly_emp_True.
+Qed.
+Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
+Proof. by rewrite /MakeAbsorbingly. Qed.
+
+(** Intuitionistically *)
 Global Instance make_intuitionistically_emp :
   @KnownMakeIntuitionistically PROP emp emp | 0.
 Proof.
@@ -74,16 +134,7 @@ Global Instance make_intuitionistically_default P :
   MakeIntuitionistically P (â–¡ P) | 100.
 Proof. by rewrite /MakeIntuitionistically. Qed.
 
-Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
-Proof.
-  by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
-     -absorbingly_emp_True.
-Qed.
-Global Instance make_absorbingly_True : @KnownMakeAbsorbingly PROP True True | 0.
-Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbingly_pure. Qed.
-Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
-Proof. by rewrite /MakeAbsorbingly. Qed.
-
+(** Later *)
 Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
 Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
 Global Instance make_laterN_emp `{!BiAffine PROP} n :
@@ -92,6 +143,7 @@ Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
 Global Instance make_laterN_default n P : MakeLaterN n P (â–·^n P) | 100.
 Proof. by rewrite /MakeLaterN. Qed.
 
+(** Except-0 *)
 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.
diff --git a/iris/proofmode/classes_make.v b/iris/proofmode/classes_make.v
index a0d8f134213142a0fbe9fd0a2ff195e6d3f87223..7d0bda7a2248c1f0784c50b5781139d482cc9331 100644
--- a/iris/proofmode/classes_make.v
+++ b/iris/proofmode/classes_make.v
@@ -39,6 +39,14 @@ that would have this behavior. *)
 From iris.bi Require Export bi.
 From iris.prelude Require Import options.
 
+(** Aliases for [Affine] and [Absorbing], but the instances are severely
+restricted. They only inspect the top-level symbol or check if the whole BI
+is affine. *)
+Class QuickAffine {PROP : bi} (P : PROP) := quick_affine : Affine P.
+Global Hint Mode QuickAffine + ! : typeclass_instances.
+Class QuickAbsorbing {PROP : bi} (P : PROP) := quick_absorbing : Absorbing P.
+Global Hint Mode QuickAbsorbing + ! : typeclass_instances.
+
 Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
   make_embed : ⎡P⎤ ⊣⊢ Q.
 Global Arguments MakeEmbed {_ _ _} _%I _%I.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 2557911ad37cca02d1ef2415e4a2d6a4d42d8824..2107e27c68f51b50a19a5d930abc4dd72b0a08dd 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -147,6 +147,65 @@ Tactic failure: iSpecialize: Q not persistent.
      : string
 The command has indeed failed with message:
 Tactic failure: iSpecialize: (|==> P)%I not persistent.
+"test_iFrame_affinely_emp"
+     : string
+1 goal
+  
+  PROP : bi
+  P : PROP
+  ============================
+  "H" : P
+  --------------------------------------â–¡
+  ∃ _ : nat, emp
+"test_iFrame_affinely_True"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  P : PROP
+  ============================
+  "H" : P
+  --------------------------------------â–¡
+  ∃ _ : nat, True
+"test_iFrame_or_1"
+     : string
+1 goal
+  
+  PROP : bi
+  P1, P2, P3 : PROP
+  ============================
+  --------------------------------------∗
+  ▷ (∃ _ : nat, emp)
+"test_iFrame_or_2"
+     : string
+1 goal
+  
+  PROP : bi
+  P1, P2, P3 : PROP
+  ============================
+  --------------------------------------∗
+  ▷ (∃ x : nat, emp ∧ ⌜x = 0⌝ ∨ emp)
+"test_iFrame_or_affine_1"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  P1, P2, P3 : PROP
+  ============================
+  --------------------------------------∗
+  ▷ (∃ _ : nat, True)
+"test_iFrame_or_affine_2"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  P1, P2, P3 : PROP
+  ============================
+  --------------------------------------∗
+  ▷ (∃ _ : nat, True)
 "test_iInduction_multiple_IHs"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index ea515a6b899e25ce8f96ec87c02b9d7bea479fa2..d98cccf87be3558a3a7d96f7930fac01ffb34386 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -51,10 +51,6 @@ Proof.
   - iSplitL "HQ"; first iAssumption. by iSplitL "H1".
 Qed.
 
-Lemma demo_3 P1 P2 P3 :
-  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
-Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
-
 Lemma test_pure_space_separated P1 :
   <affine> ⌜True⌝ ∗ P1 -∗ P1.
 Proof.
@@ -561,6 +557,65 @@ Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} :
   P -∗ Q -∗ <affine> (P ∗ Q).
 Proof. iIntros "HP HQ". iFrame "HQ". by iModIntro. Qed.
 
+Check "test_iFrame_affinely_emp".
+Lemma test_iFrame_affinely_emp P :
+  □ P -∗ ∃ _ : nat, <affine> P. (* The ∃ makes sure [iFrame] does not solve the
+  goal and we can [Show] the result *)
+Proof.
+  iIntros "#H". iFrame "H".
+  Show. (* This should become [∃ _ : nat, emp]. *)
+  by iExists 1.
+Qed.
+Check "test_iFrame_affinely_True".
+Lemma test_iFrame_affinely_True `{!BiAffine PROP} P :
+  □ P -∗ ∃ x : nat, <affine> P.
+Proof.
+  iIntros "#H". iFrame "H".
+  Show. (* This should become [∃ _ : nat, True]. Since we are in an affine BI,
+  no unnecessary [emp]s should be created. *)
+  by iExists 1.
+Qed.
+
+Check "test_iFrame_or_1".
+Lemma test_iFrame_or_1 P1 P2 P3 :
+  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ <affine> ⌜x = 0⌝) ∨ P3).
+Proof.
+  iIntros "($ & $ & $)".
+  Show. (* By framing [P3], the disjunction becomes [<affine> ⌜x = 0⌝ ∨ emp].
+  The [iFrame] tactic simplifies disjunctions if one side is trivial. In a
+  general BI, it can only turn [Q ∨ emp] into [emp]---without information
+  loss---if [Q] is affine. Here, we have [Q := <affine> ⌜x = 0⌝], which is
+  trivially affine (i.e., [QuickAffine]), and the disjunction is thus
+  simplified to [emp]. *)
+  by iExists 0.
+Qed.
+Check "test_iFrame_or_2".
+Lemma test_iFrame_or_2 P1 P2 P3 :
+  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
+Proof.
+  iIntros "($ & $ & $)".
+  Show. (* By framing [P3], the disjunction becomes [emp ∧ ⌜x = 0⌝ ∨ emp].
+  Since [emp ∧ ⌜x = 0⌝] is not trivially affine (i.e., not [QuickAffine]) it
+  is not simplified to [emp]. *)
+  iExists 0. auto.
+Qed.
+Check "test_iFrame_or_affine_1".
+Lemma test_iFrame_or_affine_1 `{!BiAffine PROP} P1 P2 P3 :
+  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ ⌜x = 0⌝) ∨ P3).
+Proof.
+  iIntros "($ & $ & $)".
+  Show. (* If the BI is affine, the disjunction should be turned into [True]. *)
+  by iExists 0.
+Qed.
+Check "test_iFrame_or_affine_2".
+Lemma test_iFrame_or_affine_2 `{!BiAffine PROP} P1 P2 P3 :
+  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
+Proof.
+  iIntros "($ & $ & $)".
+  Show. (* If the BI is affine, the disjunction should be turned into [True]. *)
+  by iExists 0.
+Qed.
+
 Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
 Proof.
   iIntros "HF".