---

Step * of Lemma colength-zero

∀[L:Top List]. ((colength(L) = 0 ∈ ℤ) ⇒ (L ~ []))
BY
{ (Auto THEN (Unfold `list` 1 THEN D 1) THEN colistD 1 THEN Unfold `nil` 0 THEN Auto) }

1
1. u : Top
2. v : colist(Top)
3. [%2] : (colength([u / v]))↓
4. colength([u / v]) = 0 ∈ ℤ
⊢ [u / v] ~ ⋅

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  ((colength(L)  =  0)  {}\mRightarrow{}  (L  \msim{}  []))


By

---

Latex:
(Auto  THEN  (Unfold  `list`  1  THEN  D  1)  THEN  colistD  1  THEN  Unfold  `nil`  0  THEN  Auto)

---

Home Index