---

Step * of Lemma seq-single_wf

∀[T:Type]. ∀[t:T].  (seq-single(t) ∈ ℕ1 ⟶ T)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[t:T].    (seq-single(t)  \mmember{}  \mBbbN{}1  {}\mrightarrow{}  T)


By

---

Latex:
ProveWfLemma

---

Home Index