---

Step * of Lemma es-info-make-Msg-iff2

∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:f hdr].
  uiff(make-Msg(hdr;v) = info(e) ∈ Message(f);es-authentic(es;e) = ff
  ∧ (header(e) = hdr ∈ Name)
  ∧ (msgval(e) = v ∈ (f hdr)))
BY
{ (InstLemma `es-info-make-Msg-iff` [] THEN Folds ``es-info-body es-authentic`` (-1) THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `es-info-make-Msg-iff`  []  THEN  Folds  ``es-info-body  es-authentic``  (-1)  THEN  Trivial)

---

Home Index