---

Step * of Lemma map-is-top-list

∀[f:Top]. ∀[L:Top List].  (map(f;L) ∈ Top List)
BY
{ xxx((InductionOnList THEN Reduce 0) THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[L:Top  List].    (map(f;L)  \mmember{}  Top  List)


By

---

Latex:
xxx((InductionOnList  THEN  Reduce  0)  THEN  Auto)xxx

---

Home Index