---

Step * of Lemma has-valueall-append-nil

∀[l:Base]. l @ [] ~ l supposing has-valueall(l @ [])
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `has-valueall` -1
   THEN (InstLemma `evalall-sqequal` [⌜l @ []⌝]⋅ THENA Auto)
   THEN RWO "evalall-append-nil" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[l:Base].  l  @  []  \msim{}  l  supposing  has-valueall(l  @  [])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `has-valueall`  -1
  THEN  (InstLemma  `evalall-sqequal`  [\mkleeneopen{}l  @  []\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "evalall-append-nil"  (-1)
  THEN  Auto)

---

Home Index