---

Step * 1 of Lemma bag-member-union


1. T : Type
2. x : T
3. bbs : bag(T) List
⊢ uiff(x ↓∈ bag-union(bbs);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ bbs))
BY
{ (ListInd (-1) THEN Reduce 0) }

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

2
1. T : Type
2. x : T
3. u : bag(T)
4. v : bag(T) List
5. uiff(x ↓∈ bag-union(v);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ v))
⊢ uiff(x ↓∈ bag-union([u / v]);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ [u / v]))

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  bbs  :  bag(T)  List
\mvdash{}  uiff(x  \mdownarrow{}\mmember{}  bag-union(bbs);\mdownarrow{}\mexists{}b:bag(T).  (x  \mdownarrow{}\mmember{}  b  \mwedge{}  b  \mdownarrow{}\mmember{}  bbs))


By

---

Latex:
(ListInd  (-1)  THEN  Reduce  0)

---

Home Index