---

Step * 1 of Lemma mset_mon_wf


1. s : DSet@i'
⊢ mset_mon{s} ∈ AbMon
BY
{ Unfold `mset_mon` 0 
THEN ((BLemma `mk_abmonoid`) THEN Auto) }

1
1. s : DSet@i'
⊢ Ident(MSet{s};λx,y. (x + y);0{s})

---

Latex:

---

Latex:

1.  s  :  DSet@i'
\mvdash{}  mset\_mon\{s\}  \mmember{}  AbMon


By

---

Latex:
Unfold  `mset\_mon`  0 
THEN  ((BLemma  `mk\_abmonoid`)  THEN  Auto)

---

Home Index