---

Step * of Lemma has-value-last

∀[l:Base]. l ∈ Top × Top supposing (last(l))↓
BY
{ ((UnivCD THENA Auto) THEN RepUR ``last`` (-1) THEN RecUnfold `select` (-1) THEN HasValueD (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[l:Base].  l  \mmember{}  Top  \mtimes{}  Top  supposing  (last(l))\mdownarrow{}


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``last``  (-1)
  THEN  RecUnfold  `select`  (-1)
  THEN  HasValueD  (-1)
  THEN  Auto)

---

Home Index