From 14e69a411768d60ce365547c1ffd88d9bef3cdc0 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 6 Jul 2022 14:21:03 +0200
Subject: [PATCH 1/1] update in ground

+ one more lemma with list_append
---
 .../contribs/lambdadelta/ground/lib/list_rcons.ma      | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index bfbc0e986..7d67f5526 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -86,3 +86,13 @@ lemma list_ind_rcons (A) (Q:predicate …):
 @pull_2 #l2 elim l2 -l2 //
 #a2 #l2 #IH0 #l1 #IH /3 width=1 by/
 qed-.
+
+(* Advanced inversions with list_append *************************************)
+
+lemma eq_inv_list_append_dx_dx_refl (A) (l1) (l2):
+      l1 = l2⨁{A}l1 → ⓔ = l2.
+#A #l1 @(list_ind_rcons … l1) -l1 [ // ]
+#l1 #a1 #IH #l2 <list_append_rcons_dx #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
+/2 width=1 by/
+qed-.
-- 
2.39.2