---

Step * 1 of Lemma mset_inj_wf_f


1. s : DSet
2. x : |s|
3. x@0 : |s|
⊢ (x@0 #∈ mset_inj{s}(x)) ≤ 1
BY
{ (RepUR ``mset_inj mset_count count mk_mset b2i`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  x  :  |s|
3.  x@0  :  |s|
\mvdash{}  (x@0  \#\mmember{}  mset\_inj\{s\}(x))  \mleq{}  1


By

---

Latex:
(RepUR  ``mset\_inj  mset\_count  count  mk\_mset  b2i``  0  THEN  AutoSplit)

---

Home Index