X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Flist_append.ma;h=05fefceb30a13e1f9fcbd5727f728b7ce11ec1b9;hb=2e4a7c54ef77c10cb1cef4b59518c473245ea935;hp=13c68a33cb38843ec0f184012af2d3a4a803eac8;hpb=12dc655b7f5321b33b93a310d53e23e60e090caa;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
index 13c68a33c..05fefceb3 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
@@ -56,3 +56,14 @@ lemma list_append_assoc (A):
   ]
 ]
 qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_list_empty_append (A):
+      ∀l1,l2. ⓔ = l1⨁{A}l2 →
+      ∧∧ ⓔ = l1 & ⓔ = l2.
+#A *
+[ #l2 /2 width=1 by conj/
+| #a1 #l1 #l2 <list_append_lcons_sn #H destruct
+]
+qed-.