---

Step * of Lemma has-value-append-nil

∀[l:Base]. (l)↓ supposing (l @ [])↓
BY
{ (Auto
   THEN RepUR ``append list_ind`` (-1)
   THEN RW UnrollLoopsC (-1)
   THEN Reduce (-1)
   THEN HasValueD (-1)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[l:Base].  (l)\mdownarrow{}  supposing  (l  @  [])\mdownarrow{}


By

---

Latex:
(Auto
  THEN  RepUR  ``append  list\_ind``  (-1)
  THEN  RW  UnrollLoopsC  (-1)
  THEN  Reduce  (-1)
  THEN  HasValueD  (-1)
  THEN  Trivial)

---

Home Index