diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index e28c9ac2a34a9aa72da7bdbb8dd2451efce20999..4329266a730ef82f9bee5db3e3b1bf8a9825489b 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -774,8 +774,12 @@ Tactic Notation "iSplitR" := iSplitL "".
 Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
   eapply tac_and_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [env_reflexivity || fail "iAndDestruct:" H "not found"
-    |apply _ ||
-     let P := match goal with |- IntoSep _ ?P _ _ => P end in
+    |env_cbv; apply _ ||
+     let P :=
+       lazymatch goal with
+       | |- IntoSep ?P _ _ => P
+       | |- IntoAnd _ ?P _ _ => P
+       end in
      fail "iAndDestruct: cannot destruct" P
     |env_reflexivity || fail "iAndDestruct:" H1 "or" H2 " not fresh"|].