diff --git a/theories/base_logic/lib/gc.v b/theories/base_logic/lib/gc.v
index bea662c03429e51d1530f712e3340c9f73d8a619..801684ea85a5d01e55a30383b5b5c1c429e36b6c 100644
--- a/theories/base_logic/lib/gc.v
+++ b/theories/base_logic/lib/gc.v
@@ -145,7 +145,7 @@ Section gc.
         apply (auth_update_alloc _ (to_gc_map (<[l := (v, I)]> gcm)) (to_gc_map ({[l := (v, I)]}))).
         rewrite to_gc_map_insert to_gc_map_singleton.
         pose proof (to_gc_map_valid gcm).
-        setoid_rewrite alloc_singleton_local_update=>//. }
+        apply: alloc_singleton_local_update; done. }
       iMod ("Hclose" with "[H● HsepM Hl]").
       + iExists _.
         iDestruct (big_sepM_insert with "[HsepM Hl]") as "HsepM"=>//; iFrame.