---

Step * 2 1 of Lemma es-info-mk-msg


1. f : Name ─→ Type
2. es : EO+(Message(f))
3. e : E
4. auth : 𝔹
5. hdr : Name
6. v : f hdr
7. header(e) = hdr ∈ Name
⊢ msg-type(info(e);f) ⊆r (f hdr)
BY
{ (Unfold `msg-type` 0 THEN Fold `es-header` 0) }

1
1. f : Name ─→ Type
2. es : EO+(Message(f))
3. e : E
4. auth : 𝔹
5. hdr : Name
6. v : f hdr
7. header(e) = hdr ∈ Name
⊢ (f header(e)) ⊆r (f hdr)

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  es  :  EO+(Message(f))
3.  e  :  E
4.  auth  :  \mBbbB{}
5.  hdr  :  Name
6.  v  :  f  hdr
7.  header(e)  =  hdr
\mvdash{}  msg-type(info(e);f)  \msubseteq{}r  (f  hdr)


By

---

Latex:
(Unfold  `msg-type`  0  THEN  Fold  `es-header`  0)

---

Home Index