---

Step * 1 of Lemma map-id-map


1. as : Top
2. f : Top
⊢ map((λx.x) o f;as) ~ map(f;as)
BY
{ (RepUR ``map compose`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  as  :  Top
2.  f  :  Top
\mvdash{}  map((\mlambda{}x.x)  o  f;as)  \msim{}  map(f;as)


By

---

Latex:
(RepUR  ``map  compose``  0  THEN  Auto)

---

Home Index