---

Step * of Lemma mset_wf

∀s:DSet. (MSet{s} ∈ Type)
BY
{ Unfold `mset` 0 
THEN ((D 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s:DSet.  (MSet\{s\}  \mmember{}  Type)


By

---

Latex:
Unfold  `mset`  0 
THEN  ((D  0)  THEN  Auto)

---

Home Index