---

Step * 2 of Lemma bag-union-is-single


1. T : Type
2. x : T
3. bbs : bag(bag(T))
4. ∃bbs':bag(bag(T)). ((bbs = {x}.bbs' ∈ bag(bag(T))) ∧ (bag-union(bbs') = {} ∈ bag(T)))
⊢ bag-union(bbs) = {x} ∈ bag(T)
BY
{ (SquashExRepD
   THEN (HypSubst' (-2) 0 THENA Auto)
   THEN (BagToList (-3) THENA Auto)
   THEN RepUR ``single-bag cons-bag bag-union`` 0
   THEN (RWO "concat-cons2" 0 THENA Auto)
   THEN Try (Fold `bag-union` 0⋅)
   THEN Try (Fold `bag-append` 0)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN Try (Fold `single-bag` 0⋅)
   THEN RWO "bag-append-empty" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  bbs  :  bag(bag(T))
4.  \mexists{}bbs':bag(bag(T)).  ((bbs  =  \{x\}.bbs')  \mwedge{}  (bag-union(bbs')  =  \{\}))
\mvdash{}  bag-union(bbs)  =  \{x\}


By

---

Latex:
(SquashExRepD
  THEN  (HypSubst'  (-2)  0  THENA  Auto)
  THEN  (BagToList  (-3)  THENA  Auto)
  THEN  RepUR  ``single-bag  cons-bag  bag-union``  0
  THEN  (RWO  "concat-cons2"  0  THENA  Auto)
  THEN  Try  (Fold  `bag-union`  0\mcdot{})
  THEN  Try  (Fold  `bag-append`  0)
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  Try  (Fold  `single-bag`  0\mcdot{})
  THEN  RWO  "bag-append-empty"  0
  THEN  Auto)

---

Home Index