---

Step * 2 3 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. bag-no-repeats(T;as)
6. bag-no-repeats(T;bs)
7. z : T
8. z ↓∈ as
⊢ ¬z ↓∈ bs
BY
{ RepeatFor 2 (Thin (-3)) }

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
RepeatFor  2  (Thin  (-3))

---

Home Index