---

Step * of Lemma map-concat

∀[f:Top]. ∀[L:Top List].  (map(f;concat(L)) ~ concat(map(λl.map(f;l);L)))
BY
{ InductionOnList }

1
1. f : Top
⊢ map(f;concat([])) ~ concat(map(λl.map(f;l);[]))

2
1. f : Top
2. u : Top
3. v : Top List
4. map(f;concat(v)) ~ concat(map(λl.map(f;l);v))
⊢ map(f;concat([u / v])) ~ concat(map(λl.map(f;l);[u / v]))

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[L:Top  List].    (map(f;concat(L))  \msim{}  concat(map(\mlambda{}l.map(f;l);L)))


By

---

Latex:
InductionOnList

---

Home Index