---

Step * of Lemma bag-combine-unit-left

∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[a:A].  (⋃x∈[a].f[x] ~ f[a])
BY
{ (Auto
   THEN RepUR ``bag-combine bag-map bag-union concat`` 0
   THEN Folds ``bag-append empty-bag`` 0
   THEN RWO "bag-append-empty" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[a:A].    (\mcup{}x\mmember{}[a].f[x]  \msim{}  f[a])


By

---

Latex:
(Auto
  THEN  RepUR  ``bag-combine  bag-map  bag-union  concat``  0
  THEN  Folds  ``bag-append  empty-bag``  0
  THEN  RWO  "bag-append-empty"  0
  THEN  Auto)

---

Home Index