---

Step * of Lemma bag-union-as-combine

∀[A:Type]. ∀[x:bag(bag(A))].  (bag-union(x) = ⋃b∈x.b ∈ bag(A))
BY
{ xxxAutoxxx }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[x:bag(bag(A))].    (bag-union(x)  =  \mcup{}b\mmember{}x.b)


By

---

Latex:
xxxAutoxxx

---

Home Index