update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
index 31644956669dea1ade08a8e62593873695736452..e4c3d743e2d17273430c19d9672a86fe3bd7a70c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
@@ -68,6 +68,24 @@ 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):
+      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 …):