---

Step * of Lemma mprime_ty_wf

∀g:GrpSig. (Prime(g) ∈ Type)
BY
{ ((Unfold `mprime_ty` 0) THEN Auto) 
 }

---

Latex:

---

Latex:
\mforall{}g:GrpSig.  (Prime(g)  \mmember{}  Type)


By

---

Latex:
((Unfold  `mprime\_ty`  0)  THEN  Auto) 

---

Home Index