---

Step * 1 of Lemma bag-member-append


1. T : Type
2. x : T
3. as : T List
4. bs : T List
5. x ↓∈ as @ bs
⊢ ↓x ↓∈ as ∨ x ↓∈ bs
BY
{ (D -1 THEN ExRepD)⋅ }

1
1. T : Type
2. x : T
3. as : T List
4. bs : T List
5. L : T List
6. L = (as @ bs) ∈ bag(T)
7. (x ∈ L)
⊢ ↓x ↓∈ as ∨ x ↓∈ bs

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  as  :  T  List
4.  bs  :  T  List
5.  x  \mdownarrow{}\mmember{}  as  @  bs
\mvdash{}  \mdownarrow{}x  \mdownarrow{}\mmember{}  as  \mvee{}  x  \mdownarrow{}\mmember{}  bs


By

---

Latex:
(D  -1  THEN  ExRepD)\mcdot{}

---

Home Index