diff --git a/naming.txt b/naming.txt
index ed87ef4c324a8540f23e23e8147d0c83fc2a8646..3096b54347bc89105b2f7b5ba260c8c6444ec9f4 100644
--- a/naming.txt
+++ b/naming.txt
@@ -12,6 +12,7 @@ j
 k
 l
 m : iGst = ghost state
+m* : prefix for option
 n
 o
 p
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 82739945d0122589cc5d02c1461d3b9a753c8527..ea423840b7c4684009a23e86d7302e77d094781e 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -130,11 +130,11 @@ Lemma slice_delete_empty E q f P Q γ :
 Proof.
   iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
-  iInv N as (b) "[>Hγ _]" "Hclose".
+  iInv N as (b) "[>Hγ _]".
   iDestruct (big_opM_delete _ f _ false with "Hf")
     as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
   iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
-  iMod ("Hclose" with "[Hγ]"); first iExists false; eauto.
+  iModIntro. iSplitL "Hγ"; first iExists false; eauto.
   iModIntro. iNext. iSplit.
   - iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
     iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_opM_delete.
@@ -147,11 +147,11 @@ Lemma slice_fill E q f γ P Q :
   slice N γ Q -∗ ▷ Q -∗ ▷?q box N f P ={E}=∗ ▷?q box N (<[γ:=true]> f) P.
 Proof.
   iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
