---

Step * of Lemma bag-combine-single-left

∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[a:A].  (⋃x∈{a}.f[x] ~ f[a])
BY
{ (InstLemma `bag-combine-unit-left` [] THEN Fold `single-bag` (-1) THEN Trivial) }

---

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:
(InstLemma  `bag-combine-unit-left`  []  THEN  Fold  `single-bag`  (-1)  THEN  Trivial)

---

Home Index