]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/lib/stream.ma
milestone update in ground
[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / stream.ma
index ff7a6c3493dfb2bef0c2792c5836e36cd1e8674d..501daa0316a2c648f25c7d79204e7a3060fa8133 100644 (file)
@@ -27,7 +27,9 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma stream_rew (A) (t:stream A): match t with [ stream_cons a u ⇒ a ⨮ u ] = t.
+(*** stream_rew *)
+lemma stream_unfold (A) (t:stream A):
+      match t with [ stream_cons a u ⇒ a ⨮ u ] = t.
 #A * //
 qed.