diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index c35fac89001bc1b86b5afd8788ff50001ddcef30..c4205ca16adb76ebea6cb29b95177f7be4c71816 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -575,7 +575,7 @@ Section cmra_leibniz.
   Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.
 
   (** ** Persistent elements *)
-  Lemma persistent_dup_L x `{!Persistent x} : x ≡ x ⋅ x.
+  Lemma persistent_dup_L x `{!Persistent x} : x = x â‹… x.
   Proof. unfold_leibniz. by apply persistent_dup. Qed.
 
   (** ** Total core *)