update in 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 2cf2e23bf07f662e9563fc2e0dccb9274e1ff8d7..9d2fcfaacc624b00f10ec262ccf9131a0eaae807 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -14,6 +14,7 @@
 
 include "ground/notation/functions/oplusleft_3.ma".
 include "ground/lib/list_append.ma".
+include "ground/generated/pull_2.ma". 
 
 (* RIGHT CONS FOR LISTS *****************************************************)
 
@@ -41,3 +42,23 @@ lemma list_append_rcons_sn (A):
 lemma list_append_rcons_dx (A):
       ∀l1,l2,a. l1 ⨁ l2 ⨭ a = l1 ⨁{A} (l2 ⨭ a).
 // qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_list_empty_rcons (A):
+      ∀l,a. ⓔ = l⨭{A}a → ⊥.
+#A #l #a #H
+elim (eq_inv_list_empty_append … H) -H #_ #H destruct
+qed-.
+
+(* Advanced eliminations ****************************************************)
+
+lemma list_ind_rcons (A) (Q:predicate …):
+      Q (ⓔ{A}) →
+      (∀l,a. Q l -> Q (l⨭a)) →
+      ∀l. Q l.
+#A #Q #IH1 #IH2 #l
+@(list_ind_append_dx … l) -l //
+@pull_2 #l2 elim l2 -l2 //
+#a2 #l2 #IH0 #l1 #IH /3 width=1 by/
+qed-.