---

Step * of Lemma msg-body_wf2

∀[f:Name ─→ Type]. ∀[m:Message(f)]. ∀[T:Type].  msg-body(m) ∈ T supposing msg-type(m;f) ⊆r T
BY
{ (ProveWfLemma THEN (RepUR ``msg-type msg-header`` (-1) THEN AllReduce THEN Auto)⋅) }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma  THEN  (RepUR  ``msg-type  msg-header``  (-1)  THEN  AllReduce  THEN  Auto)\mcdot{})

---

Home Index