---

Step * of Lemma islist-append-nil-is-list

∀[l:Base]. l ∈ Base List supposing islist(l @ [])
BY
{ (Auto THEN (RWO "islist-append-nil-sqequal-islist" (-1) THENA Auto) THEN BLemma `islist-implies-is-list` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[l:Base].  l  \mmember{}  Base  List  supposing  islist(l  @  [])


By

---

Latex:
(Auto
  THEN  (RWO  "islist-append-nil-sqequal-islist"  (-1)  THENA  Auto)
  THEN  BLemma  `islist-implies-is-list`
  THEN  Auto)

---

Home Index