diff --git a/theories/list.v b/theories/list.v
index 4d3554d0aad7d6591fc483e365567484717dbf6a..5c66a5bfa14e949e9b8c89ddd435d655ff70b7ad 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2684,7 +2684,7 @@ Section setoid.
 
   Lemma equiv_Forall2 l k : l ≡ k ↔ Forall2 (≡) l k.
   Proof. split; induction 1; constructor; auto. Qed.
-  Lemma equiv_lookup l k : l ≡ k ↔ (∀ i, l !! i ≡ k !! i).
+  Lemma list_equiv_lookup l k : l ≡ k ↔ ∀ i, l !! i ≡ k !! i.
   Proof.
     rewrite equiv_Forall2, Forall2_lookup.
     by setoid_rewrite equiv_option_Forall2.