diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 523c5c22748811fd0158e93bcb4c567f24457b4c..660d2c30ef15a5bf0d587d990402172e8523f92d 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -265,7 +265,7 @@ Section gen_heap.
     rewrite !dom_insert_L. set_solver.
   Qed.
 
-  Lemma gen_heap_alloc_gen σ σ' :
+  Lemma gen_heap_alloc_big σ σ' :
     σ' ##ₘ σ →
     gen_heap_interp σ ==∗
     gen_heap_interp (σ' ∪ σ) ∗ ([∗ map] l ↦ v ∈ σ', l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ', meta_token l ⊤).