add more tests

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 "[% [% $]]".

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 :