---

Step * of Lemma eval_list-append-nil-is-eval_list

∀[t:Top]. (eval_list(t @ []) ~ eval_list(t))
BY
{ ListIndSq `t' }

---

Latex:

---

Latex:
\mforall{}[t:Top].  (eval\_list(t  @  [])  \msim{}  eval\_list(t))


By

---

Latex:
ListIndSq  `t'

---

Home Index