---

Step * 2 1 1 of Lemma mem_iff_count_nzero


1. s : DSet
2. a : |s|
3. u : |s|
4. v : |s| List
5. ¬(u = a ∈ |s|)
6. (u = a ∈ |s|) ∨ ((a #∈ v) > 0)
⊢ (0 + (a #∈ v)) > 0
BY
{ (D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a  :  |s|
3.  u  :  |s|
4.  v  :  |s|  List
5.  \mneg{}(u  =  a)
6.  (u  =  a)  \mvee{}  ((a  \#\mmember{}  v)  >  0)
\mvdash{}  (0  +  (a  \#\mmember{}  v))  >  0


By

---

Latex:
(D  -1  THEN  Auto)

---

Home Index