---

Step * of Lemma permr_iff_eq_counts_a

∀s:DSet. ∀as,bs:|s| List.  (as ≡(|s|) bs ⇐⇒ {∀x:|s|. ((x #∈ as) = (x #∈ bs) ∈ ℤ)})
BY
{ (Unfold `guard` 0 THEN Lemma `permr_iff_eq_counts`) }

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}as,bs:|s|  List.    (as  \mequiv{}(|s|)  bs  \mLeftarrow{}{}\mRightarrow{}  \{\mforall{}x:|s|.  ((x  \#\mmember{}  as)  =  (x  \#\mmember{}  bs))\})


By

---

Latex:
(Unfold  `guard`  0  THEN  Lemma  `permr\_iff\_eq\_counts`)

---

Home Index