---

Step * of Lemma map-length

∀[f,as:Top].  (||map(f;as)|| ~ ||as||)
BY
{ ListIndSq `as' }

---

Latex:

---

Latex:
\mforall{}[f,as:Top].    (||map(f;as)||  \msim{}  ||as||)


By

---

Latex:
ListIndSq  `as'

---

Home Index