---

Step * of Lemma empty-bag-union

∀T:Type. ∀bs:bag(bag(T)).  ((bag-union(bs) = {} ∈ bag(T)) ⇒ (bs ~ bag-rep(#(bs);{})))
BY
{ Auto }

1
1. T : Type
2. bs : bag(bag(T))
3. bag-union(bs) = {} ∈ bag(T)
⊢ bs ~ bag-rep(#(bs);{})

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}bs:bag(bag(T)).    ((bag-union(bs)  =  \{\})  {}\mRightarrow{}  (bs  \msim{}  bag-rep(\#(bs);\{\})))


By

---

Latex:
Auto

---

Home Index