---

Step * of Lemma length-if-co-list-sq

∀[T:Type]. ∀[t:colist(T)]. ∀[n:ℕ].  ||t|| ~ n supposing ||t|| = n ∈ partial(ℤ)
BY
{ (RepeatFor 3 (Intro)
   THEN (InstLemma `length-in-bar-int-if-co-list` [⌜T⌝;⌜t⌝]⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (Assert ⌜||t|| = n ∈ ℤ⌝⋅ THENM (HypSubst' (-1) 0 THEN Auto))) }

1
.....assertion..... 
1. T : Type
2. t : colist(T)
3. n : ℕ
4. ||t|| ∈ partial(ℤ)
5. ||t|| = n ∈ partial(ℤ)
⊢ ||t|| = n ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].  \mforall{}[n:\mBbbN{}].    ||t||  \msim{}  n  supposing  ||t||  =  n


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (InstLemma  `length-in-bar-int-if-co-list`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}||t||  =  n\mkleeneclose{}\mcdot{}  THENM  (HypSubst'  (-1)  0  THEN  Auto)))

---

Home Index