---

Step * of Lemma filter-concat

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

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

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

---

Latex:

---

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


By

---

Latex:
InductionOnList

---

Home Index