Nuprl Lemma : vr_PEXT_implies_PROOF_IRREL
vr_PEXT 
vr_PROOF_IRREL
Proof not projected
Definitions occuring in Statement :
vr_PROOF_IRREL: vr_PROOF_IRREL,
vr_PEXT: vr_PEXT,
implies: P Q
Definitions :
ifthenelse: if b then t else f fi ,
btrue: tt,
equal: s = t,
product: x:A 
B[x],
and: P 
Q,
iff: P 
Q,
implies: P Q,
universe: Type,
vr_PEXT: vr_PEXT,
function: x:A 
B[x],
member: t 
T,
all: 
x:A. B[x],
vr_PROOF_IRREL: vr_PROOF_IRREL,
prop: 
,
rev_implies: P Q,
bool: 
,
squash: 
T,
true: True,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
bfalse: ff
Lemmas :
bool_wf,
true_wf,
squash_wf,
ifthenelse_wf,
rev_implies_wf,
iff_wf,
vr_PEXT_implies_t_eq_f,
vr_PEXT_wf
vr\_PEXT {}\mRightarrow{} vr\_PROOF\_IRREL
Date html generated:
2012_02_20-PM-03_34_50
Last ObjectModification:
2012_02_02-PM-01_55_39
Home
Index