∀s:DSet. (<MSet{s},⋃,0> ∈ AbMon)
{ ((Unfold `mset_union_mon` 0
THENM RepD THENM BLemma `mk_abmonoid`) THEN Auto) }
1. s : DSet@i'
⊢ Assoc(MSet{s};λx,y. (x ⋃ y))
1. s : DSet@i'
⊢ Ident(MSet{s};λx,y. (x ⋃ y);0{s})
1. s : DSet@i'
⊢ Comm(MSet{s};λx,y. (x ⋃ y))