---

Step * of Lemma length-concat-map-single

∀[f,L:Top].  (||concat(map(λx.[f[x]];L))|| ~ ||L||)
BY
{ (RWW "concat-map-single map-length" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f,L:Top].    (||concat(map(\mlambda{}x.[f[x]];L))||  \msim{}  ||L||)


By

---

Latex:
(RWW  "concat-map-single  map-length"  0  THEN  Auto)

---

Home Index