From 20fc362038aa0e158ca5b43243d34f74a4e0a9bf Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Fri, 3 Dec 2021 17:12:20 +0100
Subject: [PATCH] list_fmap_inj1 -> list_fmap_inj_1

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

diff --git a/theories/list.v b/theories/list.v
index 3d368840..13679892 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3757,7 +3757,7 @@ Section fmap.
     intros [|??]; intros; f_equal/=; simplify_eq; auto.
   Qed.
 
-  Lemma list_fmap_inj1 (f1 f2 : A → B) l x :
+  Lemma list_fmap_inj_1 (f1 f2 : A → B) l x :
     f1 <$> l = f2 <$> l → x ∈ l → f1 x = f2 x.
   Proof. intros Hf Hin. induction Hin; naive_solver. Qed.
 
-- 
GitLab