---

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


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

1
.....basecase..... 
1. T : Type
2. j : ℤ
⊢ λt,x. Ax ∈ ∀t:colist(T)
           ((λlist_ind,L. eval v = L in
                          if v is a pair then let a,b = v 
                                              in (list_ind b) + 1 otherwise if v = Ax then 0 otherwise ⊥^0 
             ⊥ 
             t)↓
           ⇒ (is-list(t))↓)

2
.....upcase..... 
1. T : Type
2. j : ℤ
3. 0 < j
4. λt,x. Ax ∈ ∀t:colist(T)
            ((λlist_ind,L. eval v = L in
                           if v is a pair then let a,b = v 
                                               in (list_ind b) + 1 otherwise if v = Ax then 0 otherwise ⊥^j - 1 
              ⊥ 
              t)↓
            ⇒ (is-list(t))↓)
⊢ λt,x. Ax ∈ ∀t:colist(T)
           ((λlist_ind,L. eval v = L in
                          if v is a pair then let a,b = v 
                                              in (list_ind b) + 1 otherwise if v = Ax then 0 otherwise ⊥^j 
             ⊥ 
             t)↓
           ⇒ (is-list(t))↓)

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``length  list\_ind``  -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))

---

Home Index