diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 2c2581979e881121cef445cc56b3933bd1e41414..7c058426c0d6073c86eb555d10ac91deb0a33e36 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -138,3 +138,7 @@ Proof.
   iIntros "H". iExists _, [#10].
   iSpecialize ("H" $! _ [#10]). done.
 Qed.
+
+Lemma demo_16 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
+  P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
+Proof. eauto with iFrame. Qed.