---

Step * 2 3 1 of Lemma bag-append-no-repeats


1. T : Type
2. as : T List
3. bs : T List
4. bag-no-repeats(T;as + bs)
5. z : T
6. z ↓∈ as
⊢ ¬z ↓∈ bs
BY
{ (Unfold `bag-append` -3 THEN D -3 THEN Auto THEN ExRepD THEN D 0 THEN Auto)⋅ }

1
1. T : Type
2. as : T List
3. bs : T List
4. L : T List
5. L = (as @ bs) ∈ bag(T)
6. no_repeats(T;L)
7. z : T
8. z ↓∈ as
9. z ↓∈ bs
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  bag-no-repeats(T;as  +  bs)
5.  z  :  T
6.  z  \mdownarrow{}\mmember{}  as
\mvdash{}  \mneg{}z  \mdownarrow{}\mmember{}  bs


By

---

Latex:
(Unfold  `bag-append`  -3  THEN  D  -3  THEN  Auto  THEN  ExRepD  THEN  D  0  THEN  Auto)\mcdot{}

---

Home Index