diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index a02d41a26e24d92ad1addabf3810fa86196e77a0..84303024140d4c597236fbe52ea0ac3b9dc96cdf 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -310,5 +310,5 @@ Proof.
   iMod (gen_heap_init ∅) as (gen_heap) "Hinterp". iExists gen_heap.
   iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
   { apply map_disjoint_empty_r. }
-  rewrite right_id. done.
+  rewrite right_id_L. done.
 Qed.