-  iInv N as (b') "[>Hγ _]" "Hclose".
+  iInv N as (b') "[>Hγ _]".
   iDestruct (big_opM_delete _ f _ false with "Hf")
     as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
   iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
-  iMod ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
+  iModIntro. iSplitL "Hγ HQ"; first (iNext; iExists true; by iFrame).
   iModIntro; iNext; iExists Φ; iSplit.
   - by rewrite big_opM_insert_override.
   - rewrite -insert_delete big_opM_insert ?lookup_delete //.
@@ -164,13 +164,13 @@ Lemma slice_empty E q f P Q γ :
   slice N γ Q -∗ ▷?q box N f P ={E}=∗ ▷ Q ∗ ▷?q box N (<[γ:=false]> f) P.
 Proof.
   iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
-  iInv N as (b) "[>Hγ HQ]" "Hclose".
+  iInv N as (b) "[>Hγ HQ]".
   iDestruct (big_opM_delete _ f with "Hf")
     as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
   iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
   iFrame "HQ".
   iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']".
-  iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
+  iModIntro. iSplitL "Hγ"; first (iNext; iExists false; by repeat iSplit).
   iModIntro; iNext; iExists Φ; iSplit.
   - by rewrite big_opM_insert_override.
   - rewrite -insert_delete big_opM_insert ?lookup_delete //.
@@ -213,9 +213,9 @@ Proof.
   rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
   iApply (@big_sepM_impl with "Hf").
   iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
-  iInv N as (b) "[>Hγ _]" "Hclose".
+  iInv N as (b) "[>Hγ _]".
   iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
-  iApply "Hclose". iNext; iExists true. by iFrame.
+  iModIntro. iSplitL; last done. iNext; iExists true. iFrame.
 Qed.
 
 Lemma box_empty E f P :
@@ -230,10 +230,10 @@ Proof.
   { rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
     iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
     assert (true = b) as <- by eauto.
-    iInv N as (b) "[>Hγ HΦ]" "Hclose".
+    iInv N as (b) "[>Hγ HΦ]".
     iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
     iMod (box_own_auth_update γ true true false with "[$Hγ $Hγ']") as "[Hγ $]".
-    iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
+    iModIntro. iSplitL "Hγ"; first (iNext; iExists false; iFrame; eauto).
     iFrame "HγΦ Hinv". by iApply "HΦ". }
   iModIntro; iSplitL "HΦ".
   - rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP".
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 762d6e22e3e48c439704931e5abef81ed62c4db9..9626bd963df53d6dd0b144e0853b613b52defb7b 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -73,9 +73,8 @@ Section proofs.
   Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.
   Proof.
     iIntros (?) "#Hinv Hγ". iDestruct "Hinv" as (P') "[#HP' Hinv]".
-    iInv N as "[HP|>Hγ']" "Hclose".
-    - iMod ("Hclose" with "[Hγ]") as "_"; first by eauto. iModIntro. iNext.
-      iApply "HP'". done.
+    iInv N as "[HP|>Hγ']".
+    - iModIntro. iFrame "Hγ". iModIntro. iApply "HP'". done.
     - iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[].
   Qed.
 
@@ -92,15 +91,15 @@ Section proofs.
   Qed.
 
   Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
-  Global Instance elim_inv_cinv p γ E N P Q Q' :
-    (∀ R, ElimModal True false false (|={E,E∖↑N}=> R) R Q Q') →
-    ElimInv (↑N ⊆ E) (cinv N γ P) (cinv_own γ p)
-      (▷ P ∗ cinv_own γ p) (▷ P ={E∖↑N,E}=∗ True) Q Q'.
+
+  Global Instance into_acc_cinv E N γ P p :
+    IntoAcc (X:=unit) (cinv N γ P)
+            (↑N ⊆ E) (cinv_own γ p) (fupd E (E∖↑N)) (fupd (E∖↑N) E)
+            (λ _, ▷ P ∗ cinv_own γ p)%I (λ _, ▷ P)%I (λ _, None)%I.
   Proof.
-    rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
-    iApply Helim; [done|]; simpl. iSplitR "H2"; [|done].
-    iMod (cinv_open E N γ p P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto. 
-    by iFrame.
+    rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown".
+    rewrite exist_unit -assoc.
+    iApply (cinv_open with "Hinv"); done.
   Qed.
 End proofs.
 
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 5ec29362dc650289a17a4cc0c558ea45cfd9e700..1ecc9bcc72d82703cc2feaa1231ecf97b684c1df 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -109,13 +109,13 @@ Qed.
 
 Global Instance into_inv_inv N P : IntoInv (inv N P) N.
 
-Global Instance elim_inv_inv E N P Q Q' :
-  (∀ R, ElimModal True false false (|={E,E∖↑N}=> R) R Q Q') →
-  ElimInv (↑N ⊆ E) (inv N P) True (▷ P) (▷ P ={E∖↑N,E}=∗ True) Q Q'.
+Global Instance into_acc_inv E N P :
+  IntoAcc (X:=unit) (inv N P) 
+          (↑N ⊆ E) True (fupd E (E∖↑N)) (fupd (E∖↑N) E)
+          (λ _, ▷ P)%I (λ _, ▷ P)%I (λ _, None)%I.
 Proof.
-  rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
-  iApply (Helim with "[H2]"); [done|]; simpl. iSplitR "H2"; [|done].
-  iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
+  rewrite /IntoAcc /accessor exist_unit.
+  iIntros (?) "#Hinv _". iApply inv_open; done.
 Qed.
 
 Lemma inv_open_timeless E N P `{!Timeless P} :
@@ -124,4 +124,5 @@ Proof.
   iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
   iIntros "!> {$HP} HP". iApply "Hclose"; auto.
 Qed.
+
 End inv.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index c1116ef9c88fc20abef6da276e39eb491474c834..beaf8ebfe54d0ba730328d21e212bed70a651000 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -101,25 +101,26 @@ Section proofs.
     rewrite [F as X in na_own p X](union_difference_L (↑N) F) //.
     rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..].
     iDestruct "Htoks" as "[[Htoki $] $]".
-    iInv N as "[[$ >Hdis]|>Htoki2]" "Hclose".
+    iInv "Hinv" as "[[$ >Hdis]|>Htoki2]" "Hclose".
     - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
       iIntros "!> [HP $]".
-      iInv N as "[[_ >Hdis2]|>Hitok]" "Hclose".
+      iInv N as "[[_ >Hdis2]|>Hitok]".
       + iDestruct (own_valid_2 with "Hdis Hdis2") as %[_ Hval%gset_disj_valid_op].
         set_solver.
-      + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
+      + iSplitR "Hitok"; last by iFrame. eauto with iFrame.
     - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
   Qed.
 
   Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.
-  Global Instance elim_inv_na p F E N P Q Q':
-    (∀ R, ElimModal True false false (|={E}=> R)%I R Q Q') →
-    ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) (na_inv p N P) (na_own p F)
-      (▷ P ∗ na_own p (F∖↑N)) (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F) Q Q'.
+
+  Global Instance into_acc_na p F E N P :
+    IntoAcc (X:=unit) (na_inv p N P)
+            (↑N ⊆ E ∧ ↑N ⊆ F) (na_own p F) (fupd E E) (fupd E E)
+            (λ _, ▷ P ∗ na_own p (F∖↑N))%I (λ _, ▷ P ∗ na_own p (F∖↑N))%I
+              (λ _, Some (na_own p F))%I.
   Proof.
-    rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
-    iApply Helim; [done|]; simpl. iSplitR "H2"; [|done].
-    iMod (na_inv_open p E F N P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
-    by iFrame.
+    rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
+    rewrite exist_unit -assoc /=.
+    iApply (na_inv_open with "Hinv"); done.
   Qed.
 End proofs.
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index a71141f873478c5c6b31742d0b637792411b000e..e6230678381b80e232131aa5676b28fc4d733d73 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -231,6 +231,20 @@ Proof.
   - apply impl_intro_r, impl_elim_r', exist_elim=>x.
     apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r.
 Qed.
+Lemma forall_unit (Ψ : unit → PROP) :
+  (∀ x, Ψ x) ⊣⊢ Ψ ().
+Proof.
+  apply (anti_symm (⊢)).
+  - rewrite (forall_elim ()) //.
+  - apply forall_intro=>[[]]. done.
+Qed.
+Lemma exist_unit (Ψ : unit → PROP) :
+  (∃ x, Ψ x) ⊣⊢ Ψ ().
+Proof.
+  apply (anti_symm (⊢)).
+  - apply exist_elim=>[[]]. done.
+  - rewrite -(exist_intro ()). done.
+Qed.
 
 Lemma or_and_l P Q R : P ∨ Q ∧ R ⊣⊢ (P ∨ Q) ∧ (P ∨ R).
 Proof.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 8aee1924bb7256c1691f78a3bdf35e523f97017c..3187aacea9986c27d7ef8bd1bbda169eb9e10529 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -46,24 +46,24 @@ Section mono_proof.
     {{{ mcounter l n }}} incr #l {{{ RET #(); mcounter l (S n) }}}.
   Proof.
     iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
-    iDestruct "Hl" as (γ) "[#Hinv Hγf]".
-    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
-    wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
-    iModIntro. wp_let. wp_op.
-    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
+    iDestruct "Hl" as (γ) "[#? Hγf]".
+    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
+    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
+    wp_let. wp_op.
+    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
     - iDestruct (own_valid_2 with "Hγ Hγf")
         as %[?%mnat_included _]%auth_valid_discrete_2.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
-      wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
+      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      iModIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
+      wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
       iApply (own_mono with "Hγf"). apply: auth_frag_mono.
       by apply mnat_included, le_n_S.
-    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
-      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
-      iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
+    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
+      iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
+      wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
       rewrite {3}/mcounter; eauto 10.
   Qed.
 
@@ -71,12 +71,13 @@ Section mono_proof.
     {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝%nat ∧ mcounter l i }}}.
   Proof.
     iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
-    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
+    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]".
+    wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf")
       as %[?%mnat_included _]%auth_valid_discrete_2.
     iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
     { apply auth_update, (mnat_local_update _ _ c); auto. }
-    iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
   Qed.
 End mono_proof.
@@ -123,19 +124,19 @@ Section contrib_spec.
     {{{ RET #(); ccounter γ q (S n) }}}.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
-    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
-    wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
-    iModIntro. wp_let. wp_op.
-    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
+    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
+    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
+    wp_let. wp_op.
+    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
     - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); omega. }
-      wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
+      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      iModIntro. wp_if. by iApply "HΦ".
+      wp_if. by iApply "HΦ".
     - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
-      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
-      iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
+      iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
+      wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
   Qed.
 
   Lemma read_contrib_spec γ l q n :
@@ -143,9 +144,9 @@ Section contrib_spec.
     {{{ c, RET #c; ⌜n ≤ c⌝%nat ∧ ccounter γ q n }}}.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
-    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
+    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
-    iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
   Qed.
 
@@ -154,9 +155,9 @@ Section contrib_spec.
     {{{ n, RET #n; ccounter γ 1 n }}}.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
-    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
+    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
-    iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     by iApply "HΦ".
   Qed.
 End contrib_spec.
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index f9059566e4b4ded7c276d72aac613f4ece56f56a..79d6c669426af9f85cb3250c2c4f0398608d266e 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -55,21 +55,21 @@ Proof.
   wp_apply wp_fork; simpl. iSplitR "Hf".
   - wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
   - wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
-    iInv N as (v') "[Hl _]" "Hclose".
-    wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
+    iInv N as (v') "[Hl _]".
+    wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
 Qed.
 
 Lemma join_spec (Ψ : val → iProp Σ) l :
   {{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
 Proof.
   iIntros (Φ) "H HΦ". iDestruct "H" as (γ) "[Hγ #?]".
-  iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
+  iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
-  - iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
-    iModIntro. wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
+  - iModIntro. iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
+    wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
   - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
-    + iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
-      iModIntro. wp_match. by iApply "HΦ".
+    + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
+      wp_match. by iApply "HΦ".
     + iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
 Qed.
 End proof.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 23b63251c0c89912fd501d080765eb22d5000196..f3cf0e07244a3b1512166dab528cd144a3cd31dd 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -61,12 +61,12 @@ Section proof.
     {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
   Proof.
     iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
-    wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
-    - wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
-      iModIntro. iApply ("HΦ" $! false). done.
+    wp_rec. iInv N as ([]) "[Hl HR]".
+    - wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
+      iApply ("HΦ" $! false). done.
     - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
-      iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
-      iModIntro. rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
+      iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
+      rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
   Qed.
 
   Lemma acquire_spec γ lk R :
@@ -83,8 +83,9 @@ Section proof.
   Proof.
     iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
     iDestruct "Hlock" as (l ->) "#Hinv".
-    rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
-    wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
+    rewrite /release /=. wp_let. iInv N as (b) "[Hl _]".
+    wp_store. iSplitR "HΦ"; last by iApply "HΦ".
+    iModIntro. iNext. iExists false. by iFrame.
   Qed.
 End proof.
 
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index c108b3f36103123f7a063778b7eaf0ca7a600cf5..db6c9ab28e9b0b7da3b2d2b30c71c4253140d35c 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -88,20 +88,18 @@ Section proof.
   Proof.
     iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
     iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
-    iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
+    iInv N as (o n) "(Hlo & Hln & Ha)".
     wp_load. destruct (decide (x = o)) as [->|Hneq].
     - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
-      + iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
+      + iModIntro. iSplitL "Hlo Hln Hainv Ht".
         { iNext. iExists o, n. iFrame. }
-        iModIntro. wp_let. wp_op. case_bool_decide; [|done].
-        wp_if.
+        wp_let. wp_op. case_bool_decide; [|done]. wp_if.
         iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
       + iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
         set_solver.
-    - iMod ("Hclose" with "[Hlo Hln Ha]").
+    - iModIntro. iSplitL "Hlo Hln Ha".
       { iNext. iExists o, n. by iFrame. }
-      iModIntro. wp_let.
-      wp_op. case_bool_decide; [simplify_eq |].
+      wp_let. wp_op. case_bool_decide; [simplify_eq |].
       wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
   Qed.
 
@@ -110,30 +108,28 @@ Section proof.
   Proof.
     iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
     iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj.
-    iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
-    wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_".
+    iInv N as (o n) "[Hlo [Hln Ha]]".
+    wp_load. iModIntro. iSplitL "Hlo Hln Ha".
     { iNext. iExists o, n. by iFrame. }
-    iModIntro. wp_let. wp_proj. wp_op.
-    wp_bind (CAS _ _ _).
-    iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)" "Hclose".
+    wp_let. wp_proj. wp_op. wp_bind (CAS _ _ _).
+    iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
     destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
-    - wp_cas_suc.
-      iMod (own_update with "Hauth") as "[Hauth Hofull]".
+    - iMod (own_update with "Hauth") as "[Hauth Hofull]".
       { eapply auth_update_alloc, prod_local_update_2.
         eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
         apply (seq_set_S_disjoint 0). }
       rewrite -(seq_set_S_union_L 0).
-      iMod ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_".
+      wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
       { iNext. iExists o', (S n).
         rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
-      iModIntro. wp_if.
+      wp_if.
       iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
       + iFrame. rewrite /is_lock; eauto 10.
       + by iNext.
-    - wp_cas_fail.
-      iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
+    - wp_cas_fail. iModIntro.
+      iSplitL "Hlo' Hln' Hauth Haown".
       { iNext. iExists o', n'. by iFrame. }
-      iModIntro. wp_if. by iApply "IH"; auto.
+      wp_if. by iApply "IH"; auto.
   Qed.
 
   Lemma release_spec γ lk R :
@@ -142,15 +138,15 @@ Section proof.
     iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
     iDestruct "Hγ" as (o) "Hγo".
     wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
-    iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
+    iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
     wp_load.
     iDestruct (own_valid_2 with "Hauth Hγo") as
       %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
-    iMod ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
+    iModIntro. iSplitL "Hlo Hln Hauth Haown".
     { iNext. iExists o, n. by iFrame. }
-    iModIntro. wp_op.
-    iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
-    wp_store.
+    wp_op.
+    iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
+    iApply wp_fupd. wp_store.
     iDestruct (own_valid_2 with "Hauth Hγo") as
       %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
     iDestruct "Haown" as "[[Hγo' _]|Haown]".
@@ -158,8 +154,8 @@ Section proof.
     iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
     { apply auth_update, prod_local_update_1.
       by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
-    iMod ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last by iApply "HΦ".
-    iNext. iExists (S o), n'.
+    iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
+    iIntros "!> !>". iExists (S o), n'.
     rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
   Qed.
 End proof.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 8aa18f95e6c7f003ae5ce9af5711d3a4ed884f88..13879ab407550dfa1fdd07a9cf6f935888ff4f9d 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -404,4 +404,29 @@ Section proofmode_classes.
   Global Instance add_modal_fupd_wp s E e P Φ :
     AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
+
+  Global Instance elim_acc_wp {X} E1 E2 α β γ e s Φ :
+    Atomic (stuckness_to_atomicity s) e →
+    ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
+            α β γ (WP e @ s; E1 {{ Φ }})
+            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
+  Proof.
+    intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
+    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+    iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
+    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
+  Qed.
+
+  Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
+    ElimAcc (X:=X) (fupd E E) (fupd E E)
+            α β γ (WP e @ s; E {{ Φ }})
+            (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
+  Proof.
+    rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
+    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+    iApply wp_fupd.
+    iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
+    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
+  Qed.
+
 End proofmode_classes.
diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index 159a09b5ae02e28cbbfdc268f2704109535a512a..a889f5924601ba44acc84646d1fcf1cf723a7f04 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -84,6 +84,11 @@ Qed.
 Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
 Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
 
+(** Copies of some definitions so we can control their unfolding *)
 Definition option_bind {A B} (f : A → option B) (mx : option A) : option B :=
   match mx with Some x => f x | None => None end.
-Arguments option_bind _ _ _ !_ /.
+Arguments option_bind {_ _} _ !_ / : assert.
+
+Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
+  match mx with None => y | Some x => f x end.
+Arguments from_option {_ _} _ _ !_ / : assert.
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index ff23506f5590094cdc83f8f763c93e4328edec2c..164ce8999cabb64b9da491e58c631cc533b1642b 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -1,6 +1,6 @@
 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import modality_instances classes.
+From iris.proofmode Require Import modality_instances classes ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -8,6 +8,33 @@ Section bi_instances.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 
+(* AsEmpValid *)
+Global Instance as_emp_valid_emp_valid {PROP : bi} (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0.
+Proof. by rewrite /AsEmpValid. Qed.
+Global Instance as_emp_valid_entails {PROP : bi} (P Q : PROP) : AsEmpValid0 (P ⊢ Q) (P -∗ Q).
+Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
+Global Instance as_emp_valid_equiv {PROP : bi} (P Q : PROP) : AsEmpValid0 (P ≡ Q) (P ∗-∗ Q).
+Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
+
+Global Instance as_emp_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) :
+  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀ x, φ x) (∀ x, P x).
+Proof.
+  rewrite /AsEmpValid=>H1. split=>H2.
+  - apply bi.forall_intro=>?. apply H1, H2.
+  - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
+Qed.
+
+(* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
+   sure this instance is not used when there is no embedding between
+   PROP and PROP'.
+   The first [`{BiEmbed PROP PROP'}] is not considered as a premise by
+   Coq TC search mechanism because the rest of the hypothesis is dependent
+   on it. *)
+Global Instance as_emp_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
+  BiEmbed PROP PROP' →
+  AsEmpValid0 φ P → AsEmpValid φ ⎡P⎤.
+Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ ->. rewrite embed_emp_valid //. Qed.
+
 (* FromAffinely *)
 Global Instance from_affinely_affine P : Affine P → FromAffinely P P.
 Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
@@ -820,35 +847,37 @@ Global Instance add_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
   AddModal P P' (|==> ⎡Q⎤)%I → AddModal P P' ⎡|==> Q⎤.
 Proof. by rewrite /AddModal !embed_bupd. Qed.
 
-(* IntoEmbed *)
-Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
-  IntoEmbed ⎡P⎤ P.
-Proof. by rewrite /IntoEmbed. Qed.
-
-(* AsEmpValid *)
-Global Instance as_emp_valid_emp_valid {PROP : bi} (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0.
-Proof. by rewrite /AsEmpValid. Qed.
-Global Instance as_emp_valid_entails {PROP : bi} (P Q : PROP) : AsEmpValid0 (P ⊢ Q) (P -∗ Q).
-Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
-Global Instance as_emp_valid_equiv {PROP : bi} (P Q : PROP) : AsEmpValid0 (P ≡ Q) (P ∗-∗ Q).
-Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
+(* ElimInv *)
+Global Instance elim_inv_acc_without_close {X : Type}
+       φ Pinv Pin
+       M1 M2 α β mγ Q (Q' : X → PROP) :
+  IntoAcc (X:=X) Pinv φ Pin M1 M2 α β mγ →
+  ElimAcc (X:=X) M1 M2 α β mγ Q Q' →
+  ElimInv φ Pinv Pin α None Q Q'.
+Proof.
+  rewrite /ElimAcc /IntoAcc /ElimInv.
+  iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
+  iApply (Helim with "[Hcont]").
+  - iIntros (x) "Hα". iApply "Hcont". iSplitL; simpl; done.
+  - iApply (Hacc with "Hinv Hin"). done.
+Qed.
 
-Global Instance as_emp_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) :
-  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀ x, φ x) (∀ x, P x).
+Global Instance elim_inv_acc_with_close {X : Type}
+       φ Pinv Pin
+       M1 M2 α β mγ Q Q' :
+  IntoAcc Pinv φ Pin M1 M2 α β mγ →
+  (∀ R, ElimModal True false false (M1 R) R Q Q') →
+  ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x -∗ M2 (proofmode.base.from_option id emp (mγ x))))%I
+          Q (λ _, Q').
 Proof.
-  rewrite /AsEmpValid=>H1. split=>H2.
-  - apply bi.forall_intro=>?. apply H1, H2.
-  - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
+  rewrite /ElimAcc /IntoAcc /ElimInv.
+  iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
+  iMod (Hacc with "Hinv Hin") as (x) "[Hα Hclose]"; first done.
+  iApply "Hcont". simpl. iSplitL "Hα"; done.
 Qed.
 
-(* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
-   sure this instance is not used when there is no embedding between
-   PROP and PROP'.
-   The first [`{BiEmbed PROP PROP'}] is not considered as a premise by
-   Coq TC search mechanism because the rest of the hypothesis is dependent
-   on it. *)
-Global Instance as_emp_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
-  BiEmbed PROP PROP' →
-  AsEmpValid0 φ P → AsEmpValid φ ⎡P⎤.
-Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ ->. rewrite embed_emp_valid //. Qed.
+(* IntoEmbed *)
+Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
+  IntoEmbed ⎡P⎤ P.
+Proof. by rewrite /IntoEmbed. Qed.
 End bi_instances.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 78b7091f7fb0666bdfe6b25b189f183a324d3933..5f81086c706f160e191fd126cc35d8f454d315de 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -1,6 +1,6 @@
 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import modality_instances classes.
+From iris.proofmode Require Import modality_instances classes class_instances_bi ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -551,6 +551,23 @@ Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
   AddModal P P' (|={E1,E2}=> ⎡Q⎤)%I → AddModal P P' ⎡|={E1,E2}=> Q⎤.
 Proof. by rewrite /AddModal !embed_fupd. Qed.
 
+(* ElimAcc *)
+Global Instance elim_acc_vs `{BiFUpd PROP} {X} E1 E2 E α β mγ Q :
+  (* FIXME: Why %I? ElimAcc sets the right scopes! *)
+  ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β mγ
+          (|={E1,E}=> Q)
+          (λ x, |={E2}=> (β x ∗ (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q))))%I.
+Proof.
+  rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
+  iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+  iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
+  iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
+Qed.
+
+(* IntoAcc *)
+(* TODO: We could have instances from "unfolded" accessors with or without
+   the first binder. *)
+
 (* IntoLater *)
 Global Instance into_laterN_0 only_head P : IntoLaterN only_head 0 P P.
 Proof. by rewrite /IntoLaterN /MaybeIntoLaterN. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 4ad095999e5cd16a57ac49a29b4d6abcf0575429..4878055e57ed2f2c2e2cda6543645c376f94669f 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -519,25 +519,73 @@ Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
 Arguments IntoInv {_} _%I _.
 Hint Mode IntoInv + ! - : typeclass_instances.
 
-(* Input: [Pinv]
+(** Accessors.
+    This definition only exists for the purpose of the proof mode; a truly
+    usable and general form would use telescopes and also allow binders for the
+    closing view shift.  [γ] is an [option] to make it easy for ElimAcc
+    instances to recognize the [emp] case and make it look nicer. *)
+Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
+           (α β : X → PROP) (mγ : X → option PROP) : PROP :=
+  M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (mγ x) id)))%I.
+
+(* Typeclass for assertions around which accessors can be elliminated.
+   Inputs: [Q], [E1], [E2], [α], [β], [γ]
+   Outputs: [Q']
+
+   Elliminates an accessor [accessor E1 E2 α β γ] in goal [Q'], turning the goal
+   into [Q'] with a new assumption [α x]. *)
+Class ElimAcc {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
+      (α β : X → PROP) (mγ : X → option PROP)
+      (Q : PROP) (Q' : X → PROP) :=
+  elim_acc : ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β mγ -∗ Q).
+Arguments ElimAcc {_} {_} _%I _%I _%I _%I _%I _%I : simpl never.
+Arguments elim_acc {_} {_} _%I _%I _%I _%I _%I _%I {_}.
+Hint Mode ElimAcc + ! ! ! ! ! ! ! - : typeclass_instances.
+
+(* Turn [P] into an accessor.
+   Inputs:
+   - [Pacc]: the assertion to be turned into an accessor (e.g. an invariant)
+   Outputs:
+   - [Pin]: additional logic assertion needed for starting the accessor.
+   - [φ]: additional Coq assertion needed for starting the accessor.
+   - [X] [α], [β], [γ]: the accessor parameters.
+   - [M1], [M2]: the two accessor modalities (they will typically still have
+     some evars though, e.g. for the masks)
+*)
+Class IntoAcc {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
+      (M1 M2 : PROP → PROP) (α β : X → PROP) (mγ : X → option PROP) :=
+  into_acc : φ → Pacc -∗ Pin -∗ accessor M1 M2 α β mγ.
+Arguments IntoAcc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I : simpl never.
+Arguments into_acc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I {_} : simpl never.
+Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
+
+(* The typeclass used for the [iInv] tactic.
+   Input: [Pinv]
    Arguments:
    - [Pinv] is an invariant assertion
-   - [Pin] is an additional assertion needed for opening an invariant
+   - [Pin] is an additional logic assertion needed for opening an invariant
+   - [φ] is an additional Coq assertion needed for opening an invariant
    - [Pout] is the assertion obtained by opening the invariant
-   - [Pclose] is the assertion which contains an update modality to close the invariant
+   - [Pclose] is the closing view shift.  It must be (Some _) or None
+     when doing typeclass search as instances are allowed to make a
+     case distinction on whether the user wants a closing view-shift or not.
    - [Q] is a goal on which iInv may be invoked
    - [Q'] is the transformed goal that must be proved after opening the invariant.
 
-   There are similarities to the definition of ElimModal, however we
-   want to be general enough to support uses in settings where there
-   is not a clearly associated instance of ElimModal of the right form
-   (e.g. to handle Iris 2.0 usage of iInv).
+   Most users will never want to instantiate this; there is a general instance
+   based on [ElimAcc] and [IntoAcc].  However, logics like Iris 2 that support
+   invariants but not mask-changing fancy updates can use this class directly to
+   still benefit from [iInv].
+
+   TODO: Add support for a binder (like accessors have it).
 *)
-Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Pclose Q Q' : PROP) :=
-  elim_inv : φ → Pinv ∗ Pin ∗ (Pout ∗ Pclose -∗ Q') ⊢ Q.
-Arguments ElimInv {_} _ _%I _%I _%I _%I _%I : simpl never.
-Arguments elim_inv {_} _ _%I _%I _%I _%I _%I _%I _%I.
-Hint Mode ElimInv + - ! - - - ! - : typeclass_instances.
+Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
+      (Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))
+      (Q : PROP) (Q' : X → PROP) :=
+  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (default (λ _, emp) mPclose id) x -∗ Q' x) ⊢ Q.
+Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
+Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
+Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
 
 (* We make sure that tactics that perform actions on *specific* hypotheses or
 parts of the goal look through the [tc_opaque] connective, which is used to make
@@ -585,6 +633,6 @@ Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
   ElimModal φ p p' P P' Q Q' → ElimModal φ p p' (tc_opaque P) P' Q Q' := id.
 Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
   IntoInv P N → IntoInv (tc_opaque P) N := id.
-Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Pclose Q Q' : PROP) :
-  ElimInv φ Pinv Pin Pout Pclose Q Q' →
+Instance elim_inv_tc_opaque {PROP : sbi} {X} φ Pinv Pin Pout Pclose Q Q' :
+  ElimInv (PROP:=PROP) (X:=X) φ Pinv Pin Pout Pclose Q Q' →
   ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index d8b0f59fd72593a90e12ce242c26f9774306d5d0..65b3d2961ddd4d0c786ead804caf46090064ca71 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -136,6 +136,12 @@ Definition prop_of_env {PROP : bi} (Γ : env PROP) : PROP :=
   in
   match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
 
+Definition maybe_wand {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
+  match mP with
+  | None => Q
+  | Some P => (P -∗ Q)%I
+  end.
+
 (* Coq versions of the tactics *)
 Section bi_tactics.
 Context {PROP : bi}.
@@ -438,6 +444,10 @@ Proof.
   rewrite /= assoc (comm _ P0 P) IH //.
 Qed.
 
+Lemma maybe_wand_sound (mP : option PROP) Q :
+  maybe_wand mP Q ⊣⊢ (default emp mP id -∗ Q).
+Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
+
 Global Instance envs_Forall2_refl (R : relation PROP) :
   Reflexive R → Reflexive (envs_Forall2 R).
 Proof. by constructor. Qed.
@@ -736,6 +746,7 @@ Proof.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_singleton_sound Δ2) //; simpl.
   rewrite HP1 into_wand /= -(add_modal P1' P1 Q). cancel [P1'].
+
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
@@ -1065,22 +1076,6 @@ Proof.
   rewrite HΔ. by eapply elim_modal.
 Qed.
 
-(** * Invariants *)
-Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Pclose Q Q' :
-  envs_lookup_delete false i Δ = Some (p, P, Δ') →
-  ElimInv φ P Pin Pout Pclose Q Q' →
-  φ →
-  (∀ R, ∃ Δ'',
-    envs_app false (Esnoc Enil j (Pin -∗ (Pout -∗ Pclose -∗ Q') -∗ R)%I) Δ' = Some Δ'' ∧
-    envs_entails Δ'' R) →
-  envs_entails Δ Q.
-Proof.
-  rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] ?? /(_ Q) [Δ'' [? <-]].
-  rewrite (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
-  apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
-  rewrite intuitionistically_if_elim -assoc wand_curry. auto.
-Qed.
-
 (** * Accumulate hypotheses *)
 Lemma tac_accu Δ P :
   prop_of_env (env_spatial Δ) = P →
@@ -1098,6 +1093,26 @@ Proof.
   rewrite envs_entails_eq => <-. by setoid_rewrite <-envs_incr_counter_equiv.
 Qed.
 
+(** * Invariants *)
+Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X → PROP))
+      Q (Q' : X → PROP) :
+  envs_lookup_delete false i Δ = Some (p, Pinv, Δ') →
+  ElimInv φ Pinv Pin Pout Pclose Q Q' →
+  φ →
+  (∀ R, ∃ Δ'',
+    envs_app false (Esnoc Enil j
+            (Pin -∗ (∀ x, Pout x -∗ from_option (λ Pclose, Pclose x -∗ Q' x) (Q' x) Pclose) -∗ R)%I) Δ'
+      = Some Δ'' ∧
+    envs_entails Δ'' R) →
+  envs_entails Δ Q.
+Proof.
+  rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] Hinv ? /(_ Q) [Δ'' [? <-]].
+  rewrite (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
+  apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
+  rewrite intuitionistically_if_elim -assoc. destruct Pclose; simpl in *.
+  - setoid_rewrite wand_curry. auto.
+  - setoid_rewrite <-(right_id emp%I _ (Pout _)). auto.
+Qed.
 
 End bi_tactics.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 49999e5b61006220a477eabb52f4430a30eb3ee8..920fa28677f11f26d2d960bffd40dfcf384df782 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -7,15 +7,18 @@ From stdpp Require Import hlist pretty.
 Set Default Proof Using "Type".
 Export ident.
 
+(** These are all proofmode-internal definitions and hence unfolding them should
+not affect the user's goal. *)
+(* TODO: Can we option_bind, from_option, maybe_wand reduce only if applied to a constructor? *)
 Declare Reduction env_cbv := cbv [
-  option_bind
+  option_bind from_option
   beq ascii_beq string_beq positive_beq Pos.succ ident_beq
   env_lookup env_lookup_delete env_delete env_app env_replace env_dom
   env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
     envs_simple_replace envs_replace envs_split
     envs_clear_spatial envs_clear_persistent envs_incr_counter
-    envs_split_go envs_split prop_of_env].
+    envs_split_go envs_split prop_of_env maybe_wand].
 Ltac env_cbv :=
   match goal with |- ?u => let v := eval env_cbv in u in change v end.
 Ltac env_reflexivity := env_cbv; exact eq_refl.
@@ -1887,7 +1890,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
 
 (* The argument [select] is the namespace [N] or hypothesis name ["H"] of the
 invariant. *)
-Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) constr(Hclose) :=
+Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(Hclose) "in" tactic(tac) :=
   iStartProof;
   let pats := spec_pat.parse pats in
   lazymatch pats with
@@ -1895,15 +1898,20 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) c
   | _ => fail "iInv: exactly one specialization pattern should be given"
   end;
   let H := iFresh in
+  let Pclose_pat :=
+    lazymatch Hclose with
+    | Some _ => open_constr:(Some _)
+    | None => open_constr:(None)
+    end in
   lazymatch type of select with
   | string =>
-     eapply tac_inv_elim with _ select H _ _ _ _ _ _ _;
+     eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat);
      first by (iAssumptionCore || fail "iInv: invariant" select "not found")
   | ident  =>
-     eapply tac_inv_elim with _ select H _ _ _ _ _ _ _;
+     eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat);
      first by (iAssumptionCore || fail "iInv: invariant" select "not found")
   | namespace =>
-     eapply tac_inv_elim with _ _ H _ _ _ _ _ _ _;
+     eapply @tac_inv_elim with (j:=H) (Pclose:=Pclose_pat);
      first by (iAssumptionInv select || fail "iInv: invariant" select "not found")
   | _ => fail "iInv: selector" select "is not of the right type "
   end;
@@ -1912,52 +1920,167 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) c
      fail "iInv: cannot eliminate invariant " I
     |try (split_and?; solve [ fast_done | solve_ndisj ])
     |let R := fresh in intros R; eexists; split; [env_reflexivity|];
+     (* Now we are left proving [envs_entails Δ'' R]. *)
      iSpecializePat H pats; last (
-       iApplyHyp H; clear R;
-       iIntros H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
-       iIntros Hclose;
-       tac H
+       iApplyHyp H; clear R; env_cbv;
+       (* Now the goal is [∀ x, Pout x -∗ maybe_wand (Pclose x) (Q' x)] *)
+       let x := fresh in
+       iIntros (x);
+       iIntro H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
+       lazymatch Hclose with
+       | Some ?Hcl => iIntros Hcl
+       | None => idtac
+       end;
+       tac x H
     )].
 
-Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
-  iInvCore N with "[$]" as ltac:(tac) Hclose.
+(* Without closing view shift *)
+Tactic Notation "iInvCore" constr(N) "with" constr(pats) "in" tactic(tac) :=
+  iInvCore N with pats as (@None string) in ltac:(tac).
+(* Without pattern *)
+Tactic Notation "iInvCore" constr(N) "as" constr(Hclose) "in" tactic(tac) :=
+  iInvCore N with "[$]" as Hclose in ltac:(tac).
+(* Without both *)
+Tactic Notation "iInvCore" constr(N) "in" tactic(tac) :=
+  iInvCore N with "[$]" as (@None string) in ltac:(tac).
+
+(* With everything *)
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as pat).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as (x1) pat).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as (x1 x2) pat).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as (x1 x2 x3) pat).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as (x1 x2 x3 x4) pat).
+
+(* Without closing view shift *)
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) :=
+   iInvCore N with Hs in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as pat
+                | _ => fail "Missing intro pattern for accessor variable"
+                end).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) :=
+   iInvCore N with Hs in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1) pat
+                | _ => revert x; intros x1; iDestructHyp H as      pat
+                end).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) :=
+   iInvCore N with Hs in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1 x2) pat
+                | _ => revert x; intros x1; iDestructHyp H as (   x2) pat
+                end).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")"
+    constr(pat) :=
+   iInvCore N with Hs in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1 x2 x3) pat
+                | _ => revert x; intros x1; iDestructHyp H as (   x2 x3) pat
+                end).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) :=
+   iInvCore N with Hs in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4) pat
+                | _ => revert x; intros x1; iDestructHyp H as (   x2 x3 x4) pat
+                end).
 
