---

Step * of Lemma seq-tl_wf

∀[T:Type]. ∀[s:sequence(T)].  seq-tl(s) ∈ sequence(T) supposing 0 < ||s||
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[s:sequence(T)].    seq-tl(s)  \mmember{}  sequence(T)  supposing  0  <  ||s||


By

---

Latex:
Auto

---

Home Index