X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Fstream_tls.ma;h=f66c8a63fd451ce8940fcc5297d1951b7ecc9957;hb=f717d9ef23433a96583a1bc8ae6b903689d5f033;hp=eb7210e2213d2b62bf20fc83c9c35516479a1965;hpb=62d0f5f2c89830ebe884e6afee91eb68b68790fc;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
index eb7210e22..f66c8a63f 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
@@ -52,3 +52,7 @@ lemma stream_tls_swap (A) (n) (t):
 lemma stream_tls_unit (A) (t):
       ⇂t = ⇂*{A}[𝟏]t.
 // qed.
+
+lemma stream_tls_succ_lcons (A) (n) (a) (t):
+      ⇂*[n]t = ⇂*{A}[↑n](a⨮t).
+// qed.