---

Step * of Lemma colength-cons-not-zero

∀[T:Type]. ∀[v:T List]. ∀[u:Top].  False supposing colength([u / v]) = 0 ∈ ℕ
BY
{ (RepeatFor 3 (Intro) THEN RecUnfold `colength` 0 THEN Reduce 0 THEN D 0) }

1
1. T : Type
2. v : T List
3. u : Top
4. (1 + colength(v)) = 0 ∈ ℕ
⊢ False

2
.....wf..... 
1. T : Type
2. v : T List
3. u : Top
⊢ istype((1 + colength(v)) = 0 ∈ ℕ)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[v:T  List].  \mforall{}[u:Top].    False  supposing  colength([u  /  v])  =  0


By

---

Latex:
(RepeatFor  3  (Intro)  THEN  RecUnfold  `colength`  0  THEN  Reduce  0  THEN  D  0)

---

Home Index