X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Fstream.ma;h=ff7a6c3493dfb2bef0c2792c5836e36cd1e8674d;hb=ae626612bff9c3746dd7647bbada791c737e348c;hp=490a0d0d99bd723ed7e97acd03946bebc1bf0be0;hpb=68b4f2490c12139c03760b39895619e63b0f38c9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
index 490a0d0d9..ff7a6c349 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
@@ -18,13 +18,23 @@ include "ground/lib/relations.ma".
 (* STREAMS ******************************************************************)
 
 coinductive stream (A:Type[0]): Type[0] ≝
-| seq: A → stream A → stream A
+| stream_cons: A → stream A → stream A
 .
 
-interpretation "cons (stream)" 'OPlusRight A a u = (seq A a u).
+interpretation
+  "cons (streams)"
+  'OPlusRight A a u = (stream_cons A a u).
 
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
 
-lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a ⨮ u ] = t.
+lemma stream_rew (A) (t:stream A): match t with [ stream_cons a u ⇒ a ⨮ u ] = t.
 #A * //
 qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_stream_cons_bi (A) (a1,a2:A) (u1) (u2):
+      a1 ⨮ u1 = a2 ⨮ u2 → ∧∧ a1 = a2 & u1 = u2.
+#A #a1 #a2 #u1 #u2 #H destruct
+/2 width=1 by conj/
+qed-.