---

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


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
BY
{ BotDiv }

---

Latex:

---

Latex:

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


By

---

Latex:
BotDiv

---

Home Index