---

Step * of Lemma list_accum_nil_lemma

∀z,f:Top.  (accumulate (with value x and list item y): f[x;y]over list:  []with starting value: z) ~ z)
BY
{ (xxx(RecUnfold `list_accum` 0 THEN Reduce 0)xxx THEN Auto) }

---

Latex:

---

Latex:
\mforall{}z,f:Top.
    (accumulate  (with  value  x  and  list  item  y):
        f[x;y]
      over  list:
          []
      with  starting  value:
        z)  \msim{}  z)


By

---

Latex:
(xxx(RecUnfold  `list\_accum`  0  THEN  Reduce  0)xxx  THEN  Auto)

---

Home Index