{ 
[cr:CompilationResult]. (comp-wf(cr) 
') }
{ Proof }
Definitions occuring in Statement :
comp-wf: comp-wf(cr),
compilation-result: CompilationResult,
uall: [x:A]. B[x],
prop: ,
member: t T
Definitions :
uall: [x:A]. B[x],
member: t T,
prop: ,
comp-wf: comp-wf(cr),
top: Top,
compilation-result: CompilationResult
Lemmas :
pi1_wf_top,
compilation-result_wf
\mforall{}[cr:CompilationResult]. (comp-wf(cr) \mmember{} \mBbbP{}')
Date html generated:
2011_08_17-PM-04_37_04
Last ObjectModification:
2011_06_18-AM-11_48_14
Home
Index