diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index b0c24e0afec0d6205232c2a6e217b43c3b26d92e..997f212c6c0bbaec6900ffdfbb6d718ef31fc86b 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -88,13 +88,10 @@ Section tests.
 
   Lemma test_apply_fupd_intro_mask E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
-  Proof.
-    iIntros. iApply fupd_intro_mask.
-  Qed.
+  Proof. iIntros. by iApply fupd_intro_mask. Qed.
   Lemma test_apply_fupd_intro_mask_2 E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
   Proof.
-    iIntros. iFrame.
-    by iApply fupd_intro_mask'. (* But no annotation is needed here *)
+    iIntros. iFrame. by iApply fupd_intro_mask'.
   Qed.
 End tests.