---

Step * 2 of Lemma mem_iff_count_nzero


1. s : DSet
2. a : |s|
3. u : |s|
4. v : |s| List
5. ↑(a ∈b v) ⇐⇒ (a #∈ v) > 0
⊢ ↑((u (=b) a) ∨b(a ∈b v)) ⇐⇒ (b2i(u (=b) a) + (a #∈ v)) > 0
BY
{ (RW bool_to_propC 0 THENA Auto) }

1
1. s : DSet
2. a : |s|
3. u : |s|
4. v : |s| List
5. ↑(a ∈b v) ⇐⇒ (a #∈ v) > 0
⊢ (u = a ∈ |s|) ∨ (↑(a ∈b v)) ⇐⇒ (b2i(u (=b) a) + (a #∈ v)) > 0

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a  :  |s|
3.  u  :  |s|
4.  v  :  |s|  List
5.  \muparrow{}(a  \mmember{}\msubb{}  v)  \mLeftarrow{}{}\mRightarrow{}  (a  \#\mmember{}  v)  >  0
\mvdash{}  \muparrow{}((u  (=\msubb{})  a)  \mvee{}\msubb{}(a  \mmember{}\msubb{}  v))  \mLeftarrow{}{}\mRightarrow{}  (b2i(u  (=\msubb{})  a)  +  (a  \#\mmember{}  v))  >  0


By

---

Latex:
(RW  bool\_to\_propC  0  THENA  Auto)

---

Home Index