From f2e42b1d902765f1ebacd410cc21b67ebfadcc6d Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Wed, 30 Oct 2019 22:34:27 +0100
Subject: integration of statements for rev

---
 theories/Lists/List.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 1478ea4f54..d0b4f61587 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -764,6 +764,12 @@ Section ListOps.
     rewrite IHl; auto.
   Qed.
 
+  Lemma rev_eq_app : forall l l1 l2, rev l = l1 ++ l2 -> l = rev l2 ++ rev l1.
+  Proof.
+    intros l l1 l2 Heq.
+    rewrite <- (rev_involutive l), Heq.
+    apply rev_app_distr.
+  Qed.
 
   (** Compatibility with other operations *)
 
-- 
cgit v1.2.3