diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 6764fa796dc3ce52f2580032d37f502e62aa61ff..94c2de629d210d0464db5f293d82d0ce1baf62e6 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1274,6 +1274,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
      Also, rule out cases in which it does not make sense to copy, namely when
      destructing a lemma (instead of a hypothesis) or a spatial hyopthesis
      (which cannot be kept). *)
+     iStartProof;
      lazymatch ident with
      | None => iPoseProofCore lem as p false tac
      | Some ?H =>