---

Step * 1 of Lemma bag-filter-map


1. f : Top
2. p : Top
3. as : Top
⊢ (λx.p[x]) o f ~ λx.p[f x]
BY
{ (RepUR ``compose`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Top
2.  p  :  Top
3.  as  :  Top
\mvdash{}  (\mlambda{}x.p[x])  o  f  \msim{}  \mlambda{}x.p[f  x]


By

---

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

---

Home Index