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