---

Step * 1 of Lemma mset_count_wf


1. s : DSet
2. x : |s|
3. a : MSet{s}
⊢ x #∈ a ∈ ℕ
BY
{ Unfold `member` 0 THEN ((msetD 3) THENA Auto) }

1
1. s : DSet
2. x : |s|
3. as : |s| List
4. bs : |s| List
5. as ≡(|s|) bs
⊢ (x #∈ as) = (x #∈ bs) ∈ ℕ

---

Latex:

---

Latex:

1.  s  :  DSet
2.  x  :  |s|
3.  a  :  MSet\{s\}
\mvdash{}  x  \#\mmember{}  a  \mmember{}  \mBbbN{}


By

---

Latex:
Unfold  `member`  0  THEN  ((msetD  3)  THENA  Auto)

---

Home Index