---

Step * of Lemma reduce-append

∀[f,k,as,bs:Top].  (reduce(f;k;as @ bs) ~ reduce(f;reduce(f;k;bs);as))
BY
{ ListIndSq `as' }

---

Latex:

---

Latex:
\mforall{}[f,k,as,bs:Top].    (reduce(f;k;as  @  bs)  \msim{}  reduce(f;reduce(f;k;bs);as))


By

---

Latex:
ListIndSq  `as'

---

Home Index