---

Step * of Lemma colength-positive2

∀[T:Type]. ∀[L:T List].
  ∀n:ℕ
    (0 < n
    ⇒ (colength(L) = n ∈ ℤ)
    ⇒ {(fst(L) ∈ T) ∧ (snd(L) ∈ T List) ∧ (colength(L) = (1 + colength(snd(L))) ∈ ℤ) ∧ (L ~ [fst(L) / (snd(L))])})
BY
{ (InstLemma `colength-positive` [] THEN RepeatFor 2 (ParallelLast') THEN Auto THEN D 3 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].
    \mforall{}n:\mBbbN{}
        (0  <  n
        {}\mRightarrow{}  (colength(L)  =  n)
        {}\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:
(InstLemma  `colength-positive`  []  THEN  RepeatFor  2  (ParallelLast')  THEN  Auto  THEN  D  3  THEN  Auto)

---

Home Index