---

Step * 1 of Lemma colength-zero


1. u : Top
2. v : colist(Top)
3. [%2] : (colength([u / v]))↓
4. colength([u / v]) = 0 ∈ ℤ
⊢ [u / v] ~ ⋅
BY
{ (Assert ⌜False⌝⋅ THEN Auto THEN ∀h:hyp. (RecUnfold `colength` h THEN Reduce h) ) }

1
1. u : Top
2. v : colist(Top)
3. (1 + colength(v))↓
4. (1 + colength(v)) = 0 ∈ ℤ
⊢ False

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  colist(Top)
3.  [\%2]  :  (colength([u  /  v]))\mdownarrow{}
4.  colength([u  /  v])  =  0
\mvdash{}  [u  /  v]  \msim{}  \mcdot{}


By

---

Latex:
(Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  \mforall{}h:hyp.  (RecUnfold  `colength`  h  THEN  Reduce  h)  )

---

Home Index