---

Step * 1 1 of Lemma length-zero-implies-nil


1. l : Base@i
2. ||l|| = 0 ∈ ℤ
3. (if l is a pair then let a,b = l 
                        in rec-case(b) of [] => 0 | h::t => r.r + 1 + 1 otherwise if l = Ax then 0 otherwise ⊥)↓
4. (l)↓
⊢ l = [] ∈ Base
BY
{ HVimplies2 (-2) [1] }

1
1. l : Base@i
2. ||<fst(l), snd(l)>|| = 0 ∈ ℤ
3. (rec-case(snd(l)) of [] => 0 | h::t => r.r + 1 + 1)↓
4. 0 ≤ 0
5. l ~ <fst(l), snd(l)>
⊢ <fst(l), snd(l)> = [] ∈ Base

2
1. l : Base@i
2. ||l|| = 0 ∈ ℤ
3. (if l = Ax then 0 otherwise ⊥)↓
4. (l)↓
5. ∀a,b:Top.  (if l is a pair then a otherwise b ~ b)
⊢ l = [] ∈ Base

---

Latex:

---

Latex:

1.  l  :  Base@i
2.  ||l||  =  0
3.  (if  l  is  a  pair  then  let  a,b  =  l 
                                                in  rec-case(b)  of  []  =>  0  |  h::t  =>  r.r  +  1  +  1
        otherwise  if  l  =  Ax  then  0  otherwise  \mbot{})\mdownarrow{}
4.  (l)\mdownarrow{}
\mvdash{}  l  =  []


By

---

Latex:
HVimplies2  (-2)  [1]

---

Home Index