diff --git a/CHANGELOG.md b/CHANGELOG.md
index 331ee0ee9fcace983a36ce5babcf75fc958afda7..c24bc79f4545224473dc0aea9bdb3067458c2d9c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,18 @@ way the logic is used on paper.  We also document changes in the Coq
 development; every API-breaking change should be listed, but not every new
 lemma.
 
+## Iris master
+
+**Changes in `proofmode`:**
+
+* The proofmode now preserves user-supplied names for existentials when using
+  `iDestruct ... as (?) "..."`. This is backwards-incompatible if you were
+  relying on the previous automatic names (which were always "H", possibly
+  freshened). It also requires some changes if you were implementing `IntoExist`
+  yourself, since the typeclass now forwards names. If your instance transforms
+  one `IntoExist` into another, you can generally just forward the name from the
+  premise.
+
 ## Iris 3.3.0 (released 2020-07-15)
 
 This release does not have any outstanding highlights, but contains a large
diff --git a/_CoqProject b/_CoqProject
index 7e5bfbc2686f17443245972fdabce37a17677d77..62919d7368992eee5bcbf4b45d7141b43ee87ae9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -127,6 +127,7 @@ theories/heap_lang/lib/diverge.v
 theories/heap_lang/lib/arith.v
 theories/heap_lang/lib/array.v
 theories/proofmode/base.v
+theories/proofmode/ident_name.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
 theories/proofmode/ltac_tactics.v
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index fa843801d94788852473772ecd007a6f30868634..0a20cfd6c0b2bdb1721985269828dc59d4653c09 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -77,6 +77,23 @@
   --------------------------------------∗
   Q
   
+"test_iDestruct_exists_not_exists"
+     : string
+The command has indeed failed with message:
+Tactic failure: iExistDestruct: cannot destruct P.
+"test_iDestruct_exists_intuitionistic"
+     : string
+1 subgoal
+  
+  PROP : bi
+  P : PROP
+  Φ : nat → PROP
+  y : nat
+  ============================
+  "H" : Φ y ∧ P
+  --------------------------------------â–¡
+  P
+  
 "test_iIntros_forall_pure"
      : string
 1 subgoal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index b6a70a42100bd1234c3478b5700579e1d282863b..fb17541b694ece2405c436bf7017d058ea369025 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -112,6 +112,85 @@ Qed.
 Lemma test_iDestruct_spatial_noop Q : Q -∗ Q.
 Proof. iIntros "-#HQ". done. Qed.
 
