---

Step * 1 1 of Lemma mset_count_wf


1. s : DSet
2. x : |s|
3. as : |s| List
4. bs : |s| List
5. as ≡(|s|) bs
⊢ (x #∈ as) = (x #∈ bs) ∈ ℕ
BY
{ (((FLemma `permr_iff_eq_counts_a` [-1]) THENA Auto)  THEN Unfold `mset_count` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  x  :  |s|
3.  as  :  |s|  List
4.  bs  :  |s|  List
5.  as  \mequiv{}(|s|)  bs
\mvdash{}  (x  \#\mmember{}  as)  =  (x  \#\mmember{}  bs)


By

---

Latex:
(((FLemma  `permr\_iff\_eq\_counts\_a`  [-1])  THENA  Auto)    THEN  Unfold  `mset\_count`  0  THEN  Auto)

---

Home Index