diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 2e736737e09a0b67dad8dbfa6acccd42c17f0288..f0cb736288d74e6285c85d0a07686af991f6c902 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -47,8 +47,8 @@ Section proofs.
   Proof.
     iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
     iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
-    iNext. iAlways. iSplit; (iIntros "[[? Ho]|?]";
-      [iLeft; iFrame "Ho"; by iApply "HPQ"|by iRight]).
+    iNext; iAlways.
+    iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
   Qed.
 
   Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 44a04c5b58a93a679dd3fafb1703e13aa1ad5ae7..45717fccacf715feccbb1bfa542fc89951ce16af 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -104,6 +104,12 @@ Lemma test_iFrame_pure (x y z : M) :
   ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
 Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
 
+Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
+  □ P1 -∗ Q2 -∗ P2 -∗ (P1 ∗ P2 ∗ False ∨ P2) ∗ (Q1 ∨ Q2).
+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_iAssert_persistent P Q : P -∗ Q -∗ True.
 Proof.
   iIntros "HP HQ".