From 2e67e68f202872e9ffbfcf8b6593e0242da036bf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 23 May 2016 00:57:34 +0200
Subject: [PATCH] Make some names more consistent.

---
 theories/list.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/list.v b/theories/list.v
index 4d3554d0..5c66a5bf 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.
-- 
GitLab