---

Step * of Lemma bag-union_wf

∀[T:Type]. ∀[bbs:bag(bag(T))].  (bag-union(bbs) ∈ bag(T))
BY
{ ((UnivCD THENA Auto) THEN BagD (-1) THEN Auto THEN Unfold `bag-union` 0) }

1
1. T : Type
2. as : bag(T) List
3. bs : bag(T) List
4. permutation(bag(T);as;bs)
⊢ concat(as) = concat(bs) ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bbs:bag(bag(T))].    (bag-union(bbs)  \mmember{}  bag(T))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  BagD  (-1)  THEN  Auto  THEN  Unfold  `bag-union`  0)

---

Home Index