---

Step * 2 of Lemma has-value-last-list


1. l : Base
2. (⊥)↓
3. ∀a,b:Base.  (if l is a pair then a otherwise b ~ b)
4. ∀[F:Top]. (let x,y = l in F[x;y] ~ eval x = l in ⊥)
5. (l)↓
⊢ (||l||)↓
BY
{ BotDiv }

---

Latex:

---

Latex:

1.  l  :  Base
2.  (\mbot{})\mdownarrow{}
3.  \mforall{}a,b:Base.    (if  l  is  a  pair  then  a  otherwise  b  \msim{}  b)
4.  \mforall{}[F:Top].  (let  x,y  =  l  in  F[x;y]  \msim{}  eval  x  =  l  in  \mbot{})
5.  (l)\mdownarrow{}
\mvdash{}  (||l||)\mdownarrow{}


By

---

Latex:
BotDiv

---

Home Index