X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Fstream_hdtl_eq.ma;h=f113e998871baff0546388257e7d83f345295e87;hb=4939d8280cb3467cd8fa648b1cea04f74d71e8b7;hp=ebe087664523abbd9c05a4da65dfdee03f9f8c09;hpb=e6ef5581641345f1c5c72f3c8b6040a9c6e5aecb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma
index ebe087664..f113e9988 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma
@@ -32,3 +32,18 @@ lemma stream_tl_eq_repl (A):
 elim (stream_eq_inv_cons_bi … H) -H
 /2 width=7 by/
 qed.
+
+lemma stream_hd_tl_eq_repl (A) (t1) (t2):
+      t1 ≗{A} t2 →
+      ∧∧ ⇃t1 = ⇃t2 & ⇂t1 ≗ ⇂t2.
+#A #t1 #t2 #H
+/3 width=1 by stream_tl_eq_repl, stream_hd_eq_repl, conj/
+qed-.
+
+(* Inversions with stram_eq *************************************************)
+
+lemma stream_eq_inv_hd_tl_bi (A) (t1) (t2):
+      ⇃t1 = ⇃t2 → ⇂t1 ≗ ⇂t2 → t1 ≗{A} t2.
+#A * #a1 #t1 * #a2 #t2
+/2 width=1 by stream_eq_cons/
+qed-.