Nuprl Lemma : hw5_3_1
T:Type. C:
. P:T 
. ((
x:T. (C 
(P x))) C (x:T. (P x)))
Proof
Definitions occuring in Statement :
prop: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x],
universe: Type
Definitions :
all: x:A. B[x],
prop: ,
implies: P Q,
exists: x:A. B[x],
member: t 
T,
so_lambda: 
x.t[x],
uall: [x:A]. B[x],
so_apply: x[s]
Lemmas :
exists_wf
\mforall{}T:Type. \mforall{}C:\mBbbP{}. \mforall{}P:T {}\mrightarrow{} \mBbbP{}. ((\mexists{}x:T. (C {}\mRightarrow{} (P x))) {}\mRightarrow{} C {}\mRightarrow{} (\mexists{}x:T. (P x)))
Date html generated:
2013_03_20-AM-09_55_02
Last ObjectModification:
2012_11_27-AM-10_33_33
Home
Index