---

Step * 1 1 of Lemma mset_mon_wf


1. s : DSet@i'
⊢ Ident(MSet{s};λx,y. (x + y);0{s})
BY
{ AbEval ``ident mset_sum null_mset`` 0 
THEN ((GenUnivCD) THENA Auto) }

1
1. s : DSet@i'
2. x : MSet{s}
⊢ (x @ []) = x ∈ MSet{s}

---

Latex:

---

Latex:

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


By

---

Latex:
AbEval  ``ident  mset\_sum  null\_mset``  0 
THEN  ((GenUnivCD)  THENA  Auto)

---

Home Index