Nuprl Lemma : event-ordering+_inc
∀[T:Type]. (EO+(T) ⊆ EO)
Proof
Definitions occuring in Statement :
event-ordering+: EO+(Info),
event_ordering: EO,
uall: ∀[x:A]. B[x],
subtype: S ⊆ T,
universe: Type
Lemmas :
record+_subtype_rel,
event_ordering_wf,
es-base-E_wf,
record+_wf
\mforall{}[T:Type]. (EO+(T) \msubseteq{} EO)
Date html generated:
2015_07_17-PM-00_01_04
Last ObjectModification:
2015_01_28-AM-00_34_56
Home
Index