---

Step * 1 1 1 1 of Lemma bag-map-union


1. T : Type
2. S : Type
3. f : T ⟶ bag(S)
⊢ bag-union(bag-map(λb.bag-map(f;b);[])) ~ bag-map(f;bag-union([]))
BY
{ (RepUR ``bag-union bag-map`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  Type
3.  f  :  T  {}\mrightarrow{}  bag(S)
\mvdash{}  bag-union(bag-map(\mlambda{}b.bag-map(f;b);[]))  \msim{}  bag-map(f;bag-union([]))


By

---

Latex:
(RepUR  ``bag-union  bag-map``  0  THEN  Auto)

---

Home Index