Nuprl Lemma : vr_AC_bool_subset_to_bool
vr_PROOF_IRREL
(
R:
. 
P: . ((b:. (P b)) (b:. ((P b) 
(R P b) (b':. ((R P b') b = b'))))))
Proof not projected
Definitions occuring in Statement :
vr_PROOF_IRREL: vr_PROOF_IRREL,
bool: ,
prop: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
apply: f a,
function: x:A B[x],
equal: s = t
Definitions :
lambda: 
x.A[x],
apply: f a,
CollapseTHENA: Error :CollapseTHENA,
CollapseTHEN: Error :CollapseTHEN,
bool: ,
Auto: Error :Auto,
universe: Type,
prop: ,
function: x:A B[x],
product: x:A 
B[x],
exists: x:A. B[x],
equal: s = t,
implies: P Q,
all: x:A. B[x],
and: P Q,
member: t 
T,
vr_PROOF_IRREL: vr_PROOF_IRREL,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
limited-type: LimitedType,
subtype_rel: A 
r B,
uiff: uiff(P;Q),
uimplies: b supposing a,
less_than: a < b,
not: 
A,
ge: i 
j ,
le: A 
B,
strong-subtype: strong-subtype(A;B),
union: left + right,
guard: {T}
Lemmas :
bool_wf,
vr_PROOF_IRREL_wf
vr\_PROOF\_IRREL
{}\mRightarrow{} (\mexists{}R:\mBbbB{} {}\mrightarrow{} \mBbbP{} {}\mrightarrow{} \mBbbB{} {}\mrightarrow{} \mBbbP{}
\mforall{}P:\mBbbB{} {}\mrightarrow{} \mBbbP{}. ((\mexists{}b:\mBbbB{}. (P b)) {}\mRightarrow{} (\mexists{}b:\mBbbB{}. ((P b) \mwedge{} (R P b) \mwedge{} (\mforall{}b':\mBbbB{}. ((R P b') {}\mRightarrow{} b = b'))))))
Date html generated:
2012_02_20-PM-03_35_15
Last ObjectModification:
2012_02_02-PM-01_55_43
Home
Index