---

Step * of Lemma mset_count_inj

∀s:DSet. ∀a,x:|s|.  ((x #∈ mset_inj{s}(a)) = b2i(a (=b) x) ∈ ℤ)
BY
{ ((RepD) THENA Auto) }

1
1. s : DSet
2. a : |s|
3. x : |s|
⊢ (x #∈ mset_inj{s}(a)) = b2i(a (=b) x) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a,x:|s|.    ((x  \#\mmember{}  mset\_inj\{s\}(a))  =  b2i(a  (=\msubb{})  x))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index