---

Step * of Lemma base-noloc-classrel-make-Msg2

∀[T:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:T].
  uiff(v ∈ Base(hdr)(e);info(e) = mk-msg(msg-authentic(info(e));hdr;v) ∈ Message(f)) supposing T = (f hdr) ∈ Type
BY
{ ((UnivCD THENA Auto) THEN InstLemma `base-noloc-classrel-make-Msg` [⌜f⌝;⌜es⌝;⌜e⌝;⌜hdr⌝;⌜v⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[hdr:Name].  \mforall{}[v:T].
    uiff(v  \mmember{}  Base(hdr)(e);info(e)  =  mk-msg(msg-authentic(info(e));hdr;v))  supposing  T  =  (f  hdr)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  InstLemma  `base-noloc-classrel-make-Msg`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index