Step * of Lemma has-valueall-append-nil

[l:Base]. [] supposing has-valueall(l [])
BY
((UnivCD THENA Auto)
   THEN Unfold `has-valueall` -1
   THEN (InstLemma `evalall-sqequal` [⌜[]⌝]⋅ 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