wip in delayed_updating

[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 e4c3d743e2d17273430c19d9672a86fe3bd7a70c..6b5eb992a7b64e5c932ff950b8ca00f4b8a7e29c 100644 (file)
--- 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-.