prove the view shift invariant accessor

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.