Nuprl Lemma : TR6b

[T:Type].

[P:T

].

[C:

]. ((C

(

C))

(

x:T. ((P x)

C))

((

x:T. (P x))

C))

Proof

Definitions occuring in Statement : uall:

[x:A]. B[x], prop:

, all:

x:A. B[x], not:

A, implies: P

Q, or: P

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

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

[x:A]. B[x], member: t

T, prop:

, implies: P

Q, so_lambda:

x.t[x], guard: {T}, or: P

Q, all:

x:A. B[x], so_apply: x[s], not:

A, false: False
Lemmas : all_wf, or_wf, not_wf
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. \mforall{}[C:\mBbbP{}]. ((C \mvee{} (\mneg{}C)) {}\mRightarrow{} (\mforall{}x:T. ((P x) \mvee{} C)) {}\mRightarrow{} ((\mforall{}x:T. (P x)) \mvee{} C)) Date html generated: 2014_07_17-AM-09_55_47 Last ObjectModification: 2014_06_18-PM-04_14_55 Home Index