diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index 8f0620e034ac5601ee4a51a20d4334e90264c1be..f070ae1d4498d45598770d28e2dfb25b497e801c 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -247,7 +247,7 @@ Lemma slice_iff E q f P Q Q' γ b :
 Proof.
   iIntros (??) "#HQQ' #Hs Hb". destruct b.
   - iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done.
-    iDestruct ("HQQ'" with "HQ") as "HQ'".
+    iPoseProof ("HQQ'" with "HQ") as "HQ'".
     iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
     iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
     iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 47127e687024fd9ad9da4d2e00340d944ac6c1c7..43465aca848c2100f48774241d1b2430b17ad033 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1992,6 +1992,12 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
   iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with tac.
 
 (** * Destruct tactic *)
+
+(** [CopyDestruct] is an internal class used by the [iDestruct] tactic to
+identify universally quantified hypotheses that should be copied and not be
+consumed when they are specialized in proofmode terms.
+
+Not intended for user extensibility. *)
 Class CopyDestruct {PROP : bi} (P : PROP).
 Arguments CopyDestruct {_} _%I.
 Hint Mode CopyDestruct + ! : typeclass_instances.
@@ -2013,8 +2019,8 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=
     | string => constr:(Some (INamed lem))
     | iTrm =>
        lazymatch lem with
-       | @iTrm ident ?H _ _ => constr:(Some H)
-       | @iTrm string ?H _ _ => constr:(Some (INamed H))
+       | @ITrm ident _ _?H _ _ => constr:(Some H)
+       | @ITrm string _ _ ?H _ _ => constr:(Some (INamed H))
        | _ => constr:(@None ident)
        end
     | _ => constr:(@None ident)
diff --git a/tests/proofmode.v b/tests/proofmode.v
index ef03c12c62b126ee37d59b23a0af8adf99c3c67b..d41770c4711a12bc2e4ecd0344e626f2c5b2353f 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -93,6 +93,32 @@ Lemma test_iDestruct_intuitionistic_2 P Q `{!Persistent P, !Affine P}:
   Q ∗ (Q -∗ P) -∗ P.
 Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". done. Qed.
 
+Lemma test_iDestruct_specialize_wand P Q :
+  Q ∗ □(Q -∗ P) -∗ P.
+Proof.
+  iIntros "[HQ #HQP]".
+  (* iDestruct specializes, consuming the hypothesis *)
+  iDestruct ("HQP" with "HQ") as "HQP". done.
+Qed.
+
+Lemma test_iPoseProof_copy_wand P Q :
+  Q ∗ □(Q -∗ P) -∗ P ∗ (Q -∗ P).
+Proof.
+  iIntros "[HQ #HQP]".
+  (* in contrast with [iDestruct], [iPoseProof] leaves "HQP" alone *)
+  iPoseProof ("HQP" with "HQ") as "HP".
+  iFrame "HP HQP".
+Qed.
+
+Lemma test_iDestruct_pose_forall (Φ: nat → PROP) :
+  □(∀ (x:nat), Φ x) -∗ Φ 0 ∗ Φ 1.
+Proof.
+  iIntros "#H".
+  (* iDestruct does not consume "H" because it's a [∀] *)
+  iDestruct ("H" $! 0) as "$".
+  iDestruct ("H" $! 1) as "$".
+Qed.
+
 Lemma test_iDestruct_intuitionistic_affine_bi `{!BiAffine PROP} P Q `{!Persistent P}:
   Q ∗ (Q -∗ P) -∗ P ∗ Q.
 Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.