diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v
index 9a4bb21b946ca1613e70afd4a0d0b35b0c5c7c6b..364de0720f15329ba3d7005772c96a1d1f6edfaa 100644
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -179,9 +179,9 @@ Section proofmode_classes.
     ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
   Proof.
     by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
- Qed.
+  Qed.
   Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
-    ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+    ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q) | 10.
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 End proofmode_classes.