---

Step * of Lemma map-append-empty

∀[f,b:Top].  (map(f;b) @ [] ~ map(f;b))
BY
{ ListIndSq `b' }

---

Latex:

---

Latex:
\mforall{}[f,b:Top].    (map(f;b)  @  []  \msim{}  map(f;b))


By

---

Latex:
ListIndSq  `b'

---

Home Index