milestone update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
index 4a3640baed498488974f0c6e34ec370343c8d807..5ddd583d1112a74493c882a3f2506286f38f9428 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
@@ -13,15 +13,17 @@
 (**************************************************************************)
 
 include "ground/notation/functions/downspoon_2.ma".
-include "ground/lib/stream_eq.ma".
+include "ground/lib/stream.ma".
 
 (* HEAD AND TAIL FOR STREAMS ************************************************)
 
-definition stream_hd (A:Type[0]): stream A → A ≝
-           λt. match t with [ stream_cons a _ ⇒ a ].
+definition stream_hd (A:Type[0]): stream A → A.
+#A * #a #_ @a
+defined.
 
-definition stream_tl (A:Type[0]): stream A → stream A ≝
-           λt. match t with [ stream_cons _ t ⇒ t ].
+definition stream_tl (A:Type[0]): stream A → stream A.
+#A * #_ #t @t
+defined.
 
 interpretation
   "tail (streams)"
@@ -37,7 +39,7 @@ lemma stream_tl_cons (A) (a) (t):
       t = ⫰{A}(a⨮t).
 // qed.
 
-lemma eq_stream_split_hd_tl (A) (t):
-      stream_hd … t ⨮ ⫰t ≗{A} t.
+lemma stream_split_tl (A) (t):
+      stream_hd A t ⨮ ⫰t = t.
 #A * //
 qed.