{ 
[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