diff --git a/iris_heap_lang/metatheory.v b/iris_heap_lang/metatheory.v
index 06738d24b97df0656fce5f247595c73ce1b92921..8f97184538f306f8972b3c3868a1e385a2362473 100644
--- a/iris_heap_lang/metatheory.v
+++ b/iris_heap_lang/metatheory.v
@@ -247,7 +247,7 @@ Proof.
     x ∈ x2 :b: x1 :b: X →
     binder_delete x1 (binder_delete x2 vs) !! x = None).
   { intros x x1 x2 X vs ??. rewrite !lookup_binder_delete_None. set_solver. }
-  induction e=> X vs /= ? HX.
+  induction e as [| |f x e IHe | | | | | | | | | | | | | | | | | | | |]=> X vs /= ? HX.
   3:{ f_equal. eapply IHe; eauto.
       intros x0 Hx0.
       rewrite !lookup_binder_delete_None.