---

Step * of Lemma bag-accum-map

∀[L,y,f,g:Top].  (bag-accum(x,a.f[x;a];y;bag-map(g;L)) ~ bag-accum(x,a.f[x;g a];y;L))
BY
{ (InstLemma `list_accum-map` [] THEN Fold `bag-map` (-1) THEN Fold `bag-accum` (-1) THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[L,y,f,g:Top].    (bag-accum(x,a.f[x;a];y;bag-map(g;L))  \msim{}  bag-accum(x,a.f[x;g  a];y;L))


By

---

Latex:
(InstLemma  `list\_accum-map`  []  THEN  Fold  `bag-map`  (-1)  THEN  Fold  `bag-accum`  (-1)  THEN  Trivial)

---

Home Index