---

Step * 1 of Lemma bag-member-empty


1. T : Type
2. x : T
3. L : T List
4. L = {} ∈ bag(T)
5. (x ∈ L)
6. #(L) = 0 ∈ ℤ
⊢ False
BY
{ (DVar `L' THEN RepUR ``bag-size`` -1 THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  L  :  T  List
4.  L  =  \{\}
5.  (x  \mmember{}  L)
6.  \#(L)  =  0
\mvdash{}  False


By

---

Latex:
(DVar  `L'  THEN  RepUR  ``bag-size``  -1  THEN  Auto')

---

Home Index