---

Step * of Lemma Message-eta2

∀[f:Name ⟶ Type]. ∀[m:Message(f)].  (m = mk-msg(msg-authentic(m);msg-header(m);msg-body(m)) ∈ Message(f))
BY
{ (Auto
   THEN RepeatFor 2 (D -1)
   THEN RepUR ``Message basicMessage make-Msg make-Authentic-Msg`` 0
   THEN RepUR ``msg-authentic msg-header msg-body msg-msg`` 0
   THEN AutoBoolCase ⌜m1⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[m:Message(f)].    (m  =  mk-msg(msg-authentic(m);msg-header(m);msg-body(m)))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -1)
  THEN  RepUR  ``Message  basicMessage  make-Msg  make-Authentic-Msg``  0
  THEN  RepUR  ``msg-authentic  msg-header  msg-body  msg-msg``  0
  THEN  AutoBoolCase  \mkleeneopen{}m1\mkleeneclose{}\mcdot{})

---

Home Index