From 5befd5232a6b5d9751230851b9e47c540d8dabd7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Sep 2022 14:45:57 +0200
Subject: [PATCH] Some new lines.

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

diff --git a/stdpp/list.v b/stdpp/list.v
index 9a084b61..68f54f80 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -4528,14 +4528,16 @@ Proof.
   by rewrite (assoc f), (comm f _ b), (assoc f), (comm f b), (comm f _ a2).
 Qed.
 Lemma foldr_cons_permute {A} (R : relation A) `{!PreOrder R}
-    (f : A → A → A) (a : A) `{!∀ a, Proper (R ==> R) (f a), !Assoc R f, !Comm R f} x l :
+    (f : A → A → A) (a : A)
+`{!∀ a, Proper (R ==> R) (f a), !Assoc R f, !Comm R f} x l :
   R (foldr f a (x :: l)) (foldr f (f x a) l).
 Proof.
   rewrite <-foldr_snoc.
   eapply foldr_permutation_proper'; [done..|].
   rewrite Permutation_app_comm. done.
 Qed.
-Lemma foldr_cons_permute_eq {A} (f : A → A → A) (a : A) `{!Assoc (=) f, !Comm (=) f} x l :
+Lemma foldr_cons_permute_eq {A} (f : A → A → A) (a : A)
+    `{!Assoc (=) f, !Comm (=) f} x l :
   foldr f a (x :: l) = foldr f (f x a) l.
 Proof. eapply (foldr_cons_permute eq); apply _. Qed.
 
-- 
GitLab