diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index ab012c825e6f3c4da4251a78e97f6a471fc8ffb6..d3f82d3ebf3f46c9886e188cc5a97a3281bd8d15 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -169,8 +169,8 @@ Section inv.
             (↑N ⊆ E) True (fupd E (E ∖ ↑N)) (fupd (E ∖ ↑N) E)
             (λ _ : (), (▷ P)%I) (λ _ : (), (▷ P)%I) (λ _ : (), None).
   Proof.
-    rewrite inv_unseal /IntoAcc /accessor bi.exist_unit.
-    iIntros (?) "#Hinv _". iApply "Hinv"; done.
+    rewrite /IntoAcc /accessor bi.exist_unit.
+    iIntros (?) "#Hinv _". by iApply inv_acc.
   Qed.
 
   (** ** Derived properties *)