---

Step * of Lemma msg-has-type-encodes

∀[f,m,T:Top].  (msg-has-type(m;f;T) ~ msg-header(m) encodes T)
BY
{ (Auto THEN RepUR ``msg-has-type msg-type encodes-msg-type`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f,m,T:Top].    (msg-has-type(m;f;T)  \msim{}  msg-header(m)  encodes  T)


By

---

Latex:
(Auto  THEN  RepUR  ``msg-has-type  msg-type  encodes-msg-type``  0  THEN  Auto)

---

Home Index