{ [Info,T:Type]. [X:EClass(T)]. [es:EO+(Info)]. [e:E].
    (inhabited-classrel(es;T;X;e)  ) }

{ Proof }



Definitions occuring in Statement :  inhabited-classrel: inhabited-classrel(eo;T;X;e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E uall: [x:A]. B[x] prop: member: t  T universe: Type
Definitions :  tactic: Error :tactic,  member: t  T isect: x:A. B[x] es-E: E event_ordering: EO event-ordering+: EO+(Info) uall: [x:A]. B[x] eclass: EClass(A[eo; e]) so_lambda: x y.t[x; y] universe: Type equal: s = t prop: inhabited-classrel: inhabited-classrel(eo;T;X;e) axiom: Ax all: x:A. B[x] function: x:A  B[x] subtype: S  T lambda: x.A[x] squash: T exists: x:A. B[x] product: x:A  B[x] classrel: v  X(e)
Lemmas :  classrel_wf squash_wf event-ordering+_wf event-ordering+_inc es-E_wf eclass_wf

\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].    (inhabited-classrel(es;T;X;e)  \mmember{}  \mBbbP{})


Date html generated: 2011_08_16-AM-11_29_44
Last ObjectModification: 2011_06_08-PM-01_12_54

Home Index