{ 
[T:Type]. (ClassProgram(T) 
') }
{ Proof }
Definitions occuring in Statement :
class-program: ClassProgram(T),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
class-program: ClassProgram(T),
so_lambda: 
x.t[x],
prop: 
,
all: x:A. B[x],
subtype: S 
T,
so_apply: x[s]
Lemmas :
fpf_wf,
Id_wf,
Knd_wf,
assert_wf,
hasloc_wf,
l_member_wf,
top_wf
\mforall{}[T:Type]. (ClassProgram(T) \mmember{} \mBbbU{}')
Date html generated:
2011_08_16-AM-11_01_11
Last ObjectModification:
2011_06_18-AM-09_34_43
Home
Index