---

Step * of Lemma map-as-mapfilter

∀[f:Top]. ∀[L:Top List].  (map(f;L) ~ mapfilter(f;λx.tt;L))
BY
{ (Unfold `mapfilter` 0 THEN InductionOnList THEN Reduce 0 THEN EqCD THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[L:Top  List].    (map(f;L)  \msim{}  mapfilter(f;\mlambda{}x.tt;L))


By

---

Latex:
(Unfold  `mapfilter`  0  THEN  InductionOnList  THEN  Reduce  0  THEN  EqCD  THEN  Trivial)

---

Home Index