Nuprl Lemma : exists_over_implies

Nuprl Lemma : exists_over_implies_push

T:Type.

P:

.

Q:T

. ((

x:T. (P

(Q x)))

P

(

x:T. (Q 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, member: t

T, so_lambda:

x.t[x], exists:

x:A. B[x], uall:

[x:A]. B[x], so_apply: x[s]
Lemmas : exists_wf
\mforall{}T:Type. \mforall{}P:\mBbbP{}. \mforall{}Q:T {}\mrightarrow{} \mBbbP{}. ((\mexists{}x:T. (P {}\mRightarrow{} (Q x))) {}\mRightarrow{} P {}\mRightarrow{} (\mexists{}x:T. (Q x))) Date html generated: 2013_03_20-AM-09_45_16 Last ObjectModification: 2013_03_12-PM-06_24_03 Home Index