---

Step * 1 of Lemma colength-positive


1. T : Type
2. u : T
3. v : colist(T)
4. [%2] : (1 + colength(v))↓
5. 0 < 1 + colength(v)
6. u ∈ T
⊢ v ∈ T List
BY
{ (Unhide THEN (Assert colength(v) ∈ Base BY (DoSubsume THEN Auto))) }

1
1. T : Type
2. u : T
3. v : colist(T)
4. (1 + colength(v))↓
5. 0 < 1 + colength(v)
6. u ∈ T
7. colength(v) ∈ Base
⊢ v ∈ T List

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  colist(T)
4.  [\%2]  :  (1  +  colength(v))\mdownarrow{}
5.  0  <  1  +  colength(v)
6.  u  \mmember{}  T
\mvdash{}  v  \mmember{}  T  List


By

---

Latex:
(Unhide  THEN  (Assert  colength(v)  \mmember{}  Base  BY  (DoSubsume  THEN  Auto)))

---

Home Index