---

Step * of Lemma islist-implies-is-list

∀[t:Base]. t ∈ Base List supposing islist(t)
BY
{ (Auto
   THEN RepUR ``islist eval_list list_ind`` (-1)
   THEN Compactness (-1)
   THEN Unhide
   THEN Thin (-3)
   THEN MoveToConcl 1
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN (UnivCD THENA Auto)
   THEN BotDiv
   THEN (RWO "fun_exp_unroll" (-1) THENA Auto)
   THEN SplitOnHypITE (-1)
   THEN Auto
   THEN RepUR ``compose`` (-2)) }

1
1. j : ℤ
2. 0 < j
3. ∀t:Base
     ((λlist_ind,L. eval v = L in if v is a pair then let h,t = v in eval s = list_ind t in <h, s> otherwise if v = Ax t\000Chen [] otherwise ⊥^j - 1 ⊥ t)↓
     ⇒ (t ∈ Base List))
4. t : Base
5. (eval v = t in
    if v is a pair then let h,t = v 
                        in eval s = λlist_ind,L. eval v = L in
                                                 if v is a pair then let h,t = v 
                                                                     in eval s = list_ind t in
                                                                        <h, s> otherwise if v = Ax then [] otherwise ⊥^j\000C - 1 
                                    ⊥ 
                                    t in
                           <h, s> otherwise if v = Ax then [] otherwise ⊥)↓
6. ¬(j = 0 ∈ ℤ)
⊢ t ∈ Base List

---

Latex:

---

Latex:
\mforall{}[t:Base].  t  \mmember{}  Base  List  supposing  islist(t)


By

---

Latex:
(Auto
  THEN  RepUR  ``islist  eval\_list  list\_ind``  (-1)
  THEN  Compactness  (-1)
  THEN  Unhide
  THEN  Thin  (-3)
  THEN  MoveToConcl  1
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  (UnivCD  THENA  Auto)
  THEN  BotDiv
  THEN  (RWO  "fun\_exp\_unroll"  (-1)  THENA  Auto)
  THEN  SplitOnHypITE  (-1)
  THEN  Auto
  THEN  RepUR  ``compose``  (-2))

---

Home Index