---

Step * of Lemma stream-map_wf

∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[s:stream(A)].  (stream-map(f;s) ∈ stream(B))
BY
{ (Auto THEN Unfolds ``stream-map stream`` 0)⋅ }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. s : stream(A)
⊢ fix((λstream-map,s. let a,s' = s in <f a, stream-map s'>)) s ∈ corec(S.B × S)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[s:stream(A)].    (stream-map(f;s)  \mmember{}  stream(B))


By

---

Latex:
(Auto  THEN  Unfolds  ``stream-map  stream``  0)\mcdot{}

---

Home Index