---

Step * of Lemma command-to-msg_wf

∀[M:Type ⟶ Type]. ∀[c:pCom(P.M[P])]. ∀[nmsg,lmsg:pMsg(P.M[P])].  (command-to-msg(c;nmsg;lmsg) ∈ pMsg(P.M[P]))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[c:pCom(P.M[P])].  \mforall{}[nmsg,lmsg:pMsg(P.M[P])].
    (command-to-msg(c;nmsg;lmsg)  \mmember{}  pMsg(P.M[P]))


By

---

Latex:
ProveWfLemma

---

Home Index