{ 
[d:ClassDerivation]. (cdv-types(d) 
Type List) }
{ Proof }
Definitions occuring in Statement :
cdv-types: cdv-types(dv),
classderiv: ClassDerivation,
uall: [x:A]. B[x],
member: t T,
list: type List,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
cdv-types: cdv-types(dv),
so_lambda: 
x.t[x],
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_lambda: so_lambda(x,y,z,w,v.t[x; y; z; w; v]),
so_apply: x[s],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2;s3;s4;s5]
Lemmas :
classderiv_ind_wf,
base-deriv-type_wf,
base-deriv_wf,
append_wf,
classderiv_wf,
unit_wf,
top_wf
\mforall{}[d:ClassDerivation]. (cdv-types(d) \mmember{} Type List)
Date html generated:
2011_08_17-PM-04_26_40
Last ObjectModification:
2011_06_18-AM-11_39_03
Home
Index