diff --git a/theories/list.v b/theories/list.v
index abadc41fa605caaab5dddaec759e33b9501ed4cb..190233099a28010207eed0a8b22ea964317777fb 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3100,7 +3100,7 @@ Section fmap.
     (∀ x, f x ≡ g x) → f <$> l ≡ g <$> l.
   Proof. induction l; constructor; auto. Qed.
 
-  Global Instance: Inj (=) (=) f → Inj (=) (=) (fmap f).
+  Global Instance fmap_inj: Inj (=) (=) f → Inj (=) (=) (fmap f).
   Proof.
     intros ? l1. induction l1 as [|x l1 IH]; [by intros [|??]|].
     intros [|??]; intros; f_equal/=; simplify_eq; auto.