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 :