update in delayed_updating and ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / list_rcons.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index 322235e7a15cc326f44a5c4d9c5873851f1a5612..7d67f5526371571af90a41756b2254bd005a6382 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -40,7 +40,7 @@ lemma list_append_rcons_sn (A):
 // qed.
 
 lemma list_append_rcons_dx (A):
-      ∀l1,l2,a. l1 ⨁ l2 ⨭ a = l1 ⨁{A} (l2 ⨭ a).
+      ∀l1,l2,a. (l1 ⨁ l2) ⨭ a = l1 ⨁{A} (l2 ⨭ a).
 // qed.
 
 (* Basic inversions *********************************************************)
@@ -51,6 +51,12 @@ lemma eq_inv_list_empty_rcons (A):
 elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
 qed-.
 
+lemma eq_inv_list_rcons_empty (A):
+      ∀l,a. l⨭{A}a = ⓔ → ⊥.
+#A #l #a #H0
+elim (eq_inv_list_append_empty … H0) -H0 #_ #H0 destruct
+qed-.
+
 (* Advanced inversions ******************************************************)
 
 lemma eq_inv_list_rcons_bi (A):
@@ -80,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-.