---

Step * of Lemma classfun-res-base

∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name].  Base(hdr)@e ~ msgval(e) supposing header(e) = hdr ∈ Name
BY
{ (Auto
   THEN RepUR ``classfun-res classfun base-headers-msg-val cond-msg-body`` 0
   THEN AutoSplit
   THEN Try ((Fold `es-info-body` 0 THEN Auto))
   THEN D (-2)
   THEN Fold `es-header` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[hdr:Name].
    Base(hdr)@e  \msim{}  msgval(e)  supposing  header(e)  =  hdr


By

---

Latex:
(Auto
  THEN  RepUR  ``classfun-res  classfun  base-headers-msg-val  cond-msg-body``  0
  THEN  AutoSplit
  THEN  Try  ((Fold  `es-info-body`  0  THEN  Auto))
  THEN  D  (-2)
  THEN  Fold  `es-header`  0
  THEN  Auto)

---

Home Index