---

Step * 1 of Lemma comm-msg_wf

.....wf..... 
1. M : Type ─→ Type
2. c : pCom(P.M[P])
⊢ c ∈ "msg":pMsg(P.M[P])
BY
{ (RepUR ``pCom pMsg Com tagged+`` -1 THEN Isect2HD (-1) THEN RepUR ``pMsg`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  M  :  Type  {}\mrightarrow{}  Type
2.  c  :  pCom(P.M[P])
\mvdash{}  c  \mmember{}  "msg":pMsg(P.M[P])


By

---

Latex:
(RepUR  ``pCom  pMsg  Com  tagged+``  -1  THEN  Isect2HD  (-1)  THEN  RepUR  ``pMsg``  0  THEN  Auto)

---

Home Index