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