(* Basic inversion lemmas ***************************************************)
lemma eq_stream_inv_seq: ∀A,t1,t2. t1 ≗{A} t2 →
(* Basic inversion lemmas ***************************************************)
lemma eq_stream_inv_seq: ∀A,t1,t2. t1 ≗{A} t2 →