---

Step * of Lemma mset_union_mon_wf

∀s:DSet. (<MSet{s},⋃,0> ∈ AbMon)
BY
{ ((Unfold `mset_union_mon` 0 
THENM RepD THENM BLemma `mk_abmonoid`) THEN Auto) }

1
1. s : DSet@i'
⊢ Assoc(MSet{s};λx,y. (x ⋃ y))

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

3
1. s : DSet@i'
⊢ Comm(MSet{s};λx,y. (x ⋃ y))

---

Latex:

---

Latex:
\mforall{}s:DSet.  (<MSet\{s\},\mcup{},0>  \mmember{}  AbMon)


By

---

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

---

Home Index