update in gruound

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

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
index d0e05e17e067632d71937926eba6a6494969265c..ff7a6c3493dfb2bef0c2792c5836e36cd1e8674d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
@@ -30,3 +30,11 @@ interpretation
 lemma stream_rew (A) (t:stream A): match t with [ stream_cons a u ⇒ a ⨮ u ] = t.
 #A * //
 qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_stream_cons_bi (A) (a1,a2:A) (u1) (u2):
+      a1 ⨮ u1 = a2 ⨮ u2 → ∧∧ a1 = a2 & u1 = u2.
+#A #a1 #a2 #u1 #u2 #H destruct
+/2 width=1 by conj/
+qed-.