---

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


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
BY
{ HVimplies2 (-3) [1] }

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

---

Latex:

---

Latex:

1.  l  :  Base@i
2.  ||l||  =  0
3.  (if  l  =  Ax  then  0  otherwise  \mbot{})\mdownarrow{}
4.  (l)\mdownarrow{}
5.  \mforall{}a,b:Top.    (if  l  is  a  pair  then  a  otherwise  b  \msim{}  b)
\mvdash{}  l  =  []


By

---

Latex:
HVimplies2  (-3)  [1]

---

Home Index