---

Step * of Lemma s-tl_wf

∀[A:Type]. ∀[s:stream(A)].  (s-tl(s) ∈ stream(A))
BY
{ ProveWfLemma }

1
1. A : Type
2. s : stream(A)
⊢ snd(s) ∈ stream(A)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[s:stream(A)].    (s-tl(s)  \mmember{}  stream(A))


By

---

Latex:
ProveWfLemma

---

Home Index