Step
*
of Lemma
event-ordering+_inc
∀[T:Type]. (EO+(T) ⊆ EO)
BY
{ (Unfold `event-ordering+` 0 THEN Auto) }
Latex:
\mforall{}[T:Type].  (EO+(T)  \msubseteq{}  EO)
By
(Unfold  `event-ordering+`  0  THEN  Auto)
Home
Index