---

Step * of Lemma fibs-equal-map

fibs() = stream-map(λn.fib(n);nats()) ∈ stream(ℕ)
BY
{ (BLemma `stream-extensionality` THEN Auto) }

1
1. n : ℕ@i
⊢ s-nth(n;fibs()) = s-nth(n;stream-map(λn.fib(n);nats())) ∈ ℕ

---

Latex:

---

Latex:
fibs()  =  stream-map(\mlambda{}n.fib(n);nats())


By

---

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

---

Home Index