---

Step * of Lemma colength-positive

∀[T:Type]. ∀[L:T List].
  (0 < colength(L)
  ⇒ {(fst(L) ∈ T) ∧ (snd(L) ∈ T List) ∧ (colength(L) = (1 + colength(snd(L))) ∈ ℤ) ∧ (L ~ [fst(L) / (snd(L))])})
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `list` 2
   THEN D 2
   THEN colistD 2
   THEN ∀h:hyp. (RecUnfold `colength` h THEN Reduce h) 
   THEN RepUR ``cons`` 0
   THEN Auto) }

1
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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].
    (0  <  colength(L)
    {}\mRightarrow{}  \{(fst(L)  \mmember{}  T)
          \mwedge{}  (snd(L)  \mmember{}  T  List)
          \mwedge{}  (colength(L)  =  (1  +  colength(snd(L))))
          \mwedge{}  (L  \msim{}  [fst(L)  /  (snd(L))])\})


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `list`  2
  THEN  D  2
  THEN  colistD  2
  THEN  \mforall{}h:hyp.  (RecUnfold  `colength`  h  THEN  Reduce  h) 
  THEN  RepUR  ``cons``  0
  THEN  Auto)

---

Home Index