diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index b9ba2d8a4434f4d7dd70005e90b9891d3a19e106..f836b8aef9368da518ca9b820956c79c5368d5be 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -116,7 +116,8 @@ Lemma fupd_plain_soundness_no_lc `{!invGpreS Σ} E1 E2 (P: iProp Σ) `{!Plain P}
   (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, ⊢ |={E1,E2}=> P) → ⊢ P.
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hw) "[Hw HE]".
-  iMod (lc_alloc 0) as (Hc) "[_ _]".
+  (* We don't actually want any credits, but we need the [lcGS]. *)
+  iMod (later_credits.le_upd.lc_alloc 0) as (Hc) "[_ _]".
   set (Hi := InvG _ Hw Hc false).
   iAssert (|={⊤,E2}=> P)%I as "H".
   { iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd. by constructor. }
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index e587a1448e3f01fe83e9ef256e72042ef471025c..acd0190cfc8c6f8777034ec77f3ee2f7a40f6772 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -345,7 +345,7 @@ Module le_upd.
 
   (** You probably do NOT want to use this lemma; use [lc_soundness] if you want
   to actually use [le_upd]! *)
-  Lemma lc_alloc `{!lcGpreS Σ} n :
+  Local Lemma lc_alloc `{!lcGpreS Σ} n :
     ⊢ |==> ∃ _ : lcGS Σ, lc_supply n ∗ £ n.
   Proof.
     rewrite lc_unseal /lc_def lc_supply_unseal /lc_supply_def.