---

Step * 1 of Lemma mk_mset_wf2


1. s : DSet@i'
2. as : DisList{s}@i
3. ∀x:|s|. ((x #∈ as) ≤ 1)
4. x : |s|@i
⊢ (x #∈ mk_mset(as)) ≤ 1
BY
{ ((Unfolds ``mset_count mk_mset`` 0 
THEN BHyp 3) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet@i'
2.  as  :  DisList\{s\}@i
3.  \mforall{}x:|s|.  ((x  \#\mmember{}  as)  \mleq{}  1)
4.  x  :  |s|@i
\mvdash{}  (x  \#\mmember{}  mk\_mset(as))  \mleq{}  1


By

---

Latex:
((Unfolds  ``mset\_count  mk\_mset``  0 
THEN  BHyp  3)  THEN  Auto)

---

Home Index