precommit for rtmap ...

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / streams_hdtl.ma

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 90af6fd87354cdcbf11061f7ae0aab13c07a52ab..bdc740c82ff42646cbd6fb362c6ac714fa731cf3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
@@ -32,3 +32,8 @@ qed.
 lemma eq_stream_split (A) (t): (hd … t) @ (tl … t) ≐⦋A⦌ t.
 #A * //
 qed.
+
+lemma tln_eq_repl (A) (i): eq_stream_repl A (λt1,t2. tln … i t1 ≐ tln … i t2).
+#A #i elim i -i //
+#i #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq … H) /2 width=7 by/
+qed.