+(* Without pattern *)
 Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as pat) Hclose.
+   iInvCore N as (Some Hclose) in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as pat
+                | _ => fail "Missing intro pattern for accessor variable"
+                end).
 Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
     constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1) pat) Hclose.
+   iInvCore N as (Some Hclose) in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1) pat
+                | _ => revert x; intros x1; iDestructHyp H as      pat
+                end).
 Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1 x2) pat) Hclose.
+   iInvCore N as (Some Hclose) in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1 x2) pat
+                | _ => revert x; intros x1; iDestructHyp H as (   x2) pat
+                end).
 Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")"
     constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3) pat) Hclose.
+   iInvCore N as (Some Hclose) in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1 x2 x3) pat
+                | _ => revert x; intros x1; iDestructHyp H as (   x2 x3) pat
+                end).
 Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
     constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
-Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) constr(Hclose) :=
-   iInvCore N with Hs as (fun H => iDestructHyp H as pat) Hclose.
-Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N with Hs as (fun H => iDestructHyp H as (x1) pat) Hclose.
-Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
-   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2) pat) Hclose.
-Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+   iInvCore N as (Some Hclose) in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4) pat
+                | _ => revert x; intros x1; iDestructHyp H as (   x2 x3 x4) pat
+                end).
+
+(* Without both *)
+Tactic Notation "iInv" constr(N) "as" constr(pat) :=
+   iInvCore N in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as pat
+                | _ => fail "Missing intro pattern for accessor variable"
+                end).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) :=
+   iInvCore N in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1) pat
+                | _ => revert x; intros x1; iDestructHyp H as      pat
+                end).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) :=
+   iInvCore N in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1 x2) pat
+                | _ => revert x; intros x1; iDestructHyp H as (   x2)  pat
+                end).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3) pat) Hclose.
-Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+    constr(pat) :=
+   iInvCore N in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1 x2 x3) pat
+                | _ => revert x; intros x1; iDestructHyp H as (   x2 x3)  pat
+                end).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
+    constr(pat) :=
+   iInvCore N in
+    (fun x H => lazymatch type of x with
+                | unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4) pat
+                | _ => revert x; intros x1; iDestructHyp H as (   x2 x3 x4)  pat
+                end).
 
