update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / stream_hdtl_eq.ma

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 ebe087664523abbd9c05a4da65dfdee03f9f8c09..f113e998871baff0546388257e7d83f345295e87 100644 (file)
--- 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-.