diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9628ea7e45c40f602167edd5fdbf94a1fc504314..97aa9604a368e42f51c25460be84c568ee01ae9f 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -457,17 +457,17 @@ Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
 
 (* Ensure that [% ...] works as a pattern when the left-hand side of and/sep is
 pure. *)
-Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) (P : PROP) :
+Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) P :
   ⌜φ⌝ ∧ (⌜φ⌝ ∗ P) -∗ P.
 Proof.
   iIntros "[% [% $]]".
 Qed.
-Lemma test_pure_and_sep_destruct_1 (φ : Prop) (P : PROP) :
+Lemma test_pure_and_sep_destruct_1 (φ : Prop) P :
   ⌜φ⌝ ∧ (<affine> ⌜φ⌝ ∗ P) -∗ P.
 Proof.
   iIntros "[% [% $]]".
 Qed.
-Lemma test_pure_and_sep_destruct_2 (φ : Prop) (P : PROP) :
+Lemma test_pure_and_sep_destruct_2 (φ : Prop) P :
   ⌜φ⌝ ∧ (⌜φ⌝ ∗ <absorb> P) -∗ <absorb> P.
 Proof.
   iIntros "[% [% $]]".
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 6e69c5c88d99b63e30ca76bcc6423c47985911bf..80612f2c065fdb6d776ebda867969ddd738039a4 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -103,6 +103,17 @@ Section tests.
     iAssumption.
   Qed.
 
+  Lemma test_monPred_at_and_pure P i j :
+    (monPred_in j ∧ P) i ⊢ ⌜ j ⊑ i ⌝ ∧ P i.
+  Proof.
+    iDestruct 1 as "[% $]". done.
+  Qed.
+  Lemma test_monPred_at_sep_pure P i j :
+    (monPred_in j ∗ <absorb> P) i ⊢ ⌜ j ⊑ i ⌝ ∧ <absorb> P i.
+  Proof.
+    iDestruct 1 as "[% ?]". auto.
+  Qed.
+
   Context (FU : BiFUpd PROP).
 
   Lemma test_apply_fupd_intro_mask_subseteq E1 E2 P :