+Lemma test_iDestruct_exists (Φ: nat → PROP) :
+  (∃ y, Φ y) -∗ ∃ n, Φ n.
+Proof. iIntros "H". iDestruct "H" as (y) "H". by iExists y. Qed.
+
+Lemma test_iDestruct_exists_automatic (Φ: nat → PROP) :
+  (∃ y, Φ y) -∗ ∃ n, Φ n.
+Proof.
+  iIntros "H".
+  iDestruct "H" as (?) "H".
+  (* the automatic name should by [y] *)
+  by iExists y.
+Qed.
+
+Lemma test_iDestruct_exists_automatic_multiple (Φ: nat → PROP) :
+  (∃ y n baz, Φ (y+n+baz)) -∗ ∃ n, Φ n.
+Proof. iDestruct 1 as (???) "H". by iExists (y+n+baz). Qed.
+
+Lemma test_iDestruct_exists_freshen (y:nat) (Φ: nat → PROP) :
+  (∃ y, Φ y) -∗ ∃ n, Φ n.
+Proof.
+  iIntros "H".
+  iDestruct "H" as (?) "H".
+  (* the automatic name is the freshened form of [y] *)
+  by iExists y0.
+Qed.
+
+Check "test_iDestruct_exists_not_exists".
+Lemma test_iDestruct_exists_not_exists P :
+  P -∗ P.
+Proof. Fail iDestruct 1 as (?) "H". Abort.
+
+Lemma test_iDestruct_exists_explicit_name (Φ: nat → PROP) :
+  (∃ y, Φ y) -∗ ∃ n, Φ n.
+Proof.
+  (* give an explicit name that isn't the binder name *)
+  iDestruct 1 as (foo) "?".
+  by iExists foo.
+Qed.
+
+Lemma test_iDestruct_exists_pure (Φ: nat → Prop) :
+  ⌜∃ y, Φ y⌝ ⊢@{PROP} ∃ n, ⌜Φ n⌝.
+Proof.
+  iDestruct 1 as (?) "H".
+  by iExists y.
+Qed.
+
+Lemma test_iDestruct_exists_and_pure (H: True) P :
+  ⌜False⌝ ∧ P -∗ False.
+Proof.
+  (* this automatic name uses [fresh H] as a sensible default (it's a hypothesis
+  in [Prop] and the user cannot supply a name in their code) *)
+  iDestruct 1 as (?) "H".
+  contradict H0.
+Qed.
+
+Check "test_iDestruct_exists_intuitionistic".
+Lemma test_iDestruct_exists_intuitionistic P (Φ: nat → PROP) :
+  □ (∃ y, Φ y ∧ P) -∗ P.
+Proof.
+  iDestruct 1 as (?) "#H". Show.
+  iDestruct "H" as "[_ $]".
+Qed.
+
+Lemma test_iDestruct_exists_freshen_local_name (Φ: nat → PROP) :
+  let y := 0 in
+  □ (∃ y, Φ y) -∗ ∃ n, Φ (y+n).
+Proof.
+  iIntros (y) "#H".
+  iDestruct "H" as (?) "H".
+  iExists y0; auto.
+Qed.
+
+Definition an_exists P : PROP := (∃ (an_exists_name:nat), ▷^an_exists_name P)%I.
+
+(* should use the name from within [an_exists] *)
+Lemma test_iDestruct_exists_automatic_def P :
+  an_exists P -∗ ∃ k, ▷^k P.
+Proof. iDestruct 1 as (?) "H". by iExists an_exists_name. Qed.
+
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → ⊢ ⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P.
 Proof. iIntros (??) "H". auto. Qed.
 
diff --git a/tests/telescopes.v b/tests/telescopes.v
index 664ff6a1d3a4a67892456b597e20f2155b13064b..10807e8566d4d55068802886a6f008481f53ebf0 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -21,6 +21,9 @@ Section basic_tests.
   Lemma test_iAssumption_tforall {TT : tele} (Φ : TT → PROP) :
     (∀.. x, Φ x) -∗ ∀.. x, Φ x.
   Proof. iIntros "H" (x). iAssumption. Qed.
+  Lemma test_exist_texist_auto_name {TT : tele} (Φ : TT → PROP) :
+    (∃.. y, Φ y) -∗ ∃.. x, Φ x.
+  Proof. iDestruct 1 as (?) "H". by iExists y. Qed.
   Lemma test_pure_texist {TT : tele} (φ : TT → Prop) :
     (∃.. x, ⌜ φ x ⌝) -∗ ∃.. x, ⌜ φ x ⌝ : PROP.
   Proof. iIntros (H) "!%". done. Qed.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index e3e88c265dee97f73af548b8d574c4d0e5c36f99..b5e8251e14760492ea89f9ddc374b5751ab09577 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -784,38 +784,49 @@ Global Instance from_exist_persistently {A} P (Φ : A → PROP) :
 Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
 
 (** IntoExist *)
-Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ.
+
+(* These three instances [into_exist_exist], [into_exist_pure], and
+   [into_exist_texist] need to be written without notations, for example
+   [bi_exist Φ] and not [∃ a, Φ a], so that [AsIdentName] is always passed the
+   entire body of the exists with the binder. *)
+Global Instance into_exist_exist {A} (Φ : A → PROP) name :
+  AsIdentName Φ name → IntoExist (bi_exist Φ) Φ name.
 Proof. by rewrite /IntoExist. Qed.
-Global Instance into_exist_texist {TT : tele} (Φ : TT → PROP) :
-  IntoExist (∃.. a, Φ a) Φ | 10.
-Proof. by rewrite /IntoExist bi_texist_exist. Qed.
-Global Instance into_exist_pure {A} (φ : A → Prop) :
-  @IntoExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
+Global Instance into_exist_pure {A} (φ : A → Prop) name :
+  AsIdentName φ name →
+  @IntoExist PROP A ⌜ex φ⌝ (λ a, ⌜φ a⌝)%I name.
 Proof. by rewrite /IntoExist pure_exist. Qed.
-Global Instance into_exist_affinely {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (<affine> P) (λ a, <affine> (Φ a))%I.
+Global Instance into_exist_texist {TT : tele} (Φ : TT → PROP) name :
+  AsIdentName Φ name → IntoExist (bi_texist Φ) Φ name | 10.
+Proof. by rewrite /IntoExist bi_texist_exist. Qed.
+Global Instance into_exist_affinely {A} P (Φ : A → PROP) name :
+  IntoExist P Φ name → IntoExist (<affine> P) (λ a, <affine> (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
-Global Instance into_exist_intuitionistically {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
+Global Instance into_exist_intuitionistically {A} P (Φ : A → PROP) name :
+  IntoExist P Φ name → IntoExist (□ P) (λ a, □ (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed.
+(* [to_ident_name H] makes the default name [H] when [P] is introduced with [?] *)
 Global Instance into_exist_and_pure P Q φ :
-  IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).
+  IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q) (to_ident_name H).
 Proof.
   intros (φ'&->&?). rewrite /IntoExist (into_pure P).
   apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
 Qed.
+(* [to_ident_name H] makes the default name [H] when [P] is introduced with [?] *)
 Global Instance into_exist_sep_pure P Q φ :
-  IntoPureT P φ → TCOr (Affine P) (Absorbing Q) → IntoExist (P ∗ Q) (λ _ : φ, Q).
+  IntoPureT P φ →
+  TCOr (Affine P) (Absorbing Q) →
+  IntoExist (P ∗ Q) (λ _ : φ, Q) (to_ident_name H).
 Proof.
   intros (φ'&->&?) ?. rewrite /IntoExist.
   eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
   rewrite -exist_intro //. apply sep_elim_r, _.
 Qed.
-Global Instance into_exist_absorbingly {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (<absorb> P) (λ a, <absorb> (Φ a))%I.
+Global Instance into_exist_absorbingly {A} P (Φ : A → PROP) name :
+  IntoExist P Φ name → IntoExist (<absorb> P) (λ a, <absorb> (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
-Global Instance into_exist_persistently {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (<pers> P) (λ a, <pers> (Φ a))%I.
+Global Instance into_exist_persistently {A} P (Φ : A → PROP) name :
+  IntoExist P Φ name → IntoExist (<pers> P) (λ a, <pers> (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
 
 (** IntoForall *)
diff --git a/theories/proofmode/class_instances_embedding.v b/theories/proofmode/class_instances_embedding.v
index 6e964003e154d4c1c45866ec35ae162d30835dd2..3c02a6d23db124ab5b28bcc44ff78f8e9a52bae4 100644
--- a/theories/proofmode/class_instances_embedding.v
+++ b/theories/proofmode/class_instances_embedding.v
@@ -121,8 +121,8 @@ Global Instance from_exist_embed {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
 Proof. by rewrite /FromExist -embed_exist => <-. Qed.
 
-Global Instance into_exist_embed {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Global Instance into_exist_embed {A} P (Φ : A → PROP) name :
+  IntoExist P Φ name → IntoExist ⎡P⎤ (λ a, ⎡Φ a⎤%I) name.
 Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
 
 Global Instance into_forall_embed {A} P (Φ : A → PROP) :
diff --git a/theories/proofmode/class_instances_later.v b/theories/proofmode/class_instances_later.v
index 7b2271f5b086d612af47399e9375f301d6ff2ad9..3131c3943c7a7e1d305e8a1f13d3c16f2d2fe6d5 100644
--- a/theories/proofmode/class_instances_later.v
+++ b/theories/proofmode/class_instances_later.v
@@ -161,14 +161,14 @@ Global Instance from_exist_except_0 {A} P (Φ : A → PROP) :
 Proof. rewrite /FromExist=> <-. by rewrite except_0_exist_2. Qed.
 
 (** IntoExist *)
-Global Instance into_exist_later {A} P (Φ : A → PROP) :
-  IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
+Global Instance into_exist_later {A} P (Φ : A → PROP) name :
+  IntoExist P Φ name → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
-Global Instance into_exist_laterN {A} n P (Φ : A → PROP) :
-  IntoExist P Φ → Inhabited A → IntoExist (▷^n P) (λ a, ▷^n (Φ a))%I.
+Global Instance into_exist_laterN {A} n P (Φ : A → PROP) name :
+  IntoExist P Φ name → Inhabited A → IntoExist (▷^n P) (λ a, ▷^n (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP ?. by rewrite HP laterN_exist. Qed.
-Global Instance into_exist_except_0 {A} P (Φ : A → PROP) :
-  IntoExist P Φ → Inhabited A → IntoExist (◇ P) (λ a, ◇ (Φ a))%I.
+Global Instance into_exist_except_0 {A} P (Φ : A → PROP) name :
+  IntoExist P Φ name → Inhabited A → IntoExist (◇ P) (λ a, ◇ (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
 
 (** IntoForall *)
diff --git a/theories/proofmode/class_instances_plainly.v b/theories/proofmode/class_instances_plainly.v
index 0559fc027096340b00c6837d18f2bfb4f9a1dc86..27bc8a7b9ffc7fd756e18c7deaf56d1b6abb37d1 100644
--- a/theories/proofmode/class_instances_plainly.v
+++ b/theories/proofmode/class_instances_plainly.v
@@ -75,8 +75,8 @@ Global Instance from_exist_plainly {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (■ P) (λ a, ■ (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
 
-Global Instance into_exist_plainly `{!BiPlainlyExist PROP} {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (■ P) (λ a, ■ (Φ a))%I.
+Global Instance into_exist_plainly `{!BiPlainlyExist PROP} {A} P (Φ : A → PROP) name :
+  IntoExist P Φ name → IntoExist (■ P) (λ a, ■ (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
 
 Global Instance into_forall_plainly {A} P (Φ : A → PROP) :
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 01a9ae7382d77306b80a115f510de73d8f084ded..bee8371ae8886f9a0eab4186154a7ccaa88c5c6e 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -1,7 +1,7 @@
 From stdpp Require Import namespaces.
 From iris.bi Require Export bi.
 From iris.proofmode Require Import base.
-From iris.proofmode Require Export modalities.
+From iris.proofmode Require Export ident_name modalities.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -204,11 +204,11 @@ Arguments FromExist {_ _} _%I _%I : simpl never.
 Arguments from_exist {_ _} _%I _%I {_}.
 Hint Mode FromExist + - ! - : typeclass_instances.
 
-Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
+Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :=
   into_exist : P ⊢ ∃ x, Φ x.
-Arguments IntoExist {_ _} _%I _%I : simpl never.
-Arguments into_exist {_ _} _%I _%I {_}.
-Hint Mode IntoExist + - ! - : typeclass_instances.
+Arguments IntoExist {_ _} _%I _%I _ : simpl never.
+Arguments into_exist {_ _} _%I _%I _ {_}.
+Hint Mode IntoExist + - ! - - : typeclass_instances.
 
 Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
   into_forall : P ⊢ ∀ x, Φ x.
@@ -617,8 +617,8 @@ Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
   IntoOr P Q1 Q2 → IntoOr (tc_opaque P) Q1 Q2 := id.
 Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   FromExist P Φ → FromExist (tc_opaque P) Φ := id.
-Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (tc_opaque P) Φ := id.
+Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :
+  IntoExist P Φ name → IntoExist (tc_opaque P) Φ name := id.
 Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   FromForall P Φ → FromForall (tc_opaque P) Φ := id.
 Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index e0d53b86b6682a71567e753564fab1aecc2089de..751d997a87e2ed7829152c73369d9e879d8e179a 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -726,13 +726,17 @@ Proof.
   rewrite -(from_exist P). eauto using exist_intro'.
 Qed.
 
-Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → PROP) Q :
-  envs_lookup i Δ = Some (p, P) → IntoExist P Φ →
-  (∀ a,
-    match envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ with
-    | Some Δ' => envs_entails Δ' Q
-    | None => False
-    end) →
+Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → PROP) (name: ident_name) Q :
+  envs_lookup i Δ = Some (p, P) → IntoExist P Φ name →
+  ( (* this let binding makes it easy for the tactic [iExistDestruct] to use
+       [name] (from resolving [IntoExist] in an earlier subgoal) within this
+       goal *)
+    let _ := name in
+    ∀ a,
+     match envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ with
+     | Some Δ' => envs_entails Δ' Q
+     | None => False
+     end) →
   envs_entails Δ Q.
 Proof.
   rewrite envs_entails_eq => ?? HΦ. rewrite envs_lookup_sound //.
diff --git a/theories/proofmode/ident_name.v b/theories/proofmode/ident_name.v
new file mode 100644
index 0000000000000000000000000000000000000000..c5886dcb0ab7345bf68c4d1731862c830d9faf2b
--- /dev/null
+++ b/theories/proofmode/ident_name.v
@@ -0,0 +1,36 @@
+From stdpp Require Import base.
+
+(** [ident_name] is a way to remember an identifier within the binder of a
+(trivial) function, which can be constructed and retrieved with Ltac but is easy
+to forward around opaquely in Gallina (through typeclasses, for example) *)
+Definition ident_name := unit → unit.
+
+(** [to_ident_name id] returns a constr of type [ident_name] that holds [id] in
+the binder name *)
+Ltac to_ident_name id :=
+  eval cbv in (ltac:(clear; intros id; assumption) : unit → unit).
+
+(** to_ident_name is a Gallina-level version of [to_ident_name] for constructing
+    [ident_name] literals. *)
+Notation to_ident_name id := (λ id:unit, id) (only parsing).
+
+(** The idea of [AsIdentName] is to convert the binder in [f], which should be a
+    lambda, to an [ident_name] representing the name of the binder. It has only
+    one instance, a [Hint Extern] which implements that conversion to resolve
+    [name] in Ltac (see [solve_as_ident_name]).
+
+    This typeclass can produce the fallback identifier [__unknown] when applied
+    to an identifier rather than a lambda; for example, if the user writes
+    [bi_exist Φ], there is no binder anywhere to extract. *)
+Class AsIdentName {A B} (f : A → B) (name : ident_name) := as_ident_name {}.
+Arguments as_ident_name {A B f} name : assert.
+
+Ltac solve_as_ident_name :=
+  lazymatch goal with
+  | |- AsIdentName (λ x, _) _ =>
+    let name := to_ident_name x in
+    notypeclasses refine (as_ident_name name)
+  | _ => notypeclasses refine (to_ident_name __unknown)
+  end.
+
+Hint Extern 1 (AsIdentName _ _) => solve_as_ident_name : typeclass_instances.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 52eb7fab840597485e6ad544a1c9d74ab8fd6434..4042d85e566161da21b30239fda57732741bb477 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1327,14 +1327,18 @@ Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
 
 Local Tactic Notation "iExistDestruct" constr(H)
     "as" simple_intropattern(x) constr(Hx) :=
-  eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
+  eapply tac_exist_destruct with H _ Hx _ _ _; (* (i:=H) (j:=Hx) *)
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iExistDestruct:" H "not found"
     |iSolveTC ||
-     let P := match goal with |- IntoExist ?P _ => P end in
+     let P := match goal with |- IntoExist ?P _ _ => P end in
      fail "iExistDestruct: cannot destruct" P|];
-    let y := fresh in
+    let name := lazymatch goal with
+                | |- let _ := (λ name, _) in _ => name
+                end in
+    intros _;
+    let y := fresh name in
     intros y; pm_reduce;
     match goal with
     | |- False =>
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 97dfa462f733ea953c1b89190e2f1bd0c129dfe3..22abd18c99fafb0e905186765af1864cea2d383a 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -313,8 +313,8 @@ Proof.
   rewrite /FromExist /MakeMonPredAt=><- H. setoid_rewrite <- H.
   by rewrite monPred_at_exist.
 Qed.
-Global Instance into_exist_monPred_at {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
-  IntoExist P Φ → (∀ a, MakeMonPredAt i (Φ a) (Ψ a)) → IntoExist (P i) Ψ.
+Global Instance into_exist_monPred_at {A} P (Φ : A → monPred) name (Ψ : A → PROP) i :
+  IntoExist P Φ name → (∀ a, MakeMonPredAt i (Φ a) (Ψ a)) → IntoExist (P i) Ψ name.
 Proof.
   rewrite /IntoExist /MakeMonPredAt=>-> H. setoid_rewrite <- H.
   by rewrite monPred_at_exist.
@@ -336,8 +336,11 @@ Global Instance from_exist_monPred_at_ex P (Φ : I → PROP) i :
 Proof.
   rewrite /FromExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
 Qed.
+(* TODO: this implementation uses [idx] as the automatic name for the index. In
+theory a monPred could define an appropriate metavariable for indices with an
+[ident_name] argument to [MakeMonPredAt], but this is not implemented. *)
 Global Instance into_exist_monPred_at_ex P (Φ : I → PROP) i :
-  (∀ i, MakeMonPredAt i P (Φ i)) → IntoExist ((<subj> P) i) Φ.
+  (∀ i, MakeMonPredAt i P (Φ i)) → IntoExist ((<subj> P) i) Φ (to_ident_name idx).
 Proof.
   rewrite /IntoExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
 Qed.