diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 135109503edf3d86146a133ca6e1f6c1bfc97065..76e318500dba8e7f85ccb43101656703a54d8df3 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -186,6 +186,15 @@ Global Instance add_modal_fupd `{!BiFUpd PROP} E1 E2 P Q :
   AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
 Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 
+Global Instance elim_acc_bupd `{!BiBUpd PROP} {X} α β mγ Q :
+  ElimAcc (X:=X) True bupd bupd α β mγ
+          (|==> Q)
+          (λ x, |==> β x ∗ (mγ x -∗? |==> Q))%I.
+Proof.
+  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.
 Global Instance elim_acc_fupd `{!BiFUpd PROP} {X} E1 E2 E α β mγ Q :
   ElimAcc (X:=X) True (fupd E1 E2) (fupd E2 E1) α β mγ
           (|={E1,E}=> Q)
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 6fdc67828687d48a4192416d8061caa820dda72e..9d375bbb0fa420d83a0e27d25bbbfa97e24c9da4 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -547,8 +547,6 @@ Global Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
    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} {X : Type} (φ : Prop)
       (Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index b0ce4dcf09b57832864d2a3d4a75ace04d1a8ffa..42e4e4c3109ebe06e22edf31c9e1e66156826f17 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -3136,7 +3136,7 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
 (* Without closing view shift *)
 Tactic Notation "iInvCore" constr(N) "with" constr(pats) "in" tactic3(tac) :=
   iInvCore N with pats as (@None string) in ltac:(tac).
-(* Without pattern *)
+(* Without selection pattern *)
 Tactic Notation "iInvCore" constr(N) "as" constr(Hclose) "in" tactic3(tac) :=
   iInvCore N with "[$]" as Hclose in ltac:(tac).
 (* Without both *)
@@ -3287,7 +3287,7 @@ Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(
                 | _ => revert x; intros x1; iDestructHyp H as (   x2 x3 x4 x5 x6 x7 x8 x9 x10) pat
                 end).
 
-(* Without pattern *)
+(* Without selection pattern *)
 Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
   iInvCore N as (Some Hclose) in
     (fun x H => lazymatch type of x with
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 375b0c82791168584a7bd2632f2e0b8795ea41b7..56243f168e05f00ba018d58b1414e190940b8cfb 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -134,6 +134,18 @@ The command has indeed failed with message:
 Tactic failure: iInv: invariant nroot not found.
 The command has indeed failed with message:
 Tactic failure: iInv: invariant "H2" not found.
+"test_iInv_accessor_variable"
+     : string
+The command has indeed failed with message:
+Tactic failure: Missing intro pattern for accessor variable.
+The command has indeed failed with message:
+The command has not failed!
+The command has indeed failed with message:
+Tactic failure: iExistDestruct: cannot destruct (Φ H1).
+The command has indeed failed with message:
+Tactic failure: Missing intro pattern for accessor variable.
+The command has indeed failed with message:
+Tactic failure: Missing intro pattern for accessor variable.
 "test_frac_split_combine"
      : string
 1 goal
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 93b0b1a7510861ec34dbaa4d2ec378c9c269b624..a751684b0f41a9a9690391f2cfde72e8b0d07f07 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -5,6 +5,7 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva
 From iris.prelude Require Import options.
 
 Unset Mangle Names.
+Set Default Proof Using "Type*".
 
 Section base_logic_tests.
   Context {M : ucmra}.
@@ -233,6 +234,37 @@ Section iris_tests.
     eauto.
   Qed.
 
+  (* Test [iInv] with accessor variables. *)
+  Section iInv_accessor_variables.
+    (** We consider a kind of invariant that does not take a proposition, but
+    a predicate. The invariant accessor gives the predicate existentially. *)
+    Context (INV : (bool → iProp Σ) → iProp Σ).
+    Context `{!∀ Φ,
+      IntoAcc (INV Φ) True True (fupd ⊤ ∅) (fupd ∅ ⊤) Φ Φ (λ b, Some (INV Φ))}.
+
+    Check "test_iInv_accessor_variable".
+    Lemma test_iInv_accessor_variable Φ : INV Φ ={⊤}=∗ INV Φ.
+    Proof.
+      iIntros "HINV".
+      (* There are 4 variants of [iInv] that we have to test *)
+      (* No selection pattern, no closing view shift *)
+      Fail iInv "HINV" as "HINVinner".
+      iInv "HINV" as (b) "HINVinner"; rename b into b_exists. Undo.
+      (* Both sel.pattern and closing view shift *)
+      (* FIXME this one is broken: no proper error message without a pattern for
+      the accessor variable, and an error when the pattern is given *)
+      Fail Fail iInv "HINV" with "[//]" as "HINVinner" "Hclose".
+      Fail iInv "HINV" with "[//]" as (b) "HINVinner" "Hclose"; rename b into b_exists.
+      (* Sel.pattern but no closing view shift *)
+      Fail iInv "HINV" with "[//]" as "HINVinner".
+      iInv "HINV" with "[//]" as (b) "HINVinner"; rename b into b_exists. Undo.
+      (* Closing view shift, no selection pattern *)
+      Fail iInv "HINV" as "HINVinner" "Hclose".
+      iInv "HINV" as (b) "HINVinner" "Hclose"; rename b into b_exists.
+      by iApply "Hclose".
+    Qed.
+  End iInv_accessor_variables.
+
   Theorem test_iApply_inG `{!inG Σ A} γ (x x' : A) :
     x' ≼ x →
     own γ x -∗ own γ x'.