diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index e7f1520023d3dff470264abc5dc1ed2c2fdb25c9..b543b9519b6eec966a1a328c3915fcd158d87100 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -118,7 +118,7 @@ Section has_type.
     WP ν @ E {{ Φ }}.
   Proof.
     iIntros "H◁ HΦ". setoid_rewrite has_type_value. unfold has_type.
-    destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]".
+    destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]". simpl.
     iMod ("HΦ" $! v with "[] H◁") as "HΦ". done.
     iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH"
       forall (Φ v EQν); try done.