---

Step * 2 1 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 = a ∈ |s|) ∨ (↑(a ∈b v)) ⇐⇒ (b2i(u (=b) a) + (a #∈ v)) > 0
BY
{ (((((RWH (HypC (-1)) 0 THENA Auto) THEN Thin (-1)) THEN Unfold `b2i` 0) THEN (SplitOnConclITE THENA Auto))
   THEN (GenUnivCD THENA Auto)
   THEN Try (Complete (Auto))) }

1
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

---

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{}  (u  =  a)  \mvee{}  (\muparrow{}(a  \mmember{}\msubb{}  v))  \mLeftarrow{}{}\mRightarrow{}  (b2i(u  (=\msubb{})  a)  +  (a  \#\mmember{}  v))  >  0


By

---

Latex:
(((((RWH  (HypC  (-1))  0  THENA  Auto)  THEN  Thin  (-1))  THEN  Unfold  `b2i`  0)
    THEN  (SplitOnConclITE  THENA  Auto)
    )
  THEN  (GenUnivCD  THENA  Auto)
  THEN  Try  (Complete  (Auto)))

---

Home Index