From 09dc9e0d7c1ec3c6193818c54c22fe88b39e43cf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Jul 2019 14:36:36 +0200
Subject: [PATCH] more consistent lemma names

---
 theories/list.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index bcf2a282..8b33a412 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -913,11 +913,11 @@ Section find.
   Proof.
     induction l as [|x l IH]; [done|]. simpl.
     case_decide; [done|].
-    change (list_fmap B A f l) with (f <$> l). (* FIXME it simplified too much *)
+    change (list_fmap B A f l) with (f <$> l). (* induction didn't re-fold *)
     rewrite IH. by destruct (list_find (P ∘ f) l).
   Qed.
 
-  Lemma list_find_proper (Q : A → Prop) `{∀ x, Decision (Q x)} l :
+  Lemma list_find_ext (Q : A → Prop) `{∀ x, Decision (Q x)} l :
     (∀ x, P x ↔ Q x) →
     list_find P l = list_find Q l.
   Proof.
-- 
GitLab