---

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


1. T : Type
2. x : T
3. bag-union([]) = {x} ∈ bag(T)
⊢ ↓∃bbs':bag(bag(T)). (([] = {x}.bbs' ∈ bag(bag(T))) ∧ (bag-union(bbs') = {} ∈ bag(T)))
BY
{ (Assert ⌜False⌝⋅
   THEN Auto
   THEN RepUR ``bag-union single-bag`` (-1)⋅
   THEN (EqTypeHD (-1) THENA Auto)
   THEN (FLemma `permutation-length` [-1] THENA Auto)
   THEN Reduce (-1)
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  RepUR  ``bag-union  single-bag``  (-1)\mcdot{}
  THEN  (EqTypeHD  (-1)  THENA  Auto)
  THEN  (FLemma  `permutation-length`  [-1]  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index