diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 211b5c063b1fbc5e904c0191355c66fd0e4e251f..1d4c4d38de24f7675fcd4ae0d2a87bc16c92bfb8 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -207,6 +207,13 @@ Proof.
   by move=> /agree_op_invN->; rewrite agree_idemp.
 Qed.
 
+Lemma to_agree_includedN n a b : to_agree a ≼{n}to_agree b ↔ a ≡{n}≡ b.
+Proof.
+  split; last by intros ->.
+  intros (x & Heq). destruct Heq as [_ Hincl].
+  by destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+.
+Qed.
+
 Lemma to_agree_included a b : to_agree a ≼ to_agree b ↔ a ≡ b.
 Proof.
   split; last by intros ->.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 0f7132fb1e7639bfde74da68cd380e6f6c396e9b..fd2d17e9afdf808b7d6bb69fc90f327d254514c0 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -385,11 +385,19 @@ Proof.
   exact: cmra_update_op_l.
 Qed.
 
-Lemma auth_update_core_id a b `{!CoreId b} :
-  b ≼ a → ● a ~~> ● a ⋅ ◯ b.
+Lemma auth_update_core_id q a b `{!CoreId b} :
+  b ≼ a → ●{q} a ~~> ●{q} a ⋅ ◯ b.
 Proof.
-  intros Hincl. apply: auth_update_alloc.
-  rewrite -(left_id ε _ b). apply: core_id_local_update. done.
+  intros Heq%core_id_extract; last done. apply cmra_total_update.
+  move=> n [[[q' ag]|] bf1] [/= VL [a0 [Eq [[bf2 Ha] VL2]]]]; do 2 red; simpl in *.
+  + split; first done.
+    exists a0. split; last split; try done. exists bf2.
+    assert (a ≡{n}≡ a0) as Eq2. { apply to_agree_includedN. exists ag. done. }
+    by rewrite left_id -Eq2 -assoc -comm Heq Eq2 Ha left_id.
+  + split; first done. exists a0.
+    split; first done. split; last done. exists bf2.
+    apply (inj to_agree) in Eq.
+    by rewrite left_id -Eq -assoc -comm Heq Eq Ha left_id.
 Qed.
 
 Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε) → ● a ⋅ ◯ b ~~> ● a'.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 93f185ff38674f14528be5db66c23f3301b8981a..78cf251331231b7d58a43e823bef4c9f58e56822 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -59,14 +59,6 @@ Section updates.
     destruct mz as [z|]; [|done]. by destruct (id_freeN_r n n x z).
   Qed.
 
-  Lemma core_id_local_update x y z `{!CoreId y} :
-    y ≼ x → (x, z) ~l~> (x, z ⋅ y).
-  Proof.
-    intros Hincl n mf ? Heq; simpl in *; split; first done.
-    rewrite [x]core_id_extract // Heq. destruct mf as [f|]; last done.
-    simpl. rewrite -assoc [f â‹… y]comm assoc //.
-  Qed.
-
   Lemma local_update_discrete `{!CmraDiscrete A} (x y x' y' : A) :
     (x,y) ~l~> (x',y') ↔ ∀ mz, ✓ x → x ≡ y ⋅? mz → ✓ x' ∧ x' ≡ y' ⋅? mz.
   Proof.