diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 5b118cd105613981048b5cb11d9153636d948fa6..1e6b323130699c911bdb281797410c9e5de53b74 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -23,7 +23,7 @@ Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
 Global Instance into_absorbingly_absorbing P : Absorbing P → IntoAbsorbingly P P | 1.
 Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.
 Global Instance into_absorbingly_intuitionistically P :
-  IntoAbsorbingly (<pers> P) (â–¡ P) | 0.
+  IntoAbsorbingly (<pers> P) (â–¡ P) | 2.
 Proof.
   by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
 Qed.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index b8024b8f8b0f3d3b2edd78cdc52c4a8e0592d091..19c61a492d7859ef107847e1d224b2ccb0bd505f 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -460,4 +460,10 @@ Proof.
   - iDestruct "H" as "[_ [$ _]]".
   - iDestruct "H" as "[_ [_ #$]]".
 Qed.
+
+Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q.
+Proof.
+  iIntros "[??]". iSplit; last done.
+  lazymatch goal with |- coq_tactics.envs_entails _ (â–¡ P) => done end.
+Qed.
 End tests.