---

Step * of Lemma length-in-prop-if-co-list

∀[T:Type]. ∀[t:colist(T)].  (∃n:ℕ. (||t|| = n ∈ partial(ℤ)) ∈ ℙ)
BY
{ (Intros THEN Unhide THEN RepeatFor 2 (MemCD') THEN Try (BLemma `length-in-bar-int-if-co-list`) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].    (\mexists{}n:\mBbbN{}.  (||t||  =  n)  \mmember{}  \mBbbP{})


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  RepeatFor  2  (MemCD')
  THEN  Try  (BLemma  `length-in-bar-int-if-co-list`)
  THEN  Auto)

---

Home Index