X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream.ma;h=c852317f895c60e34fc403dd6f7c2572bc0a3620;hb=5ad776e509cd35fa003292e8bf2ed8f31d2c0a4b;hp=aaa1ba9b6551f67099861a199fdf067f9169e558;hpb=b9526dac808d40bf89dc378cf9c5ea0c121526a4;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
index aaa1ba9b6..c852317f8 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
@@ -13,8 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/notation/functions/lift_1.ma".
-include "ground_2/lib/arith.ma".
-include "ground_2/lib/streams.ma".
+include "ground_2/lib/streams_tls.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
@@ -26,7 +25,7 @@ interpretation "push (nstream)" 'Lift f = (push f).
 
 definition next: rtmap → rtmap.
 * #n #f @(⫯n@f)
-qed.
+defined.
 
 interpretation "next (nstream)" 'Successor f = (next f).
 
@@ -88,3 +87,11 @@ lemma iota_push: ∀R,a,b,f. a f = case_type0 R a b (↑f).
 lemma iota_next: ∀R,a,b,f. b f = case_type0 R a b (⫯f).
 #R #a #b * //
 qed.
+
+(* Specific properties ******************************************************)
+
+lemma tl_push: ∀f. f = ↓↑f.
+// qed.
+
+lemma tl_next: ∀f. ↓f = ↓⫯f.
+* // qed.