---

Step * of Lemma map_append_sq

∀[f,a,b:Top].  (map(f;a @ b) ~ map(f;a) @ map(f;b))
BY
{ ListIndSq `a' }

---

Latex:

---

Latex:
\mforall{}[f,a,b:Top].    (map(f;a  @  b)  \msim{}  map(f;a)  @  map(f;b))


By

---

Latex:
ListIndSq  `a'

---

Home Index