---

Step * of Lemma member-base-class2

∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name].  header(e) = hdr ∈ Name supposing ↑e ∈b Base(hdr)
BY
{ (InstLemma `member-base-class` [] THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `member-base-class`  []  THEN  Auto)

---

Home Index