---

Step * of Lemma es-info-body-equal

∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e,e':E]. ∀[T:Type].
  (msgval(e) = msgval(e') ∈ T) supposing ((e = e' ∈ E) and ((f header(e)) ⊆r T))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e,e':E].  \mforall{}[T:Type].
    (msgval(e)  =  msgval(e'))  supposing  ((e  =  e')  and  ((f  header(e))  \msubseteq{}r  T))


By

---

Latex:
Auto

---

Home Index