Nuprl Lemma : vr_test_abs2_wf
[f:Type]. [f:f]. (vr_test_abs2(x.f[x]) 
)
Proof not projected
Definitions occuring in Statement :
vr_test_abs2: vr_test_abs2(x.f[x]),
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
int: ,
universe: Type
Definitions :
vr_test_abs2: vr_test_abs2(x.f[x]),
member: t T,
uall: [x:A]. B[x]
\mforall{}[f:Type]. \mforall{}[f:f]. (vr\_test\_abs2(x.f[x]) \mmember{} \mBbbZ{})
Date html generated:
2012_02_20-PM-03_35_45
Last ObjectModification:
2012_02_02-PM-03_29_03
Home
Index