---

Step * of Lemma eo-forward-member-eclass

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[e',hdr:Top].  (e' ∈b Base(hdr) ~ e' ∈b Base(hdr))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``member-eclass base-headers-msg-val`` 0
   THEN RepeatFor 4 (EqCD)
   THEN RWW "eo-forward-info" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[e',hdr:Top].    (e'  \mmember{}\msubb{}  Base(hdr)  \msim{}  e'  \mmember{}\msubb{}  Base(hdr))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``member-eclass  base-headers-msg-val``  0
  THEN  RepeatFor  4  (EqCD)
  THEN  RWW  "eo-forward-info"  0
  THEN  Auto)

---

Home Index