---

Step * 1 2 1 2 1 of Lemma bag-member-union


1. T : Type
2. x : T
3. u : bag(T)
4. v : bag(T) List
5. x ↓∈ bag-union(v)
6. b : bag(T)
7. x ↓∈ b
8. b ↓∈ v
9. x ↓∈ b
⊢ b ↓∈ [u / v]
BY
{ (BagMemberD 0 THEN D 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  u  :  bag(T)
4.  v  :  bag(T)  List
5.  x  \mdownarrow{}\mmember{}  bag-union(v)
6.  b  :  bag(T)
7.  x  \mdownarrow{}\mmember{}  b
8.  b  \mdownarrow{}\mmember{}  v
9.  x  \mdownarrow{}\mmember{}  b
\mvdash{}  b  \mdownarrow{}\mmember{}  [u  /  v]


By

---

Latex:
(BagMemberD  0  THEN  D  0  THEN  Auto)\mcdot{}

---

Home Index