+(** Miscellaneous *)
 Tactic Notation "iAccu" :=
   iStartProof; eapply tac_accu; [env_reflexivity || fail "iAccu: not an evar"].
 
+(** Automation *)
 Hint Extern 0 (_ ⊢ _) => iStartProof.
 
 (* Make sure that by and done solve trivial things in proof mode *)
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index d3a495e55394c305da4ed7864d399cc660d7fe5f..635c3cd3915c4d0010afbc1272bd80422f3e9c02 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -486,12 +486,28 @@ Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 𝓟 𝓟' Q i :
   AddModal 𝓟 𝓟' (|={E1,E2}=> Q i) → AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
 Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
 
-Global Instance elim_inv_embed φ 𝓟inv 𝓟in 𝓟out 𝓟close Pin Pout Pclose Q Q' :
-  (∀ i, ElimInv φ 𝓟inv 𝓟in 𝓟out 𝓟close (Q i) (Q' i)) →
-  MakeEmbed 𝓟in Pin → MakeEmbed 𝓟out Pout → MakeEmbed 𝓟close Pclose →
-  ElimInv φ ⎡𝓟inv⎤ Pin Pout Pclose Q Q'.
-Proof.
-  rewrite /MakeEmbed /ElimInv=>H <- <- <- ?. iStartProof PROP.
-  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?". by iApply "HQ'".
+Global Instance elim_inv_embed_with_close {X : Type} φ
+       𝓟inv 𝓟in (𝓟out 𝓟close : X → PROP)
+       Pin (Pout Pclose : X → monPred)
+       Q (Q' : X → monPred) :
+  (∀ i, ElimInv φ 𝓟inv 𝓟in 𝓟out (Some 𝓟close) (Q i) (λ x, Q' x i)) →
+  MakeEmbed 𝓟in Pin → (∀ x, MakeEmbed (𝓟out x) (Pout x)) →
+  (∀ x, MakeEmbed (𝓟close x) (Pclose x)) →
+  ElimInv (X:=X) φ ⎡𝓟inv⎤ Pin Pout (Some Pclose) Q Q'.
+Proof.
+  rewrite /MakeEmbed /ElimInv=>H <- Hout Hclose ?. iStartProof PROP.
+  setoid_rewrite <-Hout. setoid_rewrite <-Hclose.
+  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?". by iApply "HQ'".
+Qed.
+Global Instance elim_inv_embed_without_close  {X : Type}
+       φ 𝓟inv 𝓟in (𝓟out : X → PROP) Pin (Pout : X → monPred) Q (Q' : X → monPred) :
+  (∀ i, ElimInv φ 𝓟inv 𝓟in 𝓟out None (Q i) (λ x, Q' x i)) →
+  MakeEmbed 𝓟in Pin → (∀ x, MakeEmbed (𝓟out x) (Pout x)) →
+  ElimInv (X:=X) φ ⎡𝓟inv⎤ Pin Pout None Q Q'.
+Proof.
+  rewrite /MakeEmbed /ElimInv=>H <-Hout ?. iStartProof PROP.
+  setoid_rewrite <-Hout.
+  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?". by iApply "HQ'".
 Qed.
+
 End sbi.
diff --git a/theories/tests/one_shot.v b/theories/tests/one_shot.v
index 566f525801ab8e67eacf332228bbd2fb34ca33e2..53218278ef905cf98a380cd6a3e8ad0b5e7ac048 100644
--- a/theories/tests/one_shot.v
+++ b/theories/tests/one_shot.v
@@ -49,15 +49,15 @@ Proof.
   { iNext. iLeft. by iSplitL "Hl". }
   iModIntro. iApply "Hf"; iSplit.
   - iIntros (n) "!#". wp_let.
-    iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m) "[Hl Hγ]".
-    + wp_cas_suc. iMod (own_update with "Hγ") as "Hγ".
+    iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
+    + iMod (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }
-      iMod ("Hclose" with "[-]"); last eauto.
-      iNext; iRight; iExists n; by iFrame.
-    + wp_cas_fail. iMod ("Hclose" with "[-]"); last eauto.
+      wp_cas_suc. iSplitL; last eauto.
+      iModIntro. iNext; iRight; iExists n; by iFrame.
+    + wp_cas_fail. iSplitL; last eauto.
       rewrite /one_shot_inv; eauto 10.
   - iIntros "!# /=". wp_seq. wp_bind (! _)%E.
-    iInv N as ">Hγ" "Hclose".
+    iInv N as ">Hγ".
     iAssert (∃ v, l ↦ v ∗ ((⌜v = NONEV⌝ ∗ own γ Pending) ∨
        ∃ n : Z, ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv".
     { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
@@ -69,18 +69,18 @@ Proof.
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
       + iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
-    iMod ("Hclose" with "[Hinv]") as "_"; eauto; iModIntro.
-    wp_let. iIntros "!#". wp_seq.
+    iSplitL "Hinv"; first by eauto.
+    iModIntro. wp_let. iIntros "!#". wp_seq.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
     { by wp_match. }
     wp_match. wp_bind (! _)%E.
-    iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m') "[Hl Hγ]".
+    iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
     { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
     wp_load.
     iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
-    iMod ("Hclose" with "[Hl]") as "_".
+    iModIntro. iSplitL "Hl".
     { iNext; iRight; by eauto. }
-    iModIntro. wp_match. iApply wp_assert.
+    wp_match. iApply wp_assert.
     wp_op. by case_bool_decide.
 Qed.
 
diff --git a/theories/tests/proofmode_iris.v b/theories/tests/proofmode_iris.v
index 606dd94a4599a0bc2c4c4b294294a916afeab0f8..df20ac3d192317be8b36e77e77f0ea86a12f27dc 100644
--- a/theories/tests/proofmode_iris.v
+++ b/theories/tests/proofmode_iris.v
@@ -61,6 +61,13 @@ Section iris_tests.
   Qed.
 
   Lemma test_iInv_0 N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
+  Proof.
+    iIntros "#H".
+    iInv N as "#H2".
+    iModIntro. iSplit; auto.
+  Qed.
+
+  Lemma test_iInv_0_with_close N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
   Proof.
     iIntros "#H".
     iInv N as "#H2" "Hclose".
@@ -73,13 +80,20 @@ Section iris_tests.
     inv N (<pers> P) ={E}=∗ ▷ P.
   Proof.
     iIntros (?) "#H".
-    iInv N as "#H2" "Hclose".
-    iMod ("Hclose" with "H2").
-    iModIntro. by iNext.
+    iInv N as "#H2".
+    iModIntro. iSplit; auto.
   Qed.
 
   Lemma test_iInv_2 γ p N P:
     cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
+  Proof.
+    iIntros "(#?&?)".
+    iInv N as "(#HP&Hown)".
+    iModIntro. iSplit; auto with iFrame.
+  Qed.
+
+  Lemma test_iInv_2_with_close γ p N P:
+    cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
   Proof.
     iIntros "(#?&?)".
     iInv N as "(#HP&Hown)" "Hclose".
@@ -92,15 +106,24 @@ Section iris_tests.
       ={⊤}=∗ cinv_own γ p1 ∗ cinv_own γ p2  ∗ ▷ P.
   Proof.
     iIntros "(#?&Hown1&Hown2)".
-    iInv N with "[Hown2 //]" as "(#HP&Hown2)" "Hclose".
-    iMod ("Hclose" with "HP").
-    iModIntro. iFrame. by iNext.
+    iInv N with "[Hown2 //]" as "(#HP&Hown2)".
+    iModIntro. iSplit; auto with iFrame.
   Qed.
 
   Lemma test_iInv_4 t N E1 E2 P:
     ↑N ⊆ E2 →
     na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
          ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2  ∗ ▷ P.
+  Proof.
+    iIntros (?) "(#?&Hown1&Hown2)".
+    iInv N as "(#HP&Hown2)".
+    iModIntro. iSplitL "Hown2"; auto with iFrame.
+  Qed.
+
+  Lemma test_iInv_4_with_close t N E1 E2 P:
+    ↑N ⊆ E2 →
+    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
+         ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
     iInv N as "(#HP&Hown2)" "Hclose".
@@ -116,10 +139,8 @@ Section iris_tests.
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
-    iInv N with "Hown2" as "(#HP&Hown2)" "Hclose".
-    iMod ("Hclose" with "[HP Hown2]").
-    { iFrame. done. }
-    iModIntro. iFrame. by iNext.
+    iInv N with "Hown2" as "(#HP&Hown2)".
+    iModIntro. iSplitL "Hown2"; auto with iFrame.
   Qed.
 
   Lemma test_iInv_6 t N E1 E2 P:
@@ -128,10 +149,8 @@ Section iris_tests.
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
-    iInv N with "Hown1" as "(#HP&Hown1)" "Hclose".
-    iMod ("Hclose" with "[HP Hown1]").
-    { iFrame. done. }
-    iModIntro. iFrame. by iNext.
+    iInv N with "Hown1" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
   Qed.
 
   (* test robustness in presence of other invariants *)
@@ -141,18 +160,15 @@ Section iris_tests.
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&#?&#?&Hown1&Hown2)".
-    iInv N3 with "Hown1" as "(#HP&Hown1)" "Hclose".
-    iMod ("Hclose" with "[HP Hown1]").
-    { iFrame. done. }
-    iModIntro. iFrame. by iNext.
+    iInv N3 with "Hown1" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
   Qed.
 
   (* iInv should work even where we have "inv N P" in which P contains an evar *)
   Lemma test_iInv_8 N : ∃ P, inv N P ={⊤}=∗ P ≡ True ∧ inv N P.
   Proof.
     eexists. iIntros "#H".
-    iInv N as "HP" "Hclose".
-    iMod ("Hclose" with "[$HP]"). auto.
+    iInv N as "HP". iFrame "HP". auto.
   Qed.
 
   (* test selection by hypothesis name instead of namespace *)
@@ -162,9 +178,8 @@ Section iris_tests.
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
-    iInv "HInv" with "Hown1" as "(#HP&Hown1)" "Hclose".
-    iMod ("Hclose" with "[$HP $Hown1]").
-    iModIntro. iFrame. by iNext.
+    iInv "HInv" with "Hown1" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
   Qed.
 
   (* test selection by hypothesis name instead of namespace *)
@@ -174,27 +189,24 @@ Section iris_tests.
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
-    iInv "HInv" as "(#HP&Hown1)" "Hclose".
-    iMod ("Hclose" with "[$HP $Hown1]").
-    iModIntro. iFrame. by iNext.
+    iInv "HInv" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
   Qed.
 
   (* test selection by ident name *)
   Lemma test_iInv_11 N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
   Proof.
     let H := iFresh in
-    (iIntros H; iInv H as "#H2" "Hclose").
-    iMod ("Hclose" with "H2").
-    iModIntro. by iNext.
+    (iIntros H; iInv H as "#H2"). auto.
   Qed.
 
   (* error messages *)
   Lemma test_iInv_12 N P: inv N (<pers> P) ={⊤}=∗ True.
   Proof.
     iIntros "H".
-    Fail iInv 34 as "#H2" "Hclose".
-    Fail iInv nroot as "#H2" "Hclose".
-    Fail iInv "H2" as "#H2" "Hclose".
+    Fail iInv 34 as "#H2".
+    Fail iInv nroot as "#H2".
+    Fail iInv "H2" as "#H2".
     done.
   Qed.
 
@@ -202,9 +214,7 @@ Section iris_tests.
   Lemma test_iInv_13 N:
     inv N (∃ (v1 v2 v3 : nat), emp ∗ emp ∗ emp) ={⊤}=∗ ▷ emp.
   Proof.
-    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)" "Hclose".
-    iMod ("Hclose" with "[]").
-    { iNext; iExists O; done. }
-    iModIntro. by iNext.
+    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
+    eauto.
   Qed.
 End iris_tests.