---

Step * of Lemma eval_list-sqle-append-nil

∀[t:Base]. eval_list(t) ≤ t @ [] supposing ¬is-exception(eval_list(t))
BY
{ (Auto THEN Try ((BLemma `is-exception_wf`  THEN Auto))) }

1
1. t : Base
2. ¬is-exception(eval_list(t))
3. (eval_list(t))↓
⊢ eval_list(t) ≤ t @ []

---

Latex:

---

Latex:
\mforall{}[t:Base].  eval\_list(t)  \mleq{}  t  @  []  supposing  \mneg{}is-exception(eval\_list(t))


By

---

Latex:
(Auto  THEN  Try  ((BLemma  `is-exception\_wf`    THEN  Auto)))

---

Home Index