---

Step * of Lemma comm-msg_wf

∀[M:Type ─→ Type]. ∀[c:pCom(P.M[P])].  comm-msg(c) ∈ pMsg(P.M[P]) supposing com-kind(c) = "msg" ∈ Atom
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN (GenConcl ⌈c = m ∈ "msg":pMsg(P.M[P])⌉⋅ THENA Auto)) }

1
.....wf..... 
1. M : Type ─→ Type
2. c : pCom(P.M[P])
⊢ c ∈ "msg":pMsg(P.M[P])

2
1. M : Type ─→ Type
2. c : pCom(P.M[P])
3. m : "msg":pMsg(P.M[P])@i
4. c = m ∈ "msg":pMsg(P.M[P])@i
⊢ comm-msg(m) ∈ pMsg(P.M[P]) supposing com-kind(m) = "msg" ∈ Atom

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[c:pCom(P.M[P])].    comm-msg(c)  \mmember{}  pMsg(P.M[P])  supposing  com-kind(c)  =  "msg"


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  (GenConcl  \mkleeneopen{}c  =  m\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index