---

Step * of Lemma ma-msgtype_wf

∀[da:k:Knd fp-> Type]. ∀[k:Knd].  (Msgtype(da;k) ∈ Type)
BY
{ (Unfold `ma-msgtype` 0 THEN Auto) }

---

Latex:


\mforall{}[da:k:Knd  fp->  Type].  \mforall{}[k:Knd].    (Msgtype(da;k)  \mmember{}  Type)


By

(Unfold  `ma-msgtype`  0  THEN  Auto)

---

Home Index