X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Flist_append.ma;h=e4c3d743e2d17273430c19d9672a86fe3bd7a70c;hb=df1bcd1387439133c0c33f597a5f8b2331c07772;hp=2dcf8e5767bf41807995257ae8b831b4a547f579;hpb=dd41efaab7f147d5673cc30a27d36375f9b52c9d;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 2dcf8e576..e4c3d743e 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
@@ -29,7 +29,7 @@ interpretation
 (* Basic constructions ******************************************************)
 
 lemma list_append_empty_sn (A):
-      ∀l2. l2 = Ⓔ ⨁{A} l2.
+      ∀l2. l2 = ⓔ ⨁{A} l2.
 // qed.
 
 lemma list_append_lcons_sn (A):
@@ -39,7 +39,7 @@ lemma list_append_lcons_sn (A):
 (* Advanced constructions ***************************************************)
 
 lemma list_append_empty_dx (A):
-      ∀l1. l1 = l1 ⨁{A} Ⓔ.
+      ∀l1. l1 = l1 ⨁{A} ⓔ.
 #A #l1 elim l1 -l1
 [ <list_append_empty_sn //
 | #hd #tl #IH <list_append_lcons_sn <IH //
@@ -56,3 +56,43 @@ 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-.
+
+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):
+      l1 = l1⨁{A}l2 → ⓔ = l2.
+#A #l1 elim l1 -l1 [ // ]
+#a1 #l1 #IH #l2 <list_append_lcons_sn #H0 destruct -H0
+/2 width=1 by/
+qed-.
+
+(* Advanced eliminations ****************************************************)
+
+lemma list_ind_append_dx (A) (Q:predicate …):
+      Q (ⓔ{A}) →
+      (∀l1,l2. Q l1 -> Q (l1⨁l2)) →
+      ∀l. Q l.
+#A #Q #IH1 #IH2 * //
+#a #l >(list_append_empty_sn … (a⨮l))
+/2 width=1 by/
+qed-.