---

Step * of Lemma es-info-make-Msg

∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:f hdr].
  (make-Msg(hdr;v) = info(e) ∈ Message(f)) supposing 
     (msg-authentic(info(e)) = ff and 
     (msg-body(info(e)) = v ∈ (f hdr)) and 
     (header(e) = hdr ∈ Name))
BY
{ Intros }

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
7. msg-body(info(e)) = v ∈ (f hdr)
8. msg-authentic(info(e)) = ff
⊢ make-Msg(hdr;v) = info(e) ∈ Message(f)

2
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

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[hdr:Name].  \mforall{}[v:f  hdr].
    (make-Msg(hdr;v)  =  info(e))  supposing 
          (msg-authentic(info(e))  =  ff  and 
          (msg-body(info(e))  =  v)  and 
          (header(e)  =  hdr))


By

---

Latex:
Intros

---

Home Index