X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Flist_append.ma;h=6b5eb992a7b64e5c932ff950b8ca00f4b8a7e29c;hp=e4c3d743e2d17273430c19d9672a86fe3bd7a70c;hb=e6ef5581641345f1c5c72f3c8b6040a9c6e5aecb;hpb=f31020f1ae14e28c246b6cd9cf91b5864f4f536a

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
index e4c3d743e..6b5eb992a 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
@@ -96,3 +96,12 @@ lemma list_ind_append_dx (A) (Q:predicate …):
 #a #l >(list_append_empty_sn … (a⨮l))
 /2 width=1 by/
 qed-.
+
+lemma list_ind_append_sn (A) (Q:predicate …):
+      Q (ⓔ{A}) →
+      (∀l1,l2. Q l2 -> Q (l1⨁l2)) →
+      ∀l. Q l.
+#A #Q #IH1 #IH2 * //
+#a #l >(list_append_empty_dx … (a⨮l))
+/2 width=1 by/
+qed-.