---

Step * of Lemma member-base-class

∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name].  header(e) = hdr ∈ Name 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 (InstLemma `member-implies-classrel` [⌜Message(f)⌝;⌜f hdr⌝;⌜Base(hdr)⌝;⌜es⌝;⌜e⌝]⋅
         THENA (Auto THEN D 0 THEN Auto)
         )
   THEN SqExRepD
   THEN FLemma `base-noloc-classrel` [-1]
   THEN Auto
   THEN D 0
   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:
((UnivCD
    THENA  (Auto  THEN  Using  [`U',\mkleeneopen{}f  hdr\mkleeneclose{}]  (BLemma  `member-eclass\_wf`)\mcdot{}  THEN  Auto  THEN  D  0  THEN  Auto)
    )
  THEN  (InstLemma  `member-implies-classrel`  [\mkleeneopen{}Message(f)\mkleeneclose{};\mkleeneopen{}f  hdr\mkleeneclose{};\mkleeneopen{}Base(hdr)\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  D  0  THEN  Auto)
              )
  THEN  SqExRepD
  THEN  FLemma  `base-noloc-classrel`  [-1]
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index