---

Step * of Lemma classfun-res-member-base

∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name].  Base(hdr)@e ~ msgval(e) supposing ↑e ∈b Base(hdr)
BY
{ ((UnivCD THENA (Auto THEN Using [`U',⌈f hdr⌉] (BLemma `member-eclass_wf`)⋅ THEN Auto THEN D 0 THEN Auto))
   THEN BLemma `classfun-res-base`
   THEN Auto
   THEN BLemma `member-base-class`⋅
   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  \muparrow{}e  \mmember{}\msubb{}  Base(hdr)


By

---

Latex:
((UnivCD
    THENA  (Auto  THEN  Using  [`U',\mkleeneopen{}f  hdr\mkleeneclose{}]  (BLemma  `member-eclass\_wf`)\mcdot{}  THEN  Auto  THEN  D  0  THEN  Auto)
    )
  THEN  BLemma  `classfun-res-base`
  THEN  Auto
  THEN  BLemma  `member-base-class`\mcdot{}
  THEN  Auto)

---

Home Index