---

Step * of Lemma msg-body_wf

∀[f:Name ⟶ Type]. ∀[m:Message(f)].  (msg-body(m) ∈ msg-type(m;f))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``msg-type msg-header msg-body`` 0 THEN D (-1) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[m:Message(f)].    (msg-body(m)  \mmember{}  msg-type(m;f))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``msg-type  msg-header  msg-body``  0
  THEN  D  (-1)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index