Nuprl Lemma : not_over_forall

Nuprl Lemma : not_over_forall_form

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, 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], exists:

x:A. B[x], uall:

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