-lemma eq_stream_inv_seq: â\88\80A,t1,t2. t1 â\89\90â¦\8bAâ¦\8c t2 →
- ∀u1,u2,a1,a2. a1@u1 = t1 → a2@u2 = t2 →
- u1 â\89\90 u2 ∧ a1 = a2.
+lemma eq_stream_inv_seq: â\88\80A,t1,t2. t1 â\89\97{A} t2 →
+ ∀u1,u2,a1,a2. a1⨮u1 = t1 → a2⨮u2 = t2 →
+ u1 â\89\97 u2 ∧ a1 = a2.