---

Step * of Lemma non_neg_mset_size

∀s:DSet. ∀a:MSet{s}.  (size{s}(a) ≥ 0 )
BY
{ ((RepD 
THENM CSquash 
THENM UseEqWitness Ax 
THENM OnVar `a' msetD 
THENM EqTypeCD) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a:MSet\{s\}.    (size\{s\}(a)  \mgeq{}  0  )


By

---

Latex:
((RepD 
THENM  CSquash 
THENM  UseEqWitness  Ax 
THENM  OnVar  `a'  msetD 
THENM  EqTypeCD)  THEN  Auto)

---

Home Index