---

Step * of Lemma csm-msgtype_wf

∀[V:Type]. ∀[sm:CSM(V)].  (Msg(sm) ∈ Type)
BY
{ ((Auto THEN RepeatFor 2 (D -1)) THEN RepUR ``csm-msgtype`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[V:Type].  \mforall{}[sm:CSM(V)].    (Msg(sm)  \mmember{}  Type)


By

---

Latex:
((Auto  THEN  RepeatFor  2  (D  -1))  THEN  RepUR  ``csm-msgtype``  0  THEN  Auto)\mcdot{}

---

Home Index