{ 
[env:EnvType]. [r:RunType]. (reliable-env(env; r) 
') }
{ Proof }
Definitions occuring in Statement :
RunType: RunType,
EnvType: EnvType,
reliable-env: reliable-env(env; r),
uall: [x:A]. B[x],
prop: ,
member: t T
Definitions :
uall: [x:A]. B[x],
member: t T,
so_lambda: 
x.t[x],
so_apply: x[s],
EnvType: EnvType,
RunType: RunType
Lemmas :
reliable-env_wf,
name_wf,
mData_wf,
RunType_wf,
EnvType_wf
\mforall{}[env:EnvType]. \mforall{}[r:RunType]. (reliable-env(env; r) \mmember{} \mBbbP{}')
Date html generated:
2011_08_17-PM-04_12_57
Last ObjectModification:
2011_06_18-AM-11_31_03
Home
Index