make an internal lemma local

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. }

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.