Step * of Lemma eo-forward-base-classfun-res

[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type].
  (Base(hdr)@e' Base(hdr)@e' ∈ T) supposing ((header(e') hdr ∈ Name) and hdr encodes T)
BY
(Auto THEN RepUR ``classfun-res`` 0⋅ THEN BLemma `eo-forward-base-classfun`  THEN Auto) }


Latex:



Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[e':E].  \mforall{}[hdr:Name].  \mforall{}[T:Type].
    (Base(hdr)@e'  =  Base(hdr)@e')  supposing  ((header(e')  =  hdr)  and  hdr  encodes  T)


By


Latex:
(Auto  THEN  RepUR  ``classfun-res``  0\mcdot{}  THEN  BLemma  `eo-forward-base-classfun`    THEN  Auto)




Home Index