---

Step * of Lemma eo-forward-base-classrel

∀[f:Name ─→ Type]. ∀[eo:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type]. ∀[v:T].
  uiff(v ∈ Base(hdr)(e');v ∈ Base(hdr)(e')) supposing hdr encodes T
BY
{ (Auto
   THEN MaUseClassRel (-1)
   THEN MaUseClassRel 0
   THEN All (Unfold `cond-msg-body`)
   THEN (RWW "eo-forward-info" (-1) THEN RWW "eo-forward-info" 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[eo:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[e':E].  \mforall{}[hdr:Name].  \mforall{}[T:Type].  \mforall{}[v:T].
    uiff(v  \mmember{}  Base(hdr)(e');v  \mmember{}  Base(hdr)(e'))  supposing  hdr  encodes  T


By

---

Latex:
(Auto
  THEN  MaUseClassRel  (-1)
  THEN  MaUseClassRel  0
  THEN  All  (Unfold  `cond-msg-body`)
  THEN  (RWW  "eo-forward-info"  (-1)  THEN  RWW  "eo-forward-info"  0)
  THEN  Auto)

---

Home Index