Step
*
2
of Lemma
es-info-make-Msg
1. f : Name ─→ Type
2. es : EO+(Message(f))
3. e : E
4. hdr : Name
5. v : f hdr
6. header(e) = hdr ∈ Name
⊢ (msg-body(info(e)) = v ∈ (f hdr)) = (msg-body(info(e)) = v ∈ (f hdr)) ∈ Type
BY
{ (EqCD THEN Auto) }
1
1. f : Name ─→ Type
2. es : EO+(Message(f))
3. e : E
4. hdr : Name
5. v : f hdr
6. header(e) = hdr ∈ Name
⊢ msg-type(info(e);f) ⊆r (f hdr)
Latex:
Latex:
1.  f  :  Name  {}\mrightarrow{}  Type
2.  es  :  EO+(Message(f))
3.  e  :  E
4.  hdr  :  Name
5.  v  :  f  hdr
6.  header(e)  =  hdr
\mvdash{}  (msg-body(info(e))  =  v)  =  (msg-body(info(e))  =  v)
By
Latex:
(EqCD  THEN  Auto)
Home
Index