Step
*
of Lemma
es-all-events_wf
∀[Info:Type]. ∀[es:EO+(Info)].  (E ∈ EClass(Top))
BY
{ (Unfolds ``es-all-events eclass`` 0 THEN Auto) }
Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].    (E  \mmember{}  EClass(Top))
By
(Unfolds  ``es-all-events  eclass``  0  THEN  Auto)
Home
Index