---

Step * 1 of Lemma mset_mem_iff_count_nzero


1. s : DSet
2. x : |s|
3. a : MSet{s}
⊢ Ax = Ax ∈ (↓↑(x ∈b a) ⇐⇒ (x #∈ a) > 0)
BY
{ ((msetD 3 THENM EqTypeCD 
THENM Unfolds ``mset_mem mset_count`` 0) THENA Auto) }

1
1. s : DSet
2. x : |s|
3. as : |s| List
4. bs : |s| List
5. as ≡(|s|) bs
⊢ ↑(x ∈b as) ⇐⇒ (x #∈ as) > 0

---

Latex:

---

Latex:

1.  s  :  DSet
2.  x  :  |s|
3.  a  :  MSet\{s\}
\mvdash{}  Ax  =  Ax


By

---

Latex:
((msetD  3  THENM  EqTypeCD 
THENM  Unfolds  ``mset\_mem  mset\_count``  0)  THENA  Auto)

---

Home Index