---

Step * 1 of Lemma islist-iff-length-has-value


1. T : Type
2. t : colist(T)
3. (is-list(t))↓
⊢ (||t||)↓
BY
{ (Unfold `is-list` -1
   THEN Compactness (-1)
   THEN Thin (-3)
   THEN MoveToConcl (-1)
   THEN MoveToConcl 2
   THEN UseWitness ⌜λt,x. Ax⌝⋅
   THEN WeakNatInd (-1)
   THEN All (Fold `is-list-fun`)) }

1
1. T : Type
2. j : ℤ
⊢ λt,x. Ax ∈ ∀t:colist(T). ((is-list-fun()^0 ⊥ t)↓ ⇒ (||t||)↓)

2
1. T : Type
2. j : ℤ
3. 0 < j
4. λt,x. Ax ∈ ∀t:colist(T). ((is-list-fun()^j - 1 ⊥ t)↓ ⇒ (||t||)↓)
⊢ λt,x. Ax ∈ ∀t:colist(T). ((is-list-fun()^j ⊥ t)↓ ⇒ (||t||)↓)

---

Latex:

---

Latex:

1.  T  :  Type
2.  t  :  colist(T)
3.  (is-list(t))\mdownarrow{}
\mvdash{}  (||t||)\mdownarrow{}


By

---

Latex:
(Unfold  `is-list`  -1
  THEN  Compactness  (-1)
  THEN  Thin  (-3)
  THEN  MoveToConcl  (-1)
  THEN  MoveToConcl  2
  THEN  UseWitness  \mkleeneopen{}\mlambda{}t,x.  Ax\mkleeneclose{}\mcdot{}
  THEN  WeakNatInd  (-1)
  THEN  All  (Fold  `is-list-fun`))

---

Home Index