diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index dc207ad918866e5081141999acb3626b031ff1c3..205798085cd2f6c2ae5c5387a2149bb33108992b 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -497,11 +497,13 @@ Proof.
           -impl_wand_intuitionistically -pure_impl_forall
           bi.persistently_elim //.
 Qed.
-Global Instance into_wand_forall_prop_false p (φ : Prop) P :
-  Absorbing P → IntoWand p false (∀ _ : φ, P) ⌜ φ ⌝ P.
+Global Instance into_wand_forall_prop_false p (φ : Prop) Pφ P :
+  MakeAffinely ⌜ φ ⌝ Pφ →
+  IntoWand p false (∀ _ : φ, P) Pφ P.
 Proof.
-  intros ?.
-  rewrite /IntoWand (intuitionistically_if_elim p) /= pure_wand_forall //.
+  rewrite /MakeAffinely /IntoWand=> <-.
+  rewrite (intuitionistically_if_elim p) /=.
+  by rewrite -pure_impl_forall -persistent_impl_wand_affinely.
 Qed.
 
 Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 57992ccc987e921af097c8a1edf82395f3d2dc73..9db702ed664dbb6e7b26b154098a31bd41accde3 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -178,6 +178,50 @@ Tactic failure: iSpecialize: Q not persistent.
   ⌜φ⌝
 1 goal
   
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  "H1" : P
+  --------------------------------------â–¡
+  ⌜φ⌝
+"test_iSpecialize_impl_pure"
+     : string
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  --------------------------------------∗
+  <affine> ⌜φ⌝
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  "H1" : P
+  --------------------------------------â–¡
+  <affine> ⌜φ⌝
+"test_iSpecialize_impl_pure_affine"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  --------------------------------------∗
+  ⌜φ⌝
+1 goal
+  
   PROP : bi
   BiAffine0 : BiAffine PROP
   φ : Prop
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8a48e493082f95eac582370e3ae983630b69a3a7..700bb4382f4f29d49b28d6db96acfec96952bfc7 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -480,6 +480,38 @@ Restart.
   by iFrame.
 Abort.
 
+Check "test_iSpecialize_impl_pure".
+Lemma test_iSpecialize_forall_pure (φ : Prop) P Q :
+  φ → □ (∀ _ : φ, P) -∗ (∀ _ : φ, Q) -∗ P ∗ Q.
+Proof.
+  iIntros (?) "#H1 H2".
+  (* Adds an affine modality *)
+  iSpecialize ("H1" with "[]"). { Show. done. }
+  iSpecialize ("H2" with "[]"). { Show. done. }
+Restart.
+  iIntros (?) "#H1 H2".
+  (* Solving it directly as a pure goal also works. *)
+  iSpecialize ("H1" with "[% //]").
+  iSpecialize ("H2" with "[% //]").
+  by iFrame.
+Abort.
+
+Check "test_iSpecialize_impl_pure_affine".
+Lemma test_iSpecialize_forall_pure_affine `{!BiAffine PROP} (φ : Prop) P Q :
+  φ → □ (∀ _ : φ, P) -∗ (∀ _ : φ, Q) -∗ P ∗ Q.
+Proof.
+  iIntros (?) "#H1 H2".
+  (* Does not add an affine modality *)
+  iSpecialize ("H1" with "[]"). { Show. done. }
+  iSpecialize ("H2" with "[]"). { Show. done. }
+Restart.
+  iIntros (?) "#H1 H2".
+  (* Solving it directly as a pure goal also works. *)
+  iSpecialize ("H1" with "[% //]").
+  iSpecialize ("H2" with "[% //]").
+  by iFrame.
+Abort.
+
 Check "test_iAssert_intuitionistic".
 Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
   □ P -∗ □ |==> P.