---

Step * 1 of Lemma evalall-append-nil


1. l : Base
2. (evalall(l @ []))↓
⊢ evalall(l @ []) ≤ l
BY
{ ((InstLemma `evalall-sqle` [⌜l @ []⌝]⋅ THENA Auto)
   THEN SqLeTrans (-1)
   THEN Auto
   THEN BLemma `append-nil-sqle`
   THEN Auto) }

---

Latex:

---

Latex:

1.  l  :  Base
2.  (evalall(l  @  []))\mdownarrow{}
\mvdash{}  evalall(l  @  [])  \mleq{}  l


By

---

Latex:
((InstLemma  `evalall-sqle`  [\mkleeneopen{}l  @  []\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SqLeTrans  (-1)
  THEN  Auto
  THEN  BLemma  `append-nil-sqle`
  THEN  Auto)

---

Home Index