Nuprl Lemma : norep2_OkFor_wf
norep2_OkFor() 
EClass'()
Proof not projected
Definitions occuring in Statement :
norep2_OkFor: norep2_OkFor(),
Message: Message,
eclass: EClass(A[eo; e]),
member: t T,
function: x:A B[x],
int:
Definitions :
norep2_OkFor: norep2_OkFor(),
member: t T,
uall: 
[x:A]. B[x]
Lemmas :
norep2_ok'base_wf,
norep2_okfor_wf,
concat-lifting-loc-1_wf,
Message_wf,
simple-loc-comb-1_wf
norep2\_OkFor() \mmember{} \mBbbZ{} {}\mrightarrow{} EClass'(\mBbbZ{})
Date html generated:
2012_02_20-PM-03_37_12
Last ObjectModification:
2012_02_02-PM-01_56_59
Home
Index