diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8146ab1158e1e817638df0621ba6604ad016a421..d7431c4063256474909b76cf3c51a617d1893c23 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,4 +1,5 @@
 From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import pviewshifts.
 
 Lemma demo_0 {M : cmraT} (P Q : uPred M) :
   □ (P ∨ Q) ⊢ ((∀ x, x = 0 ∨ x = 1) → (Q ∨ P)).
@@ -79,3 +80,16 @@ Proof.
   iIntros "#Hfoo **".
   by iIntros "# _".
 Qed.
+
+Section iris.
+  Context {Λ : language} {Σ : iFunctor}.
+
+  Lemma demo_7 (E1 E2 E : coPset) (P : iProp Λ Σ) :
+    E1 ⊆ E2 → E ⊆ E1 →
+    (|={E1,E}=> ▷ P) ⊢ (|={E2,E ∪ E2 ∖ E1}=> ▷ P).
+  Proof.
+    iIntros {? ?} "Hpvs".
+    iPvs "Hpvs"; first (split_and?; set_solver).
+    done.
+  Qed.
+End iris.