---

Step * of Lemma Message-eta

∀[f:Name ⟶ Type]. ∀[m:Message(f)].
  (m
  = if msg-authentic(m) then make-Authentic-Msg(msg-header(m);msg-body(m)) else make-Msg(msg-header(m);msg-body(m)) fi 
  ∈ 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
    =  if  msg-authentic(m)
        then  make-Authentic-Msg(msg-header(m);msg-body(m))
        else  make-Msg(msg-header(m);msg-body(m))
        fi  )


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