---

Step * of Lemma map-id-map

∀[as,f:Top].  (map(λx.x;map(f;as)) ~ map(f;as))
BY
{ TACTIC:((UnivCD THENA Auto) THEN (RWO "map-map" 0 THENA Auto)) }

1
1. as : Top
2. f : Top
⊢ map((λx.x) o f;as) ~ map(f;as)

---

Latex:

---

Latex:
\mforall{}[as,f:Top].    (map(\mlambda{}x.x;map(f;as))  \msim{}  map(f;as))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  (RWO  "map-map"  0  THENA  Auto))

---

Home Index