diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index aaaae3bf81eb93b531e8e82df622f51f35b09ef5..94789d0f170aae332f9cb5d943199f37f5cbdf24 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -67,7 +67,7 @@ Canonical Structure namespace_mapC :=
 
 Global Instance NamespaceMap_discrete a b :
   Discrete a → Discrete b → Discrete (NamespaceMap a b).
-Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
+Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete. Qed.
 Global Instance namespace_map_ofe_discrete :
   OfeDiscrete A → OfeDiscrete namespace_mapC.
 Proof. intros ? [??]; apply _. Qed.