diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 04276bb3b4f8bdc8f9218da72c3ebfc5dfdf10fe..660d174cb9dc320deaa232442449ead0e117a297 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -110,6 +110,13 @@ Proof. iIntros "#HP1 HQ2 HP2". iFrame "HP1 HQ2 HP2". Qed.
 Lemma test_iFrame_disjunction_2 P : P -∗ (True ∨ True) ∗ P.
 Proof. iIntros "HP". iFrame "HP". auto. Qed.
 
+Lemma test_iFrame_conjunction_1 P Q :
+  P -∗ Q -∗ (P ∗ Q) ∧ (P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
+Lemma test_iFrame_conjunction_2 P Q :
+  P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q).
+Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
+
 Lemma test_iAssert_persistent P Q : P -∗ Q -∗ True.
 Proof.
   iIntros "HP HQ".