update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
index eb7210e2213d2b62bf20fc83c9c35516479a1965..f66c8a63fd451ce8940fcc5297d1951b7ecc9957 100644 (file)
--- 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.