---

Step * of Lemma bag-append-union

∀[T:Type]. ∀as,bs:bag(bag(T)).  (bag-union(as + bs) = (bag-union(as) + bag-union(bs)) ∈ bag(T))
BY
{ ((Auto THEN BagD 2)
   THEN Auto
   THEN Assert ⌜as = v1 ∈ bag(bag(T))⌝⋅
   THEN Auto
   THEN RevHypSubst' (-1) 0
   THEN Auto
   THEN ThinVar `v1') }

1
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)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}as,bs:bag(bag(T)).    (bag-union(as  +  bs)  =  (bag-union(as)  +  bag-union(bs)))


By

---

Latex:
((Auto  THEN  BagD  2)
  THEN  Auto
  THEN  Assert  \mkleeneopen{}as  =  v1\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  RevHypSubst'  (-1)  0
  THEN  Auto
  THEN  ThinVar  `v1')

---

Home Index