From d7ee99a2d73a83fe02d49c0faa53d12894486a78 Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Tue, 26 Nov 2019 19:43:42 +0100
Subject: add elt_eq_unit

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

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index f6bd7d1460..5aea97dd6b 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -199,6 +199,14 @@ Section Facts.
     apply app_cons_not_nil in H1 as [].
   Qed.
 
+  Lemma elt_eq_unit : forall l1 l2 (a b : A),
+    l1 ++ a :: l2 = [b] -> a = b /\ l1 = [] /\ l2 = [].
+  Proof.
+    intros l1 l2 a b Heq.
+    apply app_eq_unit in Heq.
+    now destruct Heq as [[Heq1 Heq2]|[Heq1 Heq2]]; inversion_clear Heq2.
+  Qed.
+
   Lemma app_inj_tail :
     forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b.
   Proof.
-- 
cgit v1.2.3