---

Step * of Lemma list_acc_nil_red_lemma

∀b,f:Top.  (list-accum(t,a,h.f[t;a;h];b;[]) ~ b)
BY
{ (xxx(Unfold `list-accum` 0 THEN Reduce 0)xxx THEN Auto) }

---

Latex:

---

Latex:
\mforall{}b,f:Top.    (list-accum(t,a,h.f[t;a;h];b;[])  \msim{}  b)


By

---

Latex:
(xxx(Unfold  `list-accum`  0  THEN  Reduce  0)xxx  THEN  Auto)

---

Home Index