---

Step * of Lemma bag-member-union

∀[T:Type]. ∀[x:T]. ∀[bbs:bag(bag(T))].  uiff(x ↓∈ bag-union(bbs);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ bbs))
BY
{ ((UnivCD THENA Auto) THEN (BagToList (-1) THENA Auto)) }

1
1. T : Type
2. x : T
3. bbs : bag(T) List
⊢ uiff(x ↓∈ bag-union(bbs);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ bbs))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[bbs:bag(bag(T))].    uiff(x  \mdownarrow{}\mmember{}  bag-union(bbs);\mdownarrow{}\mexists{}b:bag(T).  (x  \mdownarrow{}\mmember{}  b  \mwedge{}  b  \mdownarrow{}\mmember{}  bbs))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (BagToList  (-1)  THENA  Auto))

---

Home Index