---

Step * of Lemma evalall-append-nil

∀[l:Base]. evalall(l @ []) ~ l supposing (evalall(l @ []))↓
BY
{ ((UnivCD THENA Auto) THEN SqequalSqle) }

1
1. l : Base
2. (evalall(l @ []))↓
⊢ evalall(l @ []) ≤ l

2
1. l : Base
2. (evalall(l @ []))↓
⊢ l ≤ evalall(l @ [])

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  SqequalSqle)

---

Home Index