---

Step * of Lemma length-in-bar-int-if-co-list

∀[T:Type]. ∀[t:colist(T)].  (||t|| ∈ partial(ℤ))
BY
{ ((UnivCD THENA Auto) THEN RWO "length-is-colength" 0 THEN Try (MemTop)) }

1
1. T : Type
2. t : colist(T)
⊢ colength(t) ∈ partial(ℤ)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].    (||t||  \mmember{}  partial(\mBbbZ{}))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "length-is-colength"  0  THEN  Try  (MemTop))

---

Home Index