X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Fstreams_hdtl.ma;h=3a31efc350da7ba6e6769ce360969ddfa754b564;hb=24ba1bb3f67505d3e384747ff90d26d3996bd3f5;hp=90af6fd87354cdcbf11061f7ae0aab13c07a52ab;hpb=750305d95b8f6bb40b5be0e9dfd05d42b256f2a1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
index 90af6fd87..3a31efc35 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
@@ -12,7 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/lib/streams.ma".
+include "ground_2/notation/functions/drop_1.ma".
+include "ground_2/lib/streams_eq.ma".
 include "ground_2/lib/arith.ma".
 
 (* STREAMS ******************************************************************)
@@ -23,12 +24,16 @@ definition hd (A:Type[0]): stream A → A ≝
 definition tl (A:Type[0]): stream A → stream A ≝
               λt. match t with [ seq _ t ⇒ t ].
 
-let rec tln (A:Type[0]) (i:nat) on i: stream A → stream A ≝ ?.
-cases i -i [ #t @t | #i * #_ #t @(tln … i t) ]
-qed.
+interpretation "tail (streams)" 'Drop t = (tl ? t).
 
 (* basic properties *********************************************************)
 
-lemma eq_stream_split (A) (t): (hd … t) @ (tl … t) ≐⦋A⦌ t.
+lemma hd_rew (A) (a) (t): a = hd A (a@t).
+// qed.
+
+lemma tl_rew (A) (a) (t): t = tl A (a@t).
+// qed.
+
+lemma eq_stream_split (A) (t): (hd … t) @ ↓t ≐⦋A⦌ t.
 #A * //
 qed.