diff --git a/iris_heap_lang/metatheory.v b/iris_heap_lang/metatheory.v
index a45b2faa608514d630e45898851192030005e3fa..728d4debd48d7c448a0307c97430d6f0ae959619 100644
--- a/iris_heap_lang/metatheory.v
+++ b/iris_heap_lang/metatheory.v
@@ -190,7 +190,7 @@ Qed.
 
 Lemma subst_map_empty e : subst_map ∅ e = e.
 Proof.
-  assert (∀ x, binder_delete x (∅:gmap _ val) = ∅) as Hdel.
+  assert (∀ x, binder_delete x (∅:gmap string val) = ∅) as Hdel.
   { intros [|x]; by rewrite /= ?delete_empty. }
   induction e; simplify_map_eq; rewrite ?Hdel; auto with f_equal.
 Qed.