---

Step * 1 of Lemma es-info-make-Msg-iff


1. f : Name ─→ Type
2. es : EO+(Message(f))
3. e : E
4. hdr : Name
5. v : f hdr
6. make-Msg(hdr;v) = info(e) ∈ Message(f)
⊢ msg-authentic(info(e)) = ff ∧ (header(e) = hdr ∈ Name) ∧ (msg-body(info(e)) = v ∈ (f hdr))
BY
{ (RepUR ``es-header`` 0⋅
   THEN (RevHypSubst' (-1) 0 THENA D (-1))
   THEN RepUR ``msg-header msg-body make-Msg`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  es  :  EO+(Message(f))
3.  e  :  E
4.  hdr  :  Name
5.  v  :  f  hdr
6.  make-Msg(hdr;v)  =  info(e)
\mvdash{}  msg-authentic(info(e))  =  ff  \mwedge{}  (header(e)  =  hdr)  \mwedge{}  (msg-body(info(e))  =  v)


By

---

Latex:
(RepUR  ``es-header``  0\mcdot{}
  THEN  (RevHypSubst'  (-1)  0  THENA  D  (-1))
  THEN  RepUR  ``msg-header  msg-body  make-Msg``  0
  THEN  Auto)

---

Home Index