---

Step * of Lemma colength_wf

∀[T:Type]. ∀[L:colist(T)].  (colength(L) ∈ partial(ℕ))
BY
{ TACTIC:(Auto THEN Unfold `colength` 0 THEN BLemma `colist-fix-ap-partial` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:colist(T)].    (colength(L)  \mmember{}  partial(\mBbbN{}))


By

---

Latex:
TACTIC:(Auto  THEN  Unfold  `colength`  0  THEN  BLemma  `colist-fix-ap-partial`  THEN  Auto)

---

Home Index