Nuprl Lemma : vr_COMP_wf
vr_COMP 
'
Proof not projected
Definitions occuring in Statement :
vr_COMP: vr_COMP,
member: t T,
universe: Type
Definitions :
rev_implies: P 
Q,
implies: P 
Q,
so_lambda: 
x.t[x],
and: P 
Q,
iff: P Q,
exists: 
x:A. B[x],
prop: 
,
all: 
x:A. B[x],
vr_COMP: vr_COMP,
member: t T,
so_apply: x[s],
uall: [x:A]. B[x]
Lemmas :
all_wf,
exists_wf,
iff_wf,
nat_wf
vr\_COMP \mmember{} \mBbbU{}'
Date html generated:
2012_02_20-PM-03_35_20
Last ObjectModification:
2012_02_02-PM-01_55_44
Home
Index