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