---

Step * 1 1 of Lemma stream-bijection


1. A : Type
2. a1 : stream(A)
3. a2 : stream(A)
4. (λn.s-nth(n;a1)) = (λn.s-nth(n;a2)) ∈ (ℕ ⟶ A)
⊢ a1 = a2 ∈ stream(A)
BY
{ (BLemma `stream-extensionality` THEN Auto) }

1
1. A : Type
2. a1 : stream(A)
3. a2 : stream(A)
4. (λn.s-nth(n;a1)) = (λn.s-nth(n;a2)) ∈ (ℕ ⟶ A)
5. n : ℕ
⊢ s-nth(n;a1) = s-nth(n;a2) ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  a1  :  stream(A)
3.  a2  :  stream(A)
4.  (\mlambda{}n.s-nth(n;a1))  =  (\mlambda{}n.s-nth(n;a2))
\mvdash{}  a1  =  a2


By

---

Latex:
(BLemma  `stream-extensionality`  THEN  Auto)

---

Home Index