From 32edabf7365ec02114727cc368acb53f440fc99a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 14 Oct 2023 18:48:00 +0200
Subject: [PATCH] Break long line.
---
stdpp/list.v | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/stdpp/list.v b/stdpp/list.v
index a3cdba6a..468bc1c8 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -4114,7 +4114,9 @@ Section fmap.
intros ? l1. induction l1; intros [|??]; inversion 1; constructor; auto.
Qed.
Global Instance list_fmap_eq_inj : Inj (=) (=) f → Inj (=@{list A}) (=) (fmap f).
- Proof. intros ?%list_fmap_inj ?? ?%list_eq_Forall2%(inj _). by apply list_eq_Forall2. Qed.
+ Proof.
+ intros ?%list_fmap_inj ?? ?%list_eq_Forall2%(inj _). by apply list_eq_Forall2.
+ Qed.
Global Instance list_fmap_equiv_inj `{!Equiv A, !Equiv B} :
Inj (≡) (≡) f → Inj (≡@{list A}) (≡) (fmap f).
Proof.
--
GitLab