diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 5c33516a98db11e4b8d90888688e5fe7a953460e..05dee6eeab90b4479539ed5c8335e4a0431b4aec 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -181,7 +181,7 @@ Section fractional.
   Global Instance frame_fractional p R r Φ P q RES:
     AsFractional R Φ r → AsFractional P Φ q →
     FrameFractionalHyps p R Φ RES r q →
-    Frame p R P RES.
+    Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)
   Proof.
     rewrite /Frame=>-[HR _][->?]H.
     revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 3b8c9d06cb473f9984e3afd0b09f2be513e538a8..d33ca14ebff44e96878ee9d996b02897dfd87a2a 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -284,7 +284,7 @@ Section proofmode_classes.
 
   Global Instance frame_twp p s E e R Φ Ψ :
     (∀ v, Frame p R (Φ v) (Ψ v)) →
-    Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
+    Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]) | 2.
   Proof. rewrite /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
 
   Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E [{ Φ }]).
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 59fbded04904986bf8f6555e890d10384dec0bd0..22b5565f05e5d1b9de07ecb037563be7ff251386 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -366,7 +366,7 @@ Section proofmode_classes.
 
   Global Instance frame_wp p s E e R Φ Ψ :
     (∀ v, Frame p R (Φ v) (Ψ v)) →
-    Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}).
+    Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}) | 2.
   Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 
   Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 7073ed8d2c779a779b7fc6e3f050052de1b8b651..bc90575eda6adfe2ba37f35821893d96164c7649 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -364,7 +364,7 @@ Qed.
 
 (* Framing. *)
 Global Instance frame_monPred_at_enter p i 𝓡 P 𝓠 :
-  FrameMonPredAt p i 𝓡 P 𝓠 → Frame p 𝓡 (P i) 𝓠.
+  FrameMonPredAt p i 𝓡 P 𝓠 → Frame p 𝓡 (P i) 𝓠 | 2.
 Proof. intros. done. Qed.
 Global Instance frame_monPred_at_here p P i j :
   IsBiIndexRel i j → FrameMonPredAt p j (P i) P emp | 0.
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 66a870aa54a5a58768076e1893e79d0c5b267c44..f1627aa097c34f03a16de836f2b744bb6055d692 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -73,7 +73,7 @@ Qed.
 
 Global Instance array_cons_frame l dq v vs R Q :
   Frame false R (l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs) Q →
-  Frame false R (l ↦∗{dq} (v :: vs)) Q.
+  Frame false R (l ↦∗{dq} (v :: vs)) Q | 2.
 Proof. by rewrite /Frame array_cons. Qed.
 
 Lemma update_array l dq vs off v :