---

Step * of Lemma empty-bag-union

∀[T:Type]. ∀[bbs:bag(bag(T))].  ∀bs:bag(T). (bs ↓∈ bbs ⇒ (bs = {} ∈ bag(T))) supposing bag-union(bbs) = {} ∈ bag(T)
BY
{ Auto }

1
1. T : Type
2. bbs : bag(bag(T))
3. bag-union(bbs) = {} ∈ bag(T)
4. bs : bag(T)@i
5. bs ↓∈ bbs@i
⊢ bs = {} ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bbs:bag(bag(T))].    \mforall{}bs:bag(T).  (bs  \mdownarrow{}\mmember{}  bbs  {}\mRightarrow{}  (bs  =  \{\}))  supposing  bag-union(bbs)  =  \{\}


By

---

Latex:
Auto

---

Home Index