---

Step * of Lemma has-value-l-last-default-list

∀[l,d:Base].  l ∈ Top List supposing (l-last-default(l;d))↓
BY
{ (Auto
   THEN RepUR ``l-last-default list_ind`` (-1)
   THEN Compactness (-1)
   THEN Unhide
   THEN Thin (-3)
   THEN MoveToConcl (-1)
   THEN Repeat (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN (UnivCD THENA Auto)
   THEN BotDiv
   THEN (RWO "fun_exp_unroll_1" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN HasValueD (-1)
   THEN HasValueD (-1)
   THEN HVimplies2 (-2) [1]) }

1
1. j : ℤ
2. 0 < j
3. ∀l,d:Base.
     ((λlist_ind,L. eval v = L in
                    if v is a pair then let h,t = v 
                                        in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥^j - 1 
       ⊥ 
       l 
       d)↓
     ⇒ (l ∈ Top List))
4. l : Base@i
5. d : Base@i
6. (λlist_ind,L. eval v = L in
                 if v is a pair then let h,t = v 
                                     in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥^j - 1 
    ⊥ 
    (snd(l)) 
    (fst(l)))↓@i
7. 0 ≤ 0
8. 0 ≤ 0
9. l ~ <fst(l), snd(l)>
⊢ <fst(l), snd(l)> ∈ Top List

2
1. j : ℤ
2. 0 < j
3. ∀l,d:Base.
     ((λlist_ind,L. eval v = L in
                    if v is a pair then let h,t = v 
                                        in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥^j - 1 
       ⊥ 
       l 
       d)↓
     ⇒ (l ∈ Top List))
4. l : Base@i
5. d : Base@i
6. (eval v = l in
    if v is a pair then let h,t = v 
                        in λx.(λlist_ind,L. eval v = L in
                                            if v is a pair then let h,t = v 
                                                                in λx.(list_ind t h)
                                            otherwise if v = Ax then λx.x otherwise ⊥^j - 1 
                               ⊥ 
                               t 
                               h) otherwise if v = Ax then λx.x otherwise ⊥ 
    d)↓@i
7. (if l = Ax then λx.x otherwise ⊥)↓
8. (l)↓
9. ∀a,b:Top.  (if l is a pair then a otherwise b ~ b)
⊢ l ∈ Top List

---

Latex:

---

Latex:
\mforall{}[l,d:Base].    l  \mmember{}  Top  List  supposing  (l-last-default(l;d))\mdownarrow{}


By

---

Latex:
(Auto
  THEN  RepUR  ``l-last-default  list\_ind``  (-1)
  THEN  Compactness  (-1)
  THEN  Unhide
  THEN  Thin  (-3)
  THEN  MoveToConcl  (-1)
  THEN  Repeat  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  (UnivCD  THENA  Auto)
  THEN  BotDiv
  THEN  (RWO  "fun\_exp\_unroll\_1"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  HasValueD  (-1)
  THEN  HasValueD  (-1)
  THEN  HVimplies2  (-2)  [1])

---

Home Index