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=e4c3d743e2d17273430c19d9672a86fe3bd7a70c;hb=8f1a123e61ff079b1f9ad63cc915470ec7e6abf3;hp=042497aac144f4549933ebc96f4afc615c50218b;hpb=d43c110267c05246b638e7f944e065820d5c1197;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 042497aac..e4c3d743e 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
@@ -68,6 +68,15 @@ lemma eq_inv_list_empty_append (A):
 ]
 qed-.
 
+lemma eq_inv_list_append_empty (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-.
+
 (* Advanced inversions ******************************************************)
 
 lemma eq_inv_list_append_dx_sn_refl (A) (l1) (l2):