Nuprl Lemma : not_over_forall_form

Nuprl Lemma : not_over_forall_form_squash

T:Type.

P:T

. ((

t:T. (

P t))

(

t:T. (

P t)))

Proof

Definitions occuring in Statement : prop:

, all:

x:A. B[x], exists:

x:A. B[x], not:

A, squash:

T, implies: P

Q, apply: f a, function: x:A

B[x], universe: Type
Definitions : all:

x:A. B[x], prop:

, implies: P

Q, not:

A, false: False, member: t

T, so_lambda:

x.t[x], squash:

T, exists:

x:A. B[x], uall:

[x:A]. B[x], so_apply: x[s], guard: {T}
Lemmas : squash_wf, all_wf, exists_wf, not_wf
\mforall{}T:Type. \mforall{}P:T {}\mrightarrow{} \mBbbP{}. ((\mdownarrow{}\mexists{}t:T. (\mneg{}\mdownarrow{}P t)) {}\mRightarrow{} (\mneg{}\mdownarrow{}\mforall{}t:T. (\mdownarrow{}P t))) Date html generated: 2013_03_20-AM-09_45_07 Last ObjectModification: 2013_02_25-PM-07_55_10 Home Index