---

Step * 1 1 of Lemma bag-no-repeats-cons


1. T : Type
2. b : bag(T)
3. x : T
4. bag-no-repeats(T;b)
5. ¬x ↓∈ b
6. bag-no-repeats(T;{x})
7. bag-no-repeats(T;b)
8. x1 : T
9. x1 ↓∈ {x}
⊢ ¬x1 ↓∈ b
BY
{ BagMemberD (-1) }

1
1. T : Type
2. b : bag(T)
3. x : T
4. bag-no-repeats(T;b)
5. ¬x ↓∈ b
6. bag-no-repeats(T;{x})
7. bag-no-repeats(T;b)
8. x1 : T
9. x1 = x ∈ T
⊢ ¬x1 ↓∈ b

---

Latex:

---

Latex:

1.  T  :  Type
2.  b  :  bag(T)
3.  x  :  T
4.  bag-no-repeats(T;b)
5.  \mneg{}x  \mdownarrow{}\mmember{}  b
6.  bag-no-repeats(T;\{x\})
7.  bag-no-repeats(T;b)
8.  x1  :  T
9.  x1  \mdownarrow{}\mmember{}  \{x\}
\mvdash{}  \mneg{}x1  \mdownarrow{}\mmember{}  b


By

---

Latex:
BagMemberD  (-1)

---

Home Index