---

Step * of Lemma has-value-l-last

∀[l:Base]. l ∈ Top × Top supposing (l-last(l))↓
BY
{ (Auto
   THEN RepUR ``l-last l-last-default list_ind`` (-1)
   THEN RW UnrollLoopsC (-1)
   THEN Reduce (-1)
   THEN RepeatFor 2 (HasValueD (-1))
   THEN HVimplies2 (-2) [1]
   THEN HVimplies2 (-3) [1]
   THEN BotDiv) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepUR  ``l-last  l-last-default  list\_ind``  (-1)
  THEN  RW  UnrollLoopsC  (-1)
  THEN  Reduce  (-1)
  THEN  RepeatFor  2  (HasValueD  (-1))
  THEN  HVimplies2  (-2)  [1]
  THEN  HVimplies2  (-3)  [1]
  THEN  BotDiv)

---

Home Index