Nuprl Lemma : vr_BOOLDI_wf
vr_BOOLDI 
'
Proof not projected
Definitions occuring in Statement :
vr_BOOLDI: vr_BOOLDI,
member: t T,
universe: Type
Definitions :
function: x:A 
B[x],
implies: P 
Q,
member: t T,
universe: Type,
prop: 
,
equal: s = t,
bool: 
,
all: 
x:A. B[x],
apply: f a,
vr_BOOLDI: vr_BOOLDI,
btrue: tt,
bfalse: ff
Lemmas :
bool_wf,
bfalse_wf,
btrue_wf
vr\_BOOLDI \mmember{} \mBbbU{}'
Date html generated:
2012_02_20-PM-03_34_13
Last ObjectModification:
2012_02_02-PM-01_55_31
Home
Index