diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 403a9ed0653aa879e30ea6133ae2134627991dbb..d69bf6f3215ff447a8f6b794518c0cb7c33b04aa 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -51,9 +51,9 @@ Section semtypes.
     interp τ Δ v v' -∗ ⌜val_is_unboxed v ∧ val_is_unboxed v'⌝.
   Proof.
     induction 1; simpl;
-    first [iIntros "[% %]"
+    first [iDestruct 1 as (? ?) "[% [% ?]]"
           |iDestruct 1 as (?) "[% %]"
-          |iDestruct 1 as (? ?) "[% [% ?]]"];
+          |iIntros "[% %]"];
     simplify_eq/=; eauto with iFrame.
   Qed.