(* STREAMS ******************************************************************)
coinductive stream (A:Type[0]): Type[0] ≝
-| seq: A → stream A → stream A
+| stream_cons: A → stream A → stream A
.
-interpretation "cons (stream)" 'OPlusRight A a u = (seq A a u).
+interpretation
+ "cons (streams)"
+ 'OPlusRight A a u = (stream_cons A a u).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
-lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a ⨮ u ] = t.
+(*** stream_rew *)
+lemma stream_unfold (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-.