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 b2f042c1f20faeae78cba32d601ea94e3952b311..f66c8a63fd451ce8940fcc5297d1951b7ecc9957 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
@@ -46,3 +46,13 @@ qed.
 lemma stream_tls_swap (A) (n) (t):
       (⇂*[n]⇂t) = ⇂*{A}[↑n]t.
 // qed.
+
+(* Advanced constructions ***************************************************)
+
+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.