---

Step * 1 of Lemma eval_list-sqle-append-nil


1. t : Base
2. ¬is-exception(eval_list(t))
3. (eval_list(t))↓
⊢ eval_list(t) ≤ t @ []
BY
{ (Fold `islist` (-1) THEN (FLemma `islist-implies-is-list` [-1] THENA Auto)) }

1
1. t : Base
2. ¬is-exception(eval_list(t))
3. islist(t)
4. t ∈ Base List
⊢ eval_list(t) ≤ t @ []

---

Latex:

---

Latex:

1.  t  :  Base
2.  \mneg{}is-exception(eval\_list(t))
3.  (eval\_list(t))\mdownarrow{}
\mvdash{}  eval\_list(t)  \mleq{}  t  @  []


By

---

Latex:
(Fold  `islist`  (-1)  THEN  (FLemma  `islist-implies-is-list`  [-1]  THENA  Auto))

---

Home Index