diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 628a1e1a1a4f6e4f4fb05cfd2cd8c1cdfa93fd3d..d44c52e1f7fc07e47d89f142f6a7e46e55e8c1b1 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -67,4 +67,11 @@ Section tests.
   Proof.
     iIntros "H HP". by iApply "H".
   Qed.
+
+  Lemma test_absolutely P Q : ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ ∀ᵢ (P ∗ Q).
+  Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed.
+
+  Lemma test_absolutely_affine `{BiAffine PROP} P Q R :
+    ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
+  Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
 End tests.