---

Step * 1 of Lemma bag-append-union


1. T : Type
2. bs : bag(bag(T))
3. as : bag(T) List
⊢ bag-union(as + bs) = (bag-union(as) + bag-union(bs)) ∈ bag(T)
BY
{ (ListInd (-1) THEN RepUR ``bag-append bag-union concat`` 0 THEN Fold `concat` 0 THEN Fold `bag-union` 0) }

1
1. T : Type
2. bs : bag(bag(T))
⊢ bag-union(bs) = bag-union(bs) ∈ bag(T)

2
1. T : Type
2. bs : bag(bag(T))
3. u : bag(T)
4. v : bag(T) List
5. bag-union(v + bs) = (bag-union(v) + bag-union(bs)) ∈ bag(T)
⊢ (u @ bag-union(v @ bs)) = ((u @ bag-union(v)) @ bag-union(bs)) ∈ bag(T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  bag(bag(T))
3.  as  :  bag(T)  List
\mvdash{}  bag-union(as  +  bs)  =  (bag-union(as)  +  bag-union(bs))


By

---

Latex:
(ListInd  (-1)
  THEN  RepUR  ``bag-append  bag-union  concat``  0
  THEN  Fold  `concat`  0
  THEN  Fold  `bag-union`  0)

---

Home Index