diff --git a/algebra/cmra.v b/algebra/cmra.v
index af75e124f405bae52e42d228bca99e2fc4ef6e00..7a25c150fd0ed055b59c9b3e57539e9260dcdf5b 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -344,6 +344,8 @@ Section unit.
   Proof. by intros x; rewrite (comm op) left_id. Qed.
   Global Instance cmra_unit_persistent : Persistent ∅.
   Proof. by rewrite /Persistent -{2}(cmra_core_l ∅) right_id. Qed.
+  Lemma cmra_core_unit : core (∅:A) ≡ ∅.
+  Proof. by rewrite -{2}(cmra_core_l ∅) right_id. Qed.
 End unit.
 
 (** ** Local updates *)