---

Step * of Lemma eo-forward-base-classfun

∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type].
  (Base(hdr)(e') = Base(hdr)(e') ∈ T) supposing ((header(e') = hdr ∈ Name) and hdr encodes T)
BY
{ (Auto
   THEN RepUR ``base-headers-msg-val classfun cond-msg-body`` 0
   THEN (RWO "eo-forward-info" 0⋅ THENA Auto)
   THEN Fold `member` 0
   THEN Fold `cond-msg-body` 0
   THEN BLemma `cond-msg-body-sv-bag-only`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[e':E].  \mforall{}[hdr:Name].  \mforall{}[T:Type].
    (Base(hdr)(e')  =  Base(hdr)(e'))  supposing  ((header(e')  =  hdr)  and  hdr  encodes  T)


By

---

Latex:
(Auto
  THEN  RepUR  ``base-headers-msg-val  classfun  cond-msg-body``  0
  THEN  (RWO  "eo-forward-info"  0\mcdot{}  THENA  Auto)
  THEN  Fold  `member`  0
  THEN  Fold  `cond-msg-body`  0
  THEN  BLemma  `cond-msg-body-sv-bag-only`
  THEN  Auto)

---

Home Index