---

Step * of Lemma has-value-append

∀[l,k:Base].  (l)↓ supposing (l @ k)↓
BY
{ (Auto
   THEN RepUR ``append list_ind`` (-1)
   THEN Compactness (-1)
   THEN SqUnhide
   THEN Thin (-3)
   THEN MoveToConcl 1
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN (UnivCD THENA Auto)
   THEN BotDiv) }

1
1. k : Base
2. j : ℤ
3. 0 < j
4. ∀l:Base
     ((λlist_ind,L. eval v = L in
                    if v is a pair then let a,as' = v 
                                        in [a / (list_ind as')] otherwise if v = Ax then k otherwise ⊥^j - 1 
       ⊥ 
       l)↓
     ⇒ (l)↓)
5. l : Base@i
6. (λlist_ind,L. eval v = L in
                 if v is a pair then let a,as' = v 
                                     in [a / (list_ind as')] otherwise if v = Ax then k otherwise ⊥^j 
    ⊥ 
    l)↓@i
⊢ (l)↓

---

Latex:

---

Latex:
\mforall{}[l,k:Base].    (l)\mdownarrow{}  supposing  (l  @  k)\mdownarrow{}


By

---

Latex:
(Auto
  THEN  RepUR  ``append  list\_ind``  (-1)
  THEN  Compactness  (-1)
  THEN  SqUnhide
  THEN  Thin  (-3)
  THEN  MoveToConcl  1
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  (UnivCD  THENA  Auto)
  THEN  BotDiv)

---

Home Index