diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 320f987aaaeee03cdd38b0a019e611ecedacbe8f..c5359862842f2ba3b766d572e1e9e617f63afc73 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -278,10 +278,10 @@ Section auth.
     exact: cmra_update_op_l.
   Qed.
 
-  Lemma auth_update_core_id q a b `{!CoreId b} :
+  Lemma auth_update_frac_alloc q a b `{!CoreId b} :
     b ≼ a → ●{q} a ~~> ●{q} a ⋅ ◯ b.
   Proof.
-    intros Ha%(core_id_extract _ _). apply view_update_alloc_frac=> n bf [??].
+    intros Ha%(core_id_extract _ _). apply view_update_frac_alloc=> n bf [??].
     split; [|done]. rewrite Ha (comm _ a). by apply cmra_monoN_l.
   Qed.
 
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index e0411c7fe138cab8a3b1db969fb46c40d647002d..94fe19030f2bdd6e054bad505417a068e2ce1be2 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -525,7 +525,7 @@ Section cmra.
     rewrite !cmra_total_update view_validN_eq=> ?? n [[[q ag]|] bf]; naive_solver.
   Qed.
 
-  Lemma view_update_alloc_frac q a b :
+  Lemma view_update_frac_alloc q a b :
     (∀ n bf, rel n a bf → rel n a (b ⋅ bf)) →
     ●V{q} a ~~> ●V{q} a ⋅ ◯V b.
   Proof.