]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / stream_hdtl.ma
index 468f306de0bbcbd4429b6a4607b69779e0a31e8e..d6a9a574243c23fe9e65f2ced8569ce537da3296 100644 (file)
@@ -36,11 +36,11 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma stream_hd_cons (A) (a) (t):
+lemma stream_hd_lcons (A) (a) (t):
       a = ⇃{A}(a⨮t).
 // qed.
 
-lemma stream_tl_cons (A) (a) (t):
+lemma stream_tl_lcons (A) (a) (t):
       t = ⇂{A}(a⨮t).
 // qed.