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..eb7210e2213d2b62bf20fc83c9c35516479a1965 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,9 @@ 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.