diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index baff426f0f0c40f9f6d039a20068d72bdf361d04..7401005bd150ca72c554a4008ca7a212998ca096 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -77,6 +77,17 @@ Proof.
   by iApply "Hclose".
 Qed.
 
+Lemma vs_inv_acc N E P :
+  ↑N ⊆ E →
+  ⊢ inv N P ={E,E∖↑N}=> ▷ P ∗ ∃ R, R ∗ (R ∗ ▷ P ={E∖↑N,E}=> True).
+Proof.
+  (* FIXME: scope printing is weird, there are [%stdpp]. *)
+  iIntros (?) "!# #Hinv".
+  iMod (inv_acc with "Hinv") as "[$ Hclose]"; first done.
+  iModIntro. iExists (▷ P ={E ∖ ↑N,E}=∗ True)%I. iFrame.
+  iIntros "!# [Hclose HP]". iMod ("Hclose" with "HP"). done.
+Qed.
+
 Lemma vs_alloc N P : ⊢ ▷ P ={↑N}=> inv N P.
 Proof. iIntros "!> HP". by iApply inv_alloc. Qed.