---

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


1. l : Base@i
2. ||l|| = 0 ∈ ℤ
3. (||l||)↓
⊢ l = [] ∈ Base
BY
{ (Unfold `length` -1 THEN RecUnfold `list_ind` (-1) THEN HasValueD (-1)) }

1
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

---

Latex:

---

Latex:

1.  l  :  Base@i
2.  ||l||  =  0
3.  (||l||)\mdownarrow{}
\mvdash{}  l  =  []


By

---

Latex:
(Unfold  `length`  -1  THEN  RecUnfold  `list\_ind`  (-1)  THEN  HasValueD  (-1))

---

Home Index