---

Step * of Lemma filter-as-mapfilter

∀[L,P:Top].  (filter(P;L) ~ mapfilter(λx.x;P;L))
BY
{ (Unfold `mapfilter` 0 THEN (ListIndSq `L' THEN RWO "map-ifthenelse" 0 THEN Reduce 0 THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[L,P:Top].    (filter(P;L)  \msim{}  mapfilter(\mlambda{}x.x;P;L))


By

---

Latex:
(Unfold  `mapfilter`  0  THEN  (ListIndSq  `L'  THEN  RWO  "map-ifthenelse"  0  THEN  Reduce  0  THEN  Auto))

---

Home Index