---

Step * of Lemma seq-nil_wf

∀[T:Type]. (seq-nil() ∈ sequence(T))
BY
{ (ProveWfLemma THEN FunExt THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  (seq-nil()  \mmember{}  sequence(T))


By

---

Latex:
(ProveWfLemma  THEN  FunExt  THEN  Auto)

---

Home Index