---

Step * 1 2 of Lemma bag-append-union


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)
BY
{ (Fold `bag-append` 0 THEN HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:

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))
\mvdash{}  (u  @  bag-union(v  @  bs))  =  ((u  @  bag-union(v))  @  bag-union(bs))


By

---

Latex:
(Fold  `bag-append`  0  THEN  HypSubst'  (-1)  0  THEN  Auto)

---

Home Index