---

{ [T:Type]. (EO+(T)  ') }

{ Proof }

---

Definitions occuring in Statement :  event-ordering+: EO+(Info),  uall: [x:A]. B[x],  member: t  T,  universe: Type
Definitions :  token: "$token",  lambda: x.A[x],  axiom: Ax,  event-ordering+: EO+(Info),  universe: Type,  so_lambda: x.t[x],  es-base-E: es-base-E(es),  event_ordering: EO,  record+: record+,  all: x:A. B[x],  function: x:A  B[x],  uall: [x:A]. B[x],  isect: x:A. B[x],  member: t  T,  equal: s = t
Lemmas :  record+_wf,  event_ordering_wf,  es-base-E_wf

---

\mforall{}[T:Type].  (EO+(T)  \mmember{}  \mBbbU{}')


Date html generated: 2011_08_16-AM-11_20_29
Last ObjectModification: 2011_06_20-AM-00_25_14

